A Survey of Satisfiability Modulo Theory <s> Inductiveness Check and Bounded Model Checking <s> "The Formal Semantics of Programming Languages" provides the basic mathematical techniques necessary for those who are beginning a study of semantics and logics of programming languages. Although the treatment is elementary, several of the topics covered are drawn from recent research, including the vital area of concurrency. Starting with basic set theory, structural operational semantics is introduced as a way to define the meaning of programming languages along with associated proof techniques. Denotational and axiomatic semantics are illustrated on a simple language of while-programs, and full proofs are given of the equivalence of the operational and denotational semantics and soundness and relative completeness of the axiomatic semantics. A proof of Goedel's incompleteness theorem, which emphasizes the impossibility of achieving a fully complete axiomatic semantics, is included. It is supported by an appendix providing an introduction to the theory of computability based on while-programs. Following a presentation of domain theory, the semantics and methods of proof for several functional languages are treated. The simplest language is that of recursion equations with both call-by-value and call-by-name evaluation. This work is extended to languages with higher and recursive types, including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship between denotational and operational semantics is stressed, and the proofs of the correspondence between the operation and denotational semantics are provided. The treatment of recursive types - one of the more advanced parts of the book - relies on the use of information sytems to represent domains. The book concludes with a chapter on parallel programming languages, accompanied by a discussion of methods for specifying and verifying non-deterministic and parallel programs. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Inductiveness Check and Bounded Model Checking <s> We consider the problem of computing numerical invariants of programs, for ::: instance bounds on the values of numerical program variables. More ::: specifically, we study the problem of performing static analysis by abstract ::: interpretation using template linear constraint domains. Such invariants can be ::: obtained by Kleene iterations that are, in order to guarantee termination, ::: accelerated by widening operators. In many cases, however, applying this form ::: of extrapolation leads to invariants that are weaker than the strongest ::: inductive invariant that can be expressed within the abstract domain in use. ::: Another well-known source of imprecision of traditional abstract interpretation ::: techniques stems from their use of join operators at merge nodes in the control ::: flow graph. The mentioned weaknesses may prevent these methods from proving ::: safety properties. The technique we develop in this article addresses both of ::: these issues: contrary to Kleene iterations accelerated by widening operators, ::: it is guaranteed to yield the strongest inductive invariant that can be ::: expressed within the template linear constraint domain in use. It also eschews ::: join operators by distinguishing all paths of loop-free code segments. Formally ::: speaking, our technique computes the least fixpoint within a given template ::: linear constraint domain of a transition relation that is succinctly expressed ::: as an existentially quantified linear real arithmetic formula. In contrast to ::: previously published techniques that rely on quantifier elimination, our ::: algorithm is proved to have optimal complexity: we prove that the decision ::: problem associated with our fixpoint problem is in the second level of the ::: polynomial-time hierarchy. <s> BIB002 </s> A Survey of Satisfiability Modulo Theory <s> Inductiveness Check and Bounded Model Checking <s> We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs. <s> BIB003 </s> A Survey of Satisfiability Modulo Theory <s> Inductiveness Check and Bounded Model Checking <s> Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. <s> BIB004
In some other cases BIB002 BIB003  , the formula encodes the full set of executions between two control locations in a program, such that there is no looping construct between these locations: one Boolean variable is added per control location, expressing whether or not the execution goes through that location. In the Floyd-Hoare approach to proving the correctness of programs (see e.g. BIB001 ), the user is prompted for an inductive invariant for each looping construct: a formula I that holds at loop initiation, and that, if it holds at one loop iteration, holds at the next (inductiveness). In other words, there is no execution of the loop guard and loop body that starts in I and ends in ¬I ′ (I ′ is I where the variables are renamed in order to express their final, not initial, values). In modern tools, the loop guard and body are turned into a first-order formula that is conjoined with I and ¬I ′ , then checked for unsatisfiability; or equivalently through a weakest precondition computation, as in Frama-C BIB004 . In order to prove the postcondition ∀k 0 ≤ k < n ⇒ t[k] = 42, one needs the loop invariant The inductiveness condition is where update(t, i, 42) is the array t where i has been replaced by 42, and is formula I where i has been replaced by x. This condition is checked by showing that the negation of this formula is unsatisfiable -after Skolemization: is introduced to handle the uninterpreted function f (Sec. 2.6) and the resulting problem is solved over linear integer arithmetic (Sec.2.4).