Formal verification and program synthesis

Formal verification is proving, with mathematical logic, that a program or system satisfies a precise specification for every possible input or behaviour, not only for the cases a test happened to try. Program synthesis is the converse task: constructing a program automatically from a specification, a set of examples, or both.

This page is one of the family pages of Symbolic AI techniques. Its methods use the logic and proof machinery of logic programming and theorem proving and the solvers of constraint satisfaction, SAT and SMT. For the field as a whole see What is symbolic AI? and the history of symbolic AI.

1. Deductive verification: Hoare logic and its successors

Hoare logic

Who and when. C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 1969 [1], building on Robert Floyd’s “Assigning Meanings to Programs” (1967), which attached assertions to flowcharts [2]. The system is often called Floyd–Hoare logic.

What it is. A Hoare triple $\left\{P\right\}S\left\{Q\right\}$ says: if the precondition $P$ holds before the command $S$ runs, and $S$ terminates, then the postcondition $Q$ holds afterwards. That is partial correctness; total correctness also requires proving termination. The core rules:

Read clockwise from the top left: the assignment axiom, sequential composition, the rule of consequence, and the while rule with loop invariant $I$.

Worked example: the assignment axiom. What must be true before $y:=x+1$ for $y>10$ to hold after? The axiom answers by substitution, backwards: replace $y$ by $x+1$ in the postcondition.

So $\{x>9\}y:=x+1\{y>10\}$, and by the rule of consequence any stronger precondition, such as $x=42$, also works. The backwards direction is the point: it turns program text into a logical formula that a solver can check.

A loop. For i := 0; s := 0; while i < n do (i := i + 1; s := s + i) with precondition $n\ge 0$, take the invariant

It holds after initialisation ($0=0$, $0\le n$). If it holds and $i<n$, one iteration gives $s^{\prime }=\frac{i(i+1)}{2}+(i+1)=\frac{(i+1)(i+2)}{2}$ and $i+1\le n$, so it is preserved. On exit $I\wedge i\ge n$ forces $i=n$ and hence $s=n(n+1)/2$. The quantity $n-i$ decreases and stays non-negative, which proves termination.

Where it is used today. Every auto-active verifier (Dafny, Why3, Frama-C’s WP plug-in, SPARK) generates verification conditions this way. Limits. Someone has to find the loop invariants, and the rules as stated do not handle pointers, aliasing or concurrency well; the next two entries address that.

Weakest preconditions

Who and when. Edsger W. Dijkstra, “Guarded Commands, Nondeterminacy and Formal Derivation of Programs”, Communications of the ACM, 1975 [3]. What it is. A predicate transformer: $\mathrm{wp}(S,Q)$ is the weakest condition under which $S$ is guaranteed to terminate in a state satisfying $Q$. It is computed structurally: $\mathrm{wp}(x:=E,Q)=Q[E/x]$ and $\mathrm{wp}(S;T,Q)=\mathrm{wp}(S,\mathrm{wp}(T,Q\left)\right)$. A program is correct when $P\to \mathrm{wp}(S,Q)$ is valid. Dijkstra used the calculus to derive programs from their specifications, which makes it an ancestor of program synthesis too.

Separation logic

Who and when. John C. Reynolds, Peter O’Hearn, Samin Ishtiaq and Hongseok Yang, 1999–2002; Reynolds’s LICS 2002 paper is the standard reference [4]. What it is. An extension of Hoare logic for programs that manipulate pointers. The separating conjunction $P\ast Q$ says the heap splits into two disjoint parts satisfying $P$ and $Q$. That gives the frame rule, which lets a proof about one part of memory ignore the rest:

Where it is used today. Meta’s Infer, open-sourced in 2015, applies separation logic with bi-abduction to find memory and resource bugs in large codebases before they ship [5]. Stephen Brookes and Peter O’Hearn received the 2016 Gödel Prize for concurrent separation logic.

2. Model checking and temporal logic

Temporal logic: LTL and CTL

Who and when. Amir Pnueli, “The Temporal Logic of Programs”, FOCS 1977, brought temporal logic into computer science to state properties of ongoing, reactive programs [6]; he received the 1996 Turing Award for it. Linear temporal logic (LTL) talks about single infinite executions. On a path $\pi =s_0{s}_1{s}_2\dots$, with ${\pi }^i$ the suffix starting at $s_i$:

A safety property says something bad never happens ($\mathbf{G}\neg \mathrm{crash}$); a liveness property says something good eventually happens ($\mathbf{G}(\mathrm{req}\to \mathbf{F}\mathrm{grant})$). Computation tree logic (CTL), introduced by Clarke and Emerson, quantifies over the branching future instead: $\mathbf{AG}\phi$ means on all paths, always; $\mathbf{EF}\phi$ means on some path, eventually. Neither logic contains the other; CTL* contains both.

Model checking

Who and when. Edmund Clarke and E. Allen Emerson (work of 1981, published 1982) [7], and independently Jean-Pierre Queille and Joseph Sifakis (1982) [8]. The three shared the 2007 Turing Award “for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.”

What it is. Given a finite model of a system, a Kripke structure $M=(S,S_0,R,L)$ of states, initial states, transitions and state labels, and a temporal formula $\phi$, decide automatically whether $M\models \phi$: whether every execution from an initial state satisfies $\phi$. If not, return a counterexample execution.

Worked example: checking an LTL property on a tiny system. A resource arbiter with three states: $s_0$ idle, $s_1$ labelled $\mathrm{req}$, $s_2$ labelled $\mathrm{grant}$; the idle state may wait.

Property 1: ${\phi }_1=\mathbf{G}(\mathrm{req}\to \mathbf{F}\mathrm{grant})$, every request is eventually granted. The only state labelled $\mathrm{req}$ is $s_1$, and its only successor is $s_2$, labelled $\mathrm{grant}$. So on every path, every position at $s_1$ is followed one step later by $\mathrm{grant}$, and positions at $s_0$ or $s_2$ satisfy the implication trivially. Verdict: $M\models {\phi }_1$.

Property 2: ${\phi }_2=\mathbf{G}\mathbf{F}\mathrm{grant}$, a grant happens infinitely often. The path $s_0{s}_0{s}_0\dots$, waiting forever, never reaches $s_2$. Verdict: $M⊭{\phi }_2$, and the model checker returns that lasso-shaped path as the counterexample. Whether this is a bug depends on intent: if clients must eventually ask, the fix is a fairness assumption, not a code change. The counterexample is what makes that conversation concrete.

How checkers do it. CTL is checked by computing fixpoints over sets of states, in time linear in the size of the model and of the formula. LTL is checked by translating $\neg \phi$ into a Büchi automaton, taking its product with the model and searching for an accepting cycle; the problem is PSPACE-complete in the formula but linear in the model.

Where it is used today. Hardware verification in the chip industry, communication protocols, device drivers, and distributed-systems designs. Engineers at Amazon Web Services reported using the TLA+ specification language and its model checker to find subtle bugs in designs such as DynamoDB and S3 [9].

Limits. The state-explosion problem: the number of states grows exponentially with the number of variables and concurrent components. The next three entries are the main responses to it.

Symbolic model checking with BDDs

Randal Bryant’s reduced ordered binary decision diagrams (1986) give a canonical, often compact representation of Boolean functions [10]. Burch, Clarke, McMillan, Dill and Hwang (1990) used them to represent sets of states and the transition relation as formulas rather than lists, checking systems with more than ${10}^{20}$ states [11]. Tools such as NuSMV descend from this work. BDDs can still blow up, depending heavily on variable ordering.

Bounded model checking

Biere, Cimatti, Clarke and Zhu (1999) unrolled the transition relation $k$ steps and handed the question “is there a counterexample of length at most $k$?” to a SAT solver [12]. It finds shallow bugs fast and rides on SAT solver progress; on its own it proves only the absence of short counterexamples. CBMC applies the idea to C programs.

The SPIN model checker

Gerard Holzmann began SPIN at Bell Labs in 1980; it has been freely available since 1991 and received the ACM Software System Award in 2001 [13]. Models are written in Promela, properties in LTL, and SPIN generates a problem-specific verifier in C, using partial-order reduction and bitstate hashing to fight state explosion.

3. Term rewriting and Knuth–Bendix completion

Term rewriting

What it is. A term rewriting system is a set of directed equations $l\to r$. To rewrite a term, find a subterm that matches some $l$ and replace it by the corresponding instance of $r$; repeat until no rule applies, reaching a normal form. Two properties make this a decision procedure for equality:

• Termination: no infinite rewrite sequence exists.
• Confluence: whenever a term rewrites to two different terms, both can be rewritten to a common term.

In a terminating and confluent (convergent) system every term has exactly one normal form, so $s=t$ follows from the equations exactly when $s$ and $t$ have the same normal form. Where it is used today. Computer algebra simplifiers, compiler optimisation passes, the equational engines inside theorem provers, and rewriting languages such as Maude. Limits. Termination and confluence are undecidable in general, and many useful theories (commutativity, for example) have no convergent orientation at all.

Knuth–Bendix completion

Who and when. Donald Knuth and Peter Bendix, “Simple Word Problems in Universal Algebras”, 1970 [14]. What it does. It tries to turn a set of equations into a convergent rewriting system for the same theory. Orient each equation by a reduction ordering that guarantees termination; find every critical pair, a term where two rules overlap and rewrite differently; if the two results have different normal forms, add the equation between them as a new rule; simplify and repeat.

Worked example: groups. Start from the three group axioms, oriented left to right:

Rules 2 and 3 overlap on the term $(x^{-1}·x)·z$. Rule 3 rewrites it to $x^{-1}·(x·z)$; rule 2 and then rule 1 rewrite it to $z$. Both are irreducible and different, so the critical pair yields a new rule, $x^{-1}·(x·z)\to z$. Continuing, completion stops with ten rules: the three above, that one, and

With these ten rules any two group expressions can be tested for equality by rewriting both to normal form and comparing: the word problem for free groups, solved mechanically.

Where it is used today. Completion is built into equational theorem provers; its unfailing variant (Bachmair, Dershowitz and Plaisted, 1989) never gets stuck on an equation it cannot orient, and superposition provers such as E generalise it to full first-order logic. Limits. Completion may fail, when an equation cannot be oriented, or run forever, generating infinitely many rules.

4. Abstract interpretation

Abstract interpretation

Who and when. Patrick Cousot and Radhia Cousot, POPL 1977 [15]. Why it is needed. By Rice’s theorem, no algorithm can decide any non-trivial property of the behaviour of arbitrary programs. Abstract interpretation accepts that and chooses the safe side: compute an over-approximation of every behaviour. If the approximation contains no error, the program has none; if it contains one, the analyser raises an alarm, which may be false.

How it works. Concrete sets of values are related to abstract values by a Galois connection between an abstraction map $\alpha$ and a concretisation map $\gamma$:

Every program operation $F$ gets an abstract counterpart $F^{♯}$ that over-approximates it, and loops are solved as fixpoints in the abstract domain.

Worked example: signs. Abstract each integer to one of $\{-,0,+,\top \}$, where $\top$ means “unknown”. For x := -3; y := x * x; z := x + y: $x\mapsto -$; then $-{\times }^{♯}-=+$, so the analyser proves $y>0$ without running anything; then $-{+}^{♯}+=\top$, so it cannot say whether $z>0$ (in fact $z=6$). A division by $z$ would raise an alarm: sound, imprecise. Richer domains trade cost for precision: intervals, octagons (Miné, 2004), convex polyhedra (Cousot and Halbwachs, 1978). On domains with infinite ascending chains, such as intervals, a widening operator forces loop analysis to terminate, for instance by jumping from $[0,1],[0,2],\dots$ straight to $[0,+\infty )$.

Where it is used today. Astrée, from Cousot’s group at the École normale supérieure and now sold by AbsInt, has been used by Airbus since 2003 on safety-critical software for aircraft including the A380, and AbsInt reports runs with exactly zero false alarms on primary flight-control code [16]. Frama-C, Polyspace, IKOS and Infer apply the same theory.

Limits. Every sound analyser trades false alarms against cost. Precision on real code needs domains tuned to the code’s idioms, and a flood of false alarms is the most common reason such tools are abandoned.

5. SMT-based verification

SMT-based verification

What it is. Deductive verifiers turn a program and its annotations into verification conditions, formulas that are valid exactly when the program meets its specification, as in the Hoare example above. Satisfiability modulo theories (SMT) solvers decide such formulas over theories that programs need: integers, bit-vectors, arrays, uninterpreted functions. A formula is valid when its negation is unsatisfiable.

Who and when. Greg Nelson and Derek Oppen (1979) showed how to combine decision procedures for separate theories [17]. Modern SMT solvers pair that idea with a SAT solver’s search. Z3, by Leonardo de Moura and Nikolaj Bjørner at Microsoft Research (2008), is the most widely used [18]; it was open-sourced under the MIT licence in 2015. CVC5 and Yices are other major solvers.

Worked example. The verification condition from the Hoare example, $x>10\to x+1>10$, is checked by asserting its negation in the SMT-LIB language:

Where it is used today. Dafny, Microsoft’s verification-aware language, sends its conditions to Z3 [19]. Amazon Web Services’ Zelkova translates access-control policies into SMT formulas to answer questions such as “can anyone outside this account read this bucket?” [20]. Symbolic execution and bounded model checkers rely on SMT too. Limits. Quantifiers and non-linear arithmetic make the problems undecidable or very hard; a solver can answer unknown or time out, and results can change from one solver version to the next.

6. Program synthesis

Program synthesis: the problem

Alonzo Church posed the problem of synthesising a circuit from a logical specification at the 1957 Summer Institute of Symbolic Logic at Cornell. For programs, the classical statement is: given a specification $\phi (x,y)$ relating input $x$ and output $y$, find a program $f$ such that

For reactive systems that interact with an environment forever, Pnueli and Rosner (1989) gave the LTL version of the problem [21]; it is 2EXPTIME-complete.

Deductive program synthesis

Who and when. Zohar Manna and Richard Waldinger, beginning with “Toward Automatic Program Synthesis” (1971) and culminating in “A Deductive Approach to Program Synthesis” (1980) [22]. How it works. Prove the $\forall \exists$ statement constructively; the program is read off the proof. Case splits become conditionals, induction becomes recursion. Worked example. Specification: $\forall a,b.\exists z.z\ge a\wedge z\ge b\wedge (z=a\vee z=b)$. The proof splits on $a\ge b$: in that case $z=a$ works, otherwise $z=b$. The extracted program is max(a, b) = if a ≥ b then a else b, correct by construction. The same idea, programs as proofs, is how Rocq extracts executable code from verified developments. Limits. Finding the proof is at least as hard as writing the program, and the approach needs a complete formal specification, which users rarely have.

Inductive (example-based) synthesis: FlashFill

Who and when. Sumit Gulwani, “Automating String Processing in Spreadsheets Using Input-Output Examples”, POPL 2011 [23]. The technique shipped in Microsoft Excel as Flash Fill. How it works. The user types the desired output for one or two rows. The synthesiser searches a small domain-specific language of string transformations (substrings located by token patterns, constants, concatenation) for every program consistent with the examples, represents that set compactly, and ranks the candidates to prefer the simplest. From Alan Turing → A. Turing and Grace Hopper → G. Hopper it learns roughly first character of the first word, then “. ”, then the second word, and fills in the rest of the column. Limits. Examples under-specify intent: several programs fit, and the ranked choice can generalise wrongly on rows the user never checks. A tractable search needs a narrow language.

Sketching, CEGIS and syntax-guided synthesis

Armando Solar-Lezama’s Sketch (2006) lets a programmer write a program with holes and asks a SAT solver to fill them so the program meets a specification [24]. Its engine popularised counterexample-guided inductive synthesis (CEGIS): propose a candidate that works on a finite set of inputs, ask a verifier for an input where it fails, add that input, repeat. Syntax-guided synthesis (SyGuS, Alur et al., 2013) standardised the problem as a logical specification plus a grammar of allowed programs, with a common format and an annual competition [25]. Today large language models often generate candidate programs, and the symbolic verifier in a CEGIS-style loop decides which ones are kept.

7. Verified software: CompCert and seL4

Verified software

The techniques above scale to whole systems when the proof is mechanised in a proof assistant and maintained with the code. Two projects set the standard.

CompCert

A formally verified optimising compiler for a large subset of C, led by Xavier Leroy from 2005 and written and proved in Coq, now Rocq [26]. The theorem: the compiled code behaves as the source program’s semantics prescribes, so the compiler introduces no bugs of its own in the verified passes. The evidence that this matters came from testing. Yang, Chen, Eide and Regehr’s Csmith random tester found more than 325 previously unknown bugs in mainstream C compilers; in CompCert it found bugs only in unverified parts, and reported that “the middle-end bugs we found in all other compilers are absent” [27]. CompCert received the ACM Software System Award in 2021 and has been sold commercially by AbsInt since 2015.

seL4

A general-purpose operating-system microkernel with a machine-checked proof, in Isabelle/HOL, that its C implementation is functionally correct against its specification, completed in 2009 by Gerwin Klein and colleagues at NICTA [28]. Later proofs extended it to the compiled binary, removing the compiler from what must be trusted, and to integrity and confidentiality properties. seL4 was open-sourced in 2014 and was used in DARPA’s HACMS programme for high-assurance autonomous vehicles. What it does not say. The proofs cover the kernel against its model of the hardware; a wrong specification, a hardware fault or code outside the kernel is outside the theorem.

8. Timeline

9. What formal methods cannot do

• Verify against the wrong specification. A proof shows that the code matches the specification. If the specification is wrong or incomplete, the proof certifies the wrong thing.
• Escape undecidability. Rice’s theorem means every automatic tool either restricts the programs it handles, approximates (with false alarms), bounds the search, or can answer unknown.
• Beat state explosion in general. Symbolic representations, abstraction and bounding push the frontier; they do not remove it.
• Trust themselves. Every result rests on a trusted base: a proof checker, a solver, a model of the hardware or the environment. Keeping that base small and checked is part of the discipline.
• Come cheap. Full functional verification still costs a large multiple of the effort of writing the code. Lightweight uses, such as model checking a design or proving the absence of run-time errors, are where most of the industrial payoff is.

Learned models are entering the field from both ends: as generators of invariants, proofs and candidate programs, and as systems that themselves need verification. Combining the two is the subject of neuro-symbolic AI.

10. How this connects to fail-safe models

A sound static analyser is built the way a fail-safe model is meant to behave. When Astrée cannot prove a division safe, it does not guess that it probably is; it raises an alarm. Soundness is a commitment about which way the system errs: toward a refusal the user can inspect, never toward a silent pass. Model checking adds a second habit worth copying: a negative verdict comes with evidence, a concrete counterexample path, not a bare score.

Synthesis supplies the third pattern. In CEGIS, and in current systems where a language model proposes code, the proposer can be anything; the verifier decides what is kept. A fail-safe model applies the same division to facts and actions: a model may propose; only the floor admits a fact. The caveat carries over as well: an admission check is only as good as what it checks against, which is why the sources behind each admitted fact matter as much as the check.

Peel, by Perslis Research, is to our knowledge the first fail-safe model. Knowledge in Peel is typed, sourced cards; learning is readable counts; there is no neural network in the loop that decides. It is a research prototype, not a certified safety system. For why invariants over chains of models need a symbolic layer outside the models, see our paper The Orchestration Gap [29], and for the pipeline pattern built on it, symbolic flows.

11. Questions

What is formal verification?

Formal verification is proving, with mathematical logic, that a program or hardware design satisfies a precise specification for every possible input or behaviour. Unlike testing, which checks some cases, a completed verification covers all of them, relative to the specification and to the model of the system that was verified.

What is Hoare logic?

Hoare logic, introduced by C. A. R. Hoare in 1969, is a proof system for programs built on triples {P} S {Q}: if precondition P holds before command S and S terminates, postcondition Q holds after. Its rules cover assignment, sequencing, conditionals and loops; loops need an invariant. It is the basis of modern deductive program verifiers.

What is model checking?

Model checking is an automatic technique that decides whether a finite-state model of a system satisfies a temporal-logic property, by exploring its states. If the property fails, the model checker returns a counterexample execution. It was developed by Clarke and Emerson and by Queille and Sifakis in the early 1980s and earned them the 2007 Turing Award.

What is the difference between LTL and CTL?

LTL, linear temporal logic, describes properties of individual executions, such as G(req → F grant): on every run, every request is eventually granted. CTL, computation tree logic, quantifies over branching futures, such as EF grant: from here some execution can reach a grant. Each can express properties the other cannot; CTL* includes both.

What is abstract interpretation?

Abstract interpretation, introduced by Patrick and Radhia Cousot in 1977, is a theory of sound static analysis. It runs a program over abstract values, such as signs or intervals, that over-approximate every real execution. If the approximation shows no error, the program has none; otherwise the analyser raises an alarm, which may be a false positive.

What is program synthesis?

Program synthesis is the automatic construction of a program from a specification. Deductive synthesis extracts the program from a constructive proof that the specification can be met; inductive synthesis, such as Excel’s Flash Fill, searches a restricted language for programs consistent with input-output examples; syntax-guided synthesis combines a logical specification with a grammar.

What is an SMT solver used for in verification?

Verifiers turn programs and their specifications into logical formulas called verification conditions. An SMT solver such as Z3 decides whether such formulas are satisfiable over theories like integers, bit-vectors and arrays. A condition is proved valid when its negation is unsatisfiable; otherwise the solver usually returns a counterexample.

Does formal verification mean software has no bugs?

No. It means the software meets its specification under stated assumptions. Bugs can remain in the specification, in unverified components, in the hardware or in the tools that are trusted. Even so, random testing of the verified CompCert compiler found no wrong-code errors in its verified parts, which is why the effort is made.

12. References

1. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576–583, 1969. doi:10.1145/363235.363259.
2. R. W. Floyd. Assigning Meanings to Programs. Proceedings of Symposia in Applied Mathematics 19:19–32. American Mathematical Society, 1967.
3. E. W. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM 18(8):453–457, 1975. doi:10.1145/360933.360975.
4. J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), 55–74, 2002.
5. C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. O’Hearn, I. Papakonstantinou, J. Purbrick, D. Rodriguez. Moving Fast with Software Verification. NASA Formal Methods, LNCS, 3–11. Springer, 2015.
6. A. Pnueli. The Temporal Logic of Programs. 18th Annual Symposium on Foundations of Computer Science (FOCS), 46–57, 1977. doi:10.1109/SFCS.1977.32.
7. E. M. Clarke, E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In D. Kozen (ed.), Logics of Programs, LNCS 131, 52–71. Springer, 1982. doi:10.1007/BFb0025774.
8. J.-P. Queille, J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. International Symposium on Programming, LNCS, 337–351. Springer, 1982. doi:10.1007/3-540-11494-7_22.
9. C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, M. Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM 58(4):66–73, 2015. doi:10.1145/2699417.
10. R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8):677–691, 1986.
11. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang. Symbolic Model Checking: 10²⁰ States and Beyond. Fifth IEEE Symposium on Logic in Computer Science (LICS), 1990. doi:10.1109/LICS.1990.113767.
12. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, 193–207. Springer, 1999.
13. G. J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5):279–295, 1997.
14. D. E. Knuth, P. B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech (ed.), Computational Problems in Abstract Algebra, 263–297. Pergamon Press, 1970.
15. P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL), 238–252, 1977. doi:10.1145/512950.512973.
16. AbsInt. Astrée: Fast and Sound Runtime Error Analysis. Product documentation, absint.com/astree. Accessed 2026-09-26.
17. G. Nelson, D. C. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2):245–257, 1979. doi:10.1145/357073.357079.
18. L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963, 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24.
19. K. R. M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), LNCS, 348–370. Springer, 2010.
20. J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachuk, C. Varming. Semantic-Based Automated Reasoning for AWS Access Policies Using SMT. Formal Methods in Computer Aided Design (FMCAD), 1–9, 2018. doi:10.23919/FMCAD.2018.8602994.
21. A. Pnueli, R. Rosner. On the Synthesis of a Reactive Module. Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL), 1989. doi:10.1145/75277.75293.
22. Z. Manna, R. Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems 2(1):90–121, 1980. doi:10.1145/357084.357090. See also Toward Automatic Program Synthesis, Communications of the ACM, 1971. doi:10.1145/362566.362568.
23. S. Gulwani. Automating String Processing in Spreadsheets Using Input-Output Examples. Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL), 2011. doi:10.1145/1926385.1926423.
24. A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, V. Saraswat. Combinatorial Sketching for Finite Programs. ASPLOS 2006; ACM SIGPLAN Notices 41(11):404–415, 2006. doi:10.1145/1168918.1168907.
25. R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, A. Udupa. Syntax-Guided Synthesis. Formal Methods in Computer-Aided Design (FMCAD), 2013. doi:10.1109/FMCAD.2013.6679385.
26. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7):107–115, 2009. doi:10.1145/1538788.1538814.
27. X. Yang, Y. Chen, E. Eide, J. Regehr. Finding and Understanding Bugs in C Compilers. Proceedings of the 32nd ACM Conference on Programming Language Design and Implementation (PLDI), 2011.
28. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. seL4: Formal Verification of an OS Kernel. Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), 207–220, 2009. doi:10.1145/1629575.1629596.
29. Perslis Research. The Orchestration Gap: Why Model-Level Alignment Cannot Survive Multi-Model Runtimes. 2026. research.perslis.com/orchestration-gap