-
Chapter and Conference Paper
Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation
Developers of computer-aided cryptographic tools are optimistic that formal methods will become a vital part of develo** new cryptographic systems. We study the use of such tools to specify and verify the im...
-
Chapter and Conference Paper
cvc5: A Versatile and Industrial-Strength SMT Solver
cvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5 ’s architectural design and...
-
Chapter and Conference Paper
Building Better Bit-Blasting for Floating-Point Problems
An effective approach to handling the theory of floating-point is to reduce it to the theory of bit-vectors. Implementing the required encodings is complex, error prone and requires a deep understanding of flo...
-
Chapter and Conference Paper
Application of Abstract Interpretation to the Automotive Electronic Control System
The verification and validation of industrial automotive systems is increasingly challenging as they become larger and more complex. Recent automotive Electric Control Units (ECUs) have approximately one half ...
-
Chapter and Conference Paper
Invertibility Conditions for Floating-Point Formulas
Automated reasoning procedures are essential for a number of applic...
-
Article
Open AccessIncremental bounded model checking for embedded software
Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and test case generation are some of the most commo...
-
Chapter and Conference Paper
Automatic Generation of Propagation Complete SAT Encodings
Almost all applications of SAT solvers generate Boolean formulae from higher level expression graphs by encoding the semantics of each operation or relation into propositional logic. All non-trivial relations ...
-
Chapter and Conference Paper
\(\mathsf {SC}^\mathsf{2} \) : Satisfiability Checking Meets Symbolic Computation
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application...
-
Chapter and Conference Paper
Safety Verification and Refutation by k-Invariants and k-Induction
Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checki...
-
Chapter and Conference Paper
Successful Use of Incremental BMC in the Automotive Industry
Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the ...
-
Article
Open AccessDeciding floating-point logic with abstract conflict driven clause learning
We present a bit-precise decision procedure for the theory of floating-point arithmetic. The core of our approach is a non-trivial, lattice-theoretic generalisation of the conflict-driven clause learning algor...
-
Chapter and Conference Paper
Model and Proof Generation for Heap-Manipulating Programs
Existing heap analysis techniques lack the ability to supply counterexamples in case of property violations. This hinders diagnosis, prevents test-case generation and is a barrier to the use of these tools amo...
-
Chapter and Conference Paper
Simplifying the Verification of Quantified Array Assertions via Code Transformation
Quantified assertions pose a particular challenge for automated software verification tools. They are required when proving even the most basic properties of programs that manipulate arrays and so are a major ...
-
Chapter and Conference Paper
An Abstract Interpretation of DPLL(T)
dpll(t) is a central algorithm for Satisfiability Modulo Theories (smt) solvers. The algorithm combines results of reasoning about the Boolean structure of a formula with reasoning about conjunct...
-
Chapter and Conference Paper
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
One approach for smt solvers to improve efficiency is to delegate reasoning to abstract domains. Solvers using abstract domains do not support interpolation and cannot be used for interpolation-based verification...
-
Chapter and Conference Paper
A Lightweight Technique for Distributed and Incremental Program Verification
Applying automated verification to industrial code bases creates a significant computational task even when the individual conditions to be checked are trivial. This affects the wall clock time taken to verify...
-
Chapter and Conference Paper
ANTON: Composing Logic and Logic Composing
In most styles of music, composition is governed by a set of rules. We demonstrate that approaching the automation and analysis of composition declaratively, by expressing these rules in a suitable logical lan...
-
Chapter and Conference Paper
Generating Optimal Code Using Answer Set Programming
This paper presents the Total Optimisation using Answer Set Technology (TOAST) system, which can be used to generate optimal code sequences for machine architectures via a technique known as superoptimisation. An...
-
Chapter and Conference Paper
ASPVIZ: Declarative Visualisation and Animation Using Answer Set Programming
Answer set programming provides a powerful platform for model-based reasoning problems. The answer sets are solutions, but for many non-trivial problems post-processing is often necessary for human readability...
-
Chapter and Conference Paper
Automatic Composition of Melodic and Harmonic Music by Answer Set Programming
The composition of most styles of music is governed by rules. The natural statement of these rules is declarative (“The highest and lowest notes in a piece must be separated by a consonant interval”) and non d...
