-One of the main application areas and driving forces behind the development of Satisfiability Modulo Theory (SMT) solvers is software verification. The requirements of software verification are somewhat different to other applications of automated reasoning, posing a number of challenges but also providing some interesting opportunities. This paper brings together and summarises the algebras and structures of interest, along with some of the problems that are characteristic of software verification. It is hoped that this will allow computer algebra researchers to assess the applicability of their techniques to this challenging, but rewarding domain. Software verification is the prototypical application domain for Satisfiability Modulo Theory (SMT) solvers. There are many aspects of the two research fields that show a significant degree of co-evolution. For example, the central role of theories (and the theories that are available - for example bit-vectors and arrays) can be seen as a formalisation of the domain specific decision procedures that were used in early verification systems [1]. Universal quantification is challenging for most SMT solver algorithms, leading to poor performance and thus many software verification systems avoid generating quantifiers. Likewise the importance of model generation1 is in part driven but the utility of these models for providing execution or error traces in verification systems. The coevolution can also be seen in the SMT-LIB benchmarks which feature many benchmark collections generated by verification tools. This paper aims to highlight some of the requirements and 'evolutionary pressures' that software verification places on SMT solver development. It is hoped that this context will help computer algebra researchers to identify, develop and refine algorithms so that they can demonstrate impact on commercial-scale software verification problems. The topics raised are a mix between challenges that have to be overcome and opportunities in under-explored / critical areas.
Challenge: Tolerate irrelevant formulae. The formulae generated by verification tools tend to be very different from those generated by human modelling of problems. One of the real challenges of mathematical modelling is reducing the problem to a minimal core which captures the key challenge. This is a process which requires considerable intuition and experience and it is not clear whether automating it is even possible. Consequentally, compared to directly human generated formulae, the formulae generated by verification tools are much larger and contain a significant amount of ‘simple’ and ‘irrelevant’ parts.
Opportunity: Exploit disequalities and if-then-else. Software
verification problems tend to produce formulae with some
Boolean structure, particularly from the use of if-then-else
expression to model different paths of execution. One of the
advantages of the DPLL(T)[
Challenge: Handle inequalities. Another feature common in software verification problems that is not classically algebraic is the use of inequalities. Although there are some applications, such as equivalence checking, that are possible without inequalities, the frequency of ordering comparisons in most real software means these are a critical requirement.
II. ALGEBRAS AND STRUCTURES OF INTEREST As well as having formula structure unlike conventional, human generated algebraic problems, software verification problems also tend to use unconventional algebras and relational structures. A minority of software verification systems use integers2 and reals to model variables, particularly those focused on algorithm rather than program verification. However this approach seems to becoming less common as these do not capture the full behaviour of real systems (overflow, rounding, etc.) and also increase the complexity of the decision procedure.
Core to the performance of SMT solvers on software
verification problems is their handling of the theory of fixed
width bit-vector[
Opportunity: Sub-algebras. The range of operations in the theory of bit-vectors makes it hard to find decision procedures that work well for arbitrary formulae. However for many applications, groups of variables will only ever use a handful of operations. For example, variables used as counters will only assign constants, increment and check against bounds, variables that are used as bitmaps are rarely used in multiplications and the bitwise operations form a Boolean algebra, many modern cryptographic algorithms only use add, roll and xor (ARX) and floating-point operations make heavy use of a max-plus algebra with signed comparison. Thus finding useful sub-signatures of the theory of bit-vectors, identifying their algebraic structure and then building decision procedures that exploit this structure seems like a promising research direction.
Many software verification applications concern control systems which must use sensor data to control a real-world system (aircraft, train, industrial robots, UAVs, autonomous cars, “cyber-physical systems”, etc.). Pure integer and fixedpoint control systems are becoming a rarity with most control systems using floating-point. Thus there is a significant commercial drive for verification systems to handle floating-point numbers efficiently and effectively.
The so-called “standard model” converts floating-point expressions to real expressions. For example, if f and g are floating-point variables and r denotes floating-point addition with rounding mode r: f r g ; (f + g)(1 + ) j j 6 where is a small, format dependent constant. Although this model is simple, it has a number of limitations. An extensive set of side condition are required to correctly model actual hardware (no overflows, no subnormal numbers, etc.) and often these are the precise conditions we are trying to identify. If these are used then the standard model is an overapproximation of the behaviour of hardware, meaning that spurious SAT results can be given. Worse from an application point of view is that it is difficult to generate the bit-exact traces needed to assess, diagnose and fix real systems.
As a consequence, a theory of floating-point numbers[
Opportunity: Algebraic techniques on R . vFe;s has
relatively little algebraic structure – floating-point addition and
multiplication are famously non-associative. As not-a-number
is absorbing for all operations, R is not a field but it is
an additive and multiplicative commutative monoid with the
associativity property [
Opportunity: Mixed real and float. If v and round can be handled then this may not only be able to handle floating-point problems but also mixed float and real problems which are of considerable commercial interest.
Another interest driven by control systems is that of reasoning about differential equations. Most control systems are developed with respect to a model of the environment with which they are interacting. This is normally formalised as a system of differential equations. However due to limitations of the solver technology this is not directly used in the verification, instead a computational model is built. If solvers could handle differential equations of some form, it could significantly increase the ability of tools to verify these cyberphysical systems.
Opportunity: Symbolic algorithms for differential systems.
dReal [
Determining formula satisfiability is the core role of SMT solvers. However there are a number of similar and related symbolic reasoning tasks, both inside and outside the solver, that have significant practical impact and present interesting opportunities for applying algebraic techniques.
Expression simplification is a vital component in most SMT solvers and program verification systems. It is used for performing constant folding ((x + 1) + 1 ; x + 2), simplifications (x <= x ; true) and normalisation (!(x >= y) ; x < y). Although the rewriting steps are generally simple, their effects can be drastic. For example, given unsigned integers x, y and z of more than 16 bit: assert((x * y) * z == x * (y * z)); will cause most bit-vector decision procedures to time out but can be trivially resolved by a distributivity aware simplifier.
Opportunity: Improved simplification For such a key
component of solvers, there is relatively little in the conventional
published literature. There are papers that mention the number
of simplification rules used [
Current algorithms and verification systems are often built “on top of” SMT solvers. The solver (or solvers) are the lowest level component in the algorithm and satisfiability queries are used as a way of checking inclusion or intersection between sets (represented symbolically, using equations). This architecture has proven flexible and effective. However if the reasoning system can perform more than just satisfiability queries it can be used at a higher level within verification algorithms. This section presents verification algorithms ‘from the top down’, highlighting the other kinds of symbolic reasoning task that arise.
1) The Verification Question: We present a simple model of software verification using the transition systems view. This is perhaps idiomatic of the model checking community, especially hardware model checking but it nicely illustrates some of the key challenges.
Let x be a set of variables and v a set of values. A map s : x ! v that assigns value to variables is referred to as a state (in the context of transition systems) or a valuation (in the context of logical formulae). Let statesx;v denote x ! v, the space of all such maps. Critical to symbolic verification is the idea that we can use a formula (over x) to represent a set of states. To make the distinction between sets represented by formulae and sets described by other means, we will use JF (x)K to denote the set of all valuations (states) that satisfy formula F (x).
A symbolic representation of a transition system requires a formula for the initial states, I(x) and a formula that describes the transition relation between sets T (x; x0). As our interest will be in the sets of states which are reachable from a given set of states, we define forwards and backwards reachability steps:
= =
F RStep : 2statesx;v ! 2statesx;v S [ ft 2 2statesx;v jT (s; t) ^ s 2 Sg BRStep : 2statesx;v ! 2statesx;v
S [ ft 2 2statesx;v jT (t; s) ^ s 2 Sg
Both of these are monotonic and increasing on 2statesx;v , a
complete lattice, so by the Knaster-Tarski theorem they have
fixed-points which form a complete lattice [
= lf p( X:f (X [ S))
For simplicity we will consider safety properties; those which are false if there is an execution trace from an initial state to an unsafe state. P (x) is a formula describing the set of safe states and thus:
BReach system safe system safe = = ,
LF P (F RStep; JI(x)K) LF P (BRStep; J:P (x)K) F Reach JP (x)K
BReach \ JI(x)K = ;
If a formula describing F Reach or BReach can be found, then showing system safety reduces to a single satisfiability check. However there are no guarantees that the fixed-point can be described by a formulae and even when they can, there are few algorithms that can compute them. For example, consider the following two loops, with variables in N, one has a simple, computable fix-point, the other remains an open question: while (i < n) {
a[i] = n; } } while (i != 1) { if (i % 2 == 0) i = i/2; else i = 3*1 + 1;
Opportunity: Finding exact fixed-points. There are many interesting questions related to exact descriptions of fixedpoints; both theoretical (When does an expression over language L have a fixed-point representable in L’? Is finding it computable?) and practical (What are algorithms to compute them? Are there subsets of expressions for which fixed-point formula can be easily found?).
2) Approximate Approachs to Verification: When faced with a intractable or computationally expensive problem, a common approach in software verification is to approximate. If:
U
O ^ O F Reach ^ :(U
JP (x)K ) JP (x)K ) system safe :system safe
Thus we have reduced the problem from computing fixedpoints to finding (formulae that describe) sets of states that approximate the fix-points. From the definition of F Reach we have necessary and sufficient conditions for over and under approximations: JI(x)K
Inito ^ F RStep 6 F RStepo U
(1)
Initu JI(x)K ^ F RStepu 6 F RStep (2) Different approaches to verification can be seen as different ways of finding solutions to equations (1) or (2). Some of these are known as property directed and make of P (x) so they produce an approximation that allows the safety of the system to be determined. For example, the Hoare logic system uses inductive invariants; formula Inv(x) such that: I(x) ) Inv(x)
Inv(x) ^ T (x; x0) =) Inv(x0): This is a sufficient condition for (1) and has the advantage that it is stated purely in terms of formulae, reducing the problem to existential second-order logic. Bounded model checking aims using a sequence of solutions of (2), first I(x), then I(x) _ (I(x ) ^ T (x ; x));
next I(x) _ (I(x ) ^ T (x ; x)) _ (I(x ) ^ T (x ; x ) ^ T (x ; x)); and so on. These do not have fixed-points or second-order variables and thus can be solved with simple satisfiability calls. Abstract interpretation can be seen as picking F RStepo (abstract transformer) and Inito (initial abstract state) in such a way that LF P (F RStepo; Inito) is computable in the abstract domain.
Opportunity: Finding fixed-point approximations. As with computing exact fixed-points, there are both theoretical and practical challenges. Finding new sufficient solutions to (1) and (2), especially those without fixed-points or, ideally, second-order quantification would likely yield new algorithms. A classification theorem of what solutions exist or necessary conditions would also be of great interest. Practically, algorithms that compute over or under approximations, either using one of the sufficient conditions (such as finding invariants) or directly (as abstract interpretation does) are of great interest.
3) Pre-Image, Post-Image and Merging: One approach to computing solutions to (1) and (2) is to perform stepwise approximations. This requires approximating the pre or post image of the transition relation and being able to merge two or more approximations. Pre and post image approximations can be described as finding the strongest (setwise smallest) O(x) or the weakest (setwise largest) U (x) that satisfies the appropriate formulae (given either P re or P ost): Forwards Over : P re(x) ^ T (x; x0) ) O(x0) Forwards Under : U (x0) ) P re(x) ^ T (x; x0) Backwards Over : P ost(x0) ^ T (x; x0) ) O(x)
Backwards Under : U (x) ) P ost(x0) ^ T (x; x0) Although these involve second-order quantification (we are searching for formula), they do not involve fixed-points and are significantly more practical.
Merging of approximations is needed when multiple control flow paths converge, for example after an if statement or after a loop. It is sufficient to take the disjunction of the two formula but this tends to lead to unacceptable growth in formula size. Thus it is useful to be able to find the smallest O(x) or largest U (x) such that:
O1(x) _ O2(x) ) O(x)
U (x) ) U1(x) _ U2(x)
Opportunity: Step-wise Approximations. Computing abstract
pre and post-images can clearly be seen in algebraic terms.
Quantifier elimination, either via CAD [
4) Reducing Second-Order Quantification: The preceding
sections have reduced computing system correctness to finding
formulae with the required properties; effectively solving
existential second-order logic. Templates are a commonly used (for
example [
I(x)
l 6 x ^ x 6 u ^ T (x; x0)
l 6 x ^ x 6 u
)
)
)
l 6 x ^ x 6 u
l 6 x0 ^ x0 6 u
P (x)
which requires a solver that can handle quantification
alternation but is purely first-order logic. In abstract interpretation
terms the template can be seen as characterising an abstract
domain [
Opportunity: Template algorithms. Algorithms for working with specific templates are of great utility as evidenced by the range of abstract domains that are currently in use. Algorithms that can work with arbitrary templates or templates that are monotonic with respect to the constants have received some initial investigation but there are likely to be significant theoretical and practical gains to be made. Efficient implementations of such algorithms allow user specified templates but also allow templates to be chosen automatically, effectively refining the abstraction.
Modern software verification techniques are heavily dependent on efficient SMT solvers. Correspondingly SMT solver development is often motivated, inspired and justified by software verification applications. It is hoped that this paper acts as a guide for computer algebra researchers to understand this synergy, and appreciate some of the places algebraic approaches could be fruitfully deployed and to get involved!