CAV/CADE July/Aug 1996 Automated Deduction and Formal Methods

John Rushby

Computer Science Laboratory SRI International Menlo Park CA USA

A Missed Opportunity?

• Formal methods are a natural application for automated deduction ∘ Without automation they are neither formal, nor methods

• Yet most tools for formal methods use little more than elementary techniques from automated deduction

• And few theorem provers are used in formal methods

• Why is this? What capabilities are needed?

• A look at some examples

CAV&CADE 1996 2 of 43

Extent of Automated Deduction in Formal Methods

• Traditional formal methods (e.g., VDM, Z)

∘ Automation ranges from none to rudimentary

(“Proof Assistants”)

• Methods that stress tools (e.g., B and RAISE)

∘ Automation ranges from very to… fairly rudimentary

• Automated verification methods (e.g., model checkers) ∘ Fast, effective… but specialized

• Theorem provers used for FM (e.g., ACL2, Nqthm, RRL) ∘ Strong on rewriting and arithmetic; little or no quantification

• Integrated verification systems (e.g., Coq, Eves, HOL, LP, Nuprl, PVS, STeP, VSE) ∘ Interactive; some have quite substantial automation, but

based on relatively few techniques

CAV&CADE 1996 3 of 43

Good Sources of Examples

• “Critical systems” (those where cost of failure is unacceptable) currently provide the best opportunities for formal methods

∘ Safety and security-critical systems ∘ Consumer electronics (processors, smartcards)

• “Program verification” (proving consistency between executable code and detailed specifications) is no longer of much industrial interest

∘ Traditional techniques are effective (if crude) ∘ Very few critical coding bugs escape detection ∘ Accounts for < 2% of bugs and < 10% of costs in

sophisticated industries (e.g., aerospace)

Unless it can be totally automated (as for some hardware)

Good Sources of Examples

• Main opportunities are in requirements analysis (∼ 30% of costs and > 50% of faults)

• And intrinsically hard problems of design

∘ Has to be after-the-fact verification: unlikely to solve these

hard problems by derivation or programs-from-proofs ∘ Typically concern distributed, concurrent, real time, fault

tolerant systems

• Let’s start with an example that involves all of these

Clock Synchronization

• Context: fault-tolerant systems for critical real-time applications (aircraft flight control)

• Idea: run redundant processors in lock-step, perform identical calculations in all components, use exact-match voting

• Subproblems:

∘ Interactive Consistency (aka. Byzantine Agreement)

⋆ Single-source data are distributed consistently ∘ Clock Synchronization

• Assumptions about behavior of faulty components ∘ Byzantine fault model: no assumptions ∘ Hybrid fault model: some faults are “arbitrary” (Byzantine),

some “symmetric,” some “manifest” (tolerates more faults)

CAV&CADE 1996 6 of 43

Interactive Convergence Clock Synchronization Algorithm

• Due to Lamport and Melliar-Smith (JACM, Jan 85)

• Clocks drift (at rate bounded by ρ) and need to be resynchronized periodically to keep them within δ of each other

• Each processor reads the difference between its own clock and that of each other processor (Δ_{q p}^{(i)})

• Sets any difference greater than Δ to zero

• Takes arithmetic mean of these modified differences

• And adjusts its own clock by that amount

• Byzantine fault model:

requires n > 3m processors to withstand m faults

• Hybrid fault model: n > 3a + 2s + c processors to withstand a

arbitrary, s symmetric, and c manifest faults simultaneously

CAV&CADE 1996 7 of 43

Formal Treatment

• Clocks are uninterpreted functions from “clock time” to “real time” (both interpreted as reals) ∘ c_{p}(T) is the real time when p’s clock time is T

• Synchronize every R clock time units, by own clock

∘ i’th period denoted R^{(i)}, starts at T^{(i)}

T^{(i)} = T^{(0)} + iR

R^{(i)} = [T^{(i)}, T^{(i+1)} ]

∘ Algorithm takes S clock units at end of period

S^{(i)} = [T^{(i+1)} − S, T^{(i+1)} ]

• Adjustment to processor p’s clock in i’th period is C_{p}^{(i)}

∘ Adjusted clock is c_{p}^{(i)} (T) = c_{p}(T + C_{p}^{(i)} )

CAV&CADE 1996 8 of 43

Requirements (“Clock Synchronization Conditions”)

Bounded skew (S1): If p and q are nonfaulty through period i, then

|c_{p}^{(i)} (T) − c_{q}^{(i)} (T)| < δ

for all T in R^{(i)}.

Bounded adjustment (S2): If processor p is nonfaulty through period i, then

|C_{p}^{(i+1)} − C_{p}^{(i)} | < Σ.

For real time constant δ and clock time constant Σ that are parameters to the algorithm

Assumptions

Several of these including A2: If the clock synchronization conditions hold for the i’th period,

and processors p and q are nonfaulty through period i, then

|Δ_{q p}^{(i)}| ≤ S

and

|c_{p}^{(i)} (T′ + Δ_{q p}^{(i)}) − c_{q}^{(i)} (T′)| < ϵ

for some time T′ in S^{(i)}

Algorithm

For all processors p:

C_{p}^{(i+1)} = C_{p}^{(i)} + Δ_{p}^{(i)} ,

where

C_{p}^{(0)} is arbitrary,
Δ_{p}^{(i)} = (\frac{1}{n}) n ; ∑ ; r=1 Δ̄_{r p}^{(i)} , and
Δ̄_{r p}^{(i)} = if |Δ_{r p}^{(i)}| < Δ then Δ_{r p}^{(i)} else 0

and Δ is a clock time quantity that is a parameter to the algorithm

Constraints

C0: n > m ≥ 0 C1: R ≥ 3S C2: S ≥ Σ C3: Σ ≥ Δ > 0 C4: Δ ≥ δ + ϵ + \frac{ρ}{2} S C5: δ ≥ δ_{0} + ρR

C6: δ ≥ 2(ϵ + ρS) + \frac{2mΔ}{n − m} + \frac{nρR}{n − m} + \frac{nρΣ}{n − m} + ρΔ

CAV&CADE 1996 12 of 43

Lemmas

1. If the clock synchronization conditions S1 and S2 hold for i, and processors p and q are nonfaulty through period i + 1, then

|Δ_{q p}^{(i)}| < Δ

2. If processor p is nonfaulty through period i + 1, and T and Π are such that A_{p}^{(i)} (T) and A_{p}^{(i)} (T + Π) are both in the interval [A_{p}^{(0)} (T^{(0)} ), A_{p}^{(i+1)} (T^{(i+2)} )], then

|c_{p}^{(i)} (T + Π) − [c_{p}^{(i)} (T) + Π]| ≤ \frac{ρ}{2} |Π|

where A_{p}^{(i)} (T) = T + C_{p}^{(i)}

3. If the clock synchronization conditions S1 and S2 hold for i, processors p and q are nonfaulty through period i + 1, and T ∈ S^{(i)}, then

|c_{p}^{(i)} (T + Δ_{q p}^{(i)}) − c_{q}^{(i)} (T)| < ϵ + ρS

CAV&CADE 1996 13 of 43

Lemmas (continued)

4. If the clock synchronization conditions S1 and S2 hold for i, processors p and q are nonfaulty through period i + 1, r is nonfaulty through period i, and T ∈ S^{(i)}, then

|c_{p}^{(i)} (T) + Δ̄_{r p}^{(i)} − [c_{q}^{(i)} (T) + Δ̄_{r q}^{(i)} ]| < 2(ϵ + ρS) + ρΔ

5. If the clock synchronization condition S1 holds for i, processors p and q are nonfaulty through period i + 1, and T ∈ S^{(i)}, then

|c_{p}^{(i)} (T) + Δ̄_{r p}^{(i)} − [c_{q}^{(i)} (T) + Δ̄_{r q}^{(i)} ]| < δ + 2Δ

6. If processors p and q are nonfaulty through period i + 1, and T ∈ R^{(i+1)} , then

|c_{p}^{(i+1)} (T) − c_{q}^{(i+1)} (T)|

≤ |c_{p}^{(i)} (T^{(i+1)} ) + Δ_{p}^{(i)} − [c_{q}^{(i)} (T^{(i+1)} ) + Δ_{q}^{(i)} ]| + ρ(R + Σ)

CAV&CADE 1996 14 of 43

Example Proof (Lemma 5)

Using the arithmetic identity

(a + x) − (b + y) = (a − b) + (x − y),

we obtain

|c_{p}^{(i)} (T) + Δ̄_{r p}^{(i)} − [c_{q}^{(i)} (T) + Δ̄_{r q}^{(i)} ]|
= |c_{p}^{(i)} (T) − c_{q}^{(i)} (T) + Δ̄_{r p}^{(i)} − Δ̄_{r q}^{(i)} |
≤ |c_{p}^{(i)} (T) − c_{q}^{(i)} (T)| + |Δ̄_{r p}^{(i)} | + |Δ̄_{r q}^{(i)} |

The result follows on applying S1 to the first term on the right hand side, and observing that the Algorithm ensures that the remaining two terms are no larger than Δ

Main Theorem

Lemma 6 gives

|c_{p}^{(i+1)} (T) − c_{q}^{(i+1)} (T)|
≤ |c_{p}^{(i)} (T^{(i+1)} ) + Δ_{p}^{(i)} − [c_{q}^{(i)} (T^{(i+1)} ) + Δ_{q}^{(i)} ]|  + ρ(R + Σ)

By the Algorithm, the right hand side equals

|(\frac{1}{n}) n ; ∑ ; r=1 (c_{p}^{(i)} (T^{(i+1)} ) + Δ̄_{r p}^{(i)} − [c_{q}^{(i)} (T^{(i+1)} ) + Δ̄_{r q}^{(i)} ])| + ρ(R + Σ)

≤ (\frac{1}{n}) n ; ∑ ; r=1 |c_{p}^{(i)} (T^{(i+1)} ) + Δ̄_{r p}^{(i)} − [c_{q}^{(i)} (T^{(i+1)} ) + Δ̄_{r q}^{(i)} ]| + ρ(R + Σ)
≤ (\frac{1}{n}) [(n − m)(2[ϵ + ρS] + ρΔ) + m(δ + 2Δ)]  + ρ(R + Σ)

where the first term is obtained by applying Lemma 4 to the n − m nonfaulty processors, and the second is obtained by applying Lemma 5 to the m faulty ones. The result then follows from the Constraint C6.

CAV&CADE 1996 16 of 43

Formal Verification

• Done in 1988 by von Henke and me using Ehdm (TSE, Jan 93)

• Found that 4 of the 5 lemmas in the JACM description are incorrect as stated And proof of main theorem is flawed—its induction has the form

|c_{p}^{(i)} (T) − c_{q}^{(i)} (T)| < δ implies |c_{p}^{(i+1)} (T′) − c_{q}^{(i+1)} (T′)| < ∼ δ • Repeated by Young in 1991 using Nqthm

∘ With almost all automation turned off

Capabilities Needed

• Nonlinear arithmetic with division, involving both reals and integers

• Both interpreted (e.g., | ⋆ |, c_{p}^{(i)} ) and uninterpreted (e.g., c_{p}, Δ_{q p}^{(i)}) function symbols

• Induction ∘ Main theorem is proved by induction over i ∘ Also need induction over 1 … n to justify splitting the

summation into two parts

• Not much quantifier reasoning

CAV&CADE 1996 18 of 43

Capabilities Needed (Arithmetic)

• Ubiquity of arithmetic demands some automation

• Linear arithmetic would be a good start—for example ∘ Decision procedures for Presburger arithmetic (as in HOL)

• But we have uninterpreted function symbols as well

• Better choice is a decision procedure for ground linear arithmetic (Bledsoe, Pratt, Shostak) ∘ Over both integers and reals ∘ Combined with equality over uninterpreted function symbols

• Small extensions to nonlinear case (Brooks, Sachs) are pragmatically significant (easier in SUP-INF than loop residue) ∘ Associative, commutative, distributive, cancellation laws ∘ Law of signs (minus times minus is plus)

CAV&CADE 1996 19 of 43

Capabilities Needed (First Order)

Very little nested or explicit quantification (A2 is the exception) So lemma instantiation is the main issue

• Some lemmas can be formulated as conditional rewrite rules and applied automatically ∘ Rewriting also handles definitions ∘ Needs to be integrated with decision procedures

⋆ To find matches under arithmetic

⋆ To discharge conditions

• Other lemmas can be instantiated quite effectively by simple matching heuristics (but could do better)

• Selection of lemmas left to user guidance

∘ Specific instances found automatically on basis of types

⋆ E.g., Simple vs. bounded vs. structural induction Also harder instantiations

CAV&CADE 1996 20 of 43

Capabilities Needed (Scaling)

• The combination of ground linear arithmetic, equality, arrays

i.e., f with [(x) := y](z) =^{def} if z = x then y else f(z), propositional calculus, and rewriting is enough to tackle many interesting problems

• But can get overwhelmed by scale

∘ Intermediate formulas in processor pipeline-correctness

proofs can exhaust memory, take 60 pages to print ∘ Proofs for SRT lookup table can run for three hours

• Highly optimized implementations are necessary ∘ E.g., Barrett, Jones, Levitt, and Dill’s SVC (FMCAD 96) ∘ Uses structure sharing, Davis-Putnam, C++ ∘ As a backend to PVS, provides two orders of magnitude

speedup

CAV&CADE 1996 21 of 43

Capabilities Needed (Scaling)

• Rewriting can be a bottleneck on huge formulas

• E.g., Bitvector manipulations in processor correctness proofs ∘ Can take tens of minutes ∘ Can exhaust memory, forcing user to become concerned

with how the automation works

• Conjecture that a decision procedure for a fragment of the bitvector theory would eliminate this problem

• Many techniques from the automated verification community (BMDs, QDDs) can be incorporated into theorem proving as decision procedures

CAV&CADE 1996 22 of 43

Capabilities Needed (Libraries)

• A bare specification language is only the beginning

• Most applications of formal methods require substantial investment to develop supporting theories

• Decent libraries are necessary

• Their development is difficult ∘ Design choices are critical to utility and efficiency ∘ Maintenance is a nightmare

Capabilities Needed (Interaction)

• Cannot expect to prove fairly large, hard theorems from arbitrary domains without some user guidance and interaction

• Many tools for formal methods are all interaction and no automation

∘ Focus is on interface issues

• Whereas what’s needed is a balance between automation and interaction

∘ That can shift as attention moves between easy and hard parts of a proof

Capabilities Needed (Interface)

• Interface should allow user to comprehend the big picture ∘ Where am I? ∘ Where did this subgoal come from?

• And how to proceed ∘ Formulas should be recognizable ∘ Not cluttered with extraneous information ∘ Commands should have reasonably predictable outcomes

and costs ∘ Not too many choices

Capabilities Needed (Pruning and Debugging)

• There’s more to formal methods than proving true theorems

• Want to know exactly what assumptions, lemmas were used ∘ In order to prune them, sharpen their statements ∘ Assumptions must be validated in the real world

⋆ Trivial example: Clock synchronization originally assumed all initial corrections are zero (i.e., C_{p}^{(0)} = 0)

• Many (most) conjectures are false when first proposed

∘ Need to fail quickly, return useful information

⋆ Heuristics often be ill-suited to this requirement ∘ Would like to quickly check specific instances, downscaled

(finite state) versions, simplified conjectures

CAV&CADE 1996 26 of 43

Fast Feedback: Example

• Havelund and Shankar formally verified a boundedretransmission communications protocol from Philips (FME 96)

• First “downscaled” (aggressively simplified) it to finite-state ∘ Restricted size of data structures to explicit small values ∘ Adequate for refutation, not for verification

• Checked safety properties by state exploration using Murϕ

• Then started verification of full protocol in PVS

• Desired invariant needed strengthening by additional conjuncts ∘ Plausible conjuncts found by examining failed proof state ∘ Checked with Murϕ ∘ Added to invariant without quitting proof ∘ Iterated the above—57 times!

CAV&CADE 1996 27 of 43

Capabilities Needed (Coping with Changes)

Want to use automated formal methods to support active design exploration

• Like computational fluid dynamics supports design of aerofoils

• Change assumptions, requirements, or design, rerun proof

∘ Automation should adapt gracefully to small changes ∘ Pinpoint major deviations, and allow local “patching”

• E.g., can significantly tighten bound on clock synchronization by using observation (due to Palumbo and Graham) that there is no error when reading own clock

Active Design Exploration: Simple Example

Extension of clock synchronization algorithm to hybrid fault model (PODC ’94)

• Two additional cases in Lemma 5.

• Generalize splitting of summation from two to several parts

• More complicated constraints and assumptions

• About a week’s work (cf. 2–3 months for original)

• Discovered previously verified version of Lemma 4 needs to be strengthened

• Inconceivable to do this without automation

∘ True of most algorithms for hybrid fault model—too much case analysis to tackle unaided (e.g., bug in a published algorithm)

CAV&CADE 1996 29 of 43

Active Design Exploration: Larger Example

• There are dozens of clock synchronization algorithms

• Schneider showed many of them can be given a uniform treatment

• Shankar formally verified this general treatment (FTRTFT 92)

∘ Establishes correctness of all algorithms in a certain class

satisfying 11 assumptions ∘ Found and corrected several small errors during verification ∘ And showed interactive convergence satisfies the

assumptions

• Paul Miner argued that one of the assumptions is very difficult to establish of a given algorithm ∘ Almost as hard as proving synchronization

CAV&CADE 1996 30 of 43

Active Design Exploration: Larger Example (ctd. 1)

• Miner showed troubling assumption could be discharged once and for all from suitably modified versions of the other ten

• And showed these are satisfied by the Lundelius-Lynch algorithm

∘ Fault-tolerant midpoint: read the other clocks, exclude m slowest and m fastest, and set own clock to mid-point of remainder

• Then built a circuit to do it

• Incorporating a clever optimization due to Torres-Pomales

∘ Run own clock at half speed after seeing m + 1’st clock, until see n − m’th

CAV&CADE 1996 31 of 43

Active Design Exploration: Larger Example (ctd. 2)

Formal methods applied to the optimized clock synchronization circuit (DCC 96)

• DDD (stream-based transformation system for hardware) used for routine design

• BDD-based tautology checker used for low-level optimizations

• PVS used for the clock-rate optimization

∘ Needs fairly heavy arithmetic, again

∘ Connection to DDD via streams

(formalized as a co-inductive type) ∘ Optimization verified as a bisimulation on streams

The Theorem Proving Lifecycle

There is a lifecycle to theorem proving during formal development Need different capabilities for each stage

• Exploration: must fail quickly, be able to stay in the loop Specialized methods are very useful ∘ Animation (direct execution/simulation) ∘ State exploration (reachability analysis) ∘ “Backwards execution” (fault-tree analysis) ∘ Efficient methods for specialized cases (model checking)

• Development: efficiency!

Plus ability to comprehend overall structure

• Presentation: want a real proof

• Maintenance and Generalization: robustness

CAV&CADE 1996 33 of 43

Capabilities Required (Tool and Method Integration)

• Already described how Murϕ (state exploration) and DDD (transformation) have been used together with theorem proving

• Need to make use of other specialized methods, and integrate them more closely

• Example: finite-state model checking ∘ Real system of interest is usually infinite state ∘ Conventionally, downscale or abstract to finite state by hand ∘ Then model check the reduced system ∘ Design exploration performed on reduced system

• Theorem proving could justify and automate the reduction ∘ Model checking eliminates need for invariants (hmm…)

Tool and Method Integration: Model Checking

• Need to be able to describe a temporal logic, its models, and satisfaction relation in the logic of the theorem prover

• Model checker is then a decision procedure for a finite-state fragment

• Example: CTL, transition relations, and the satisfaction relation between them can be specified in PVS in terms of Park’s μ-calculus (QBL with least and greatest fixed points)

∘ EX (N, f)(u) : bool = ∃v : (f(v) ∧ N(u, v)) ∘ EG (N, f)(u) : bool = ν(λQ : (f ∧ EX (N, Q)))

• A BDD-based validity checker for the Boolean fragment of Park’s μ-calculus is available as a backend to PVS

• Combination provides CTL model checking on finite-state systems

CAV&CADE 1996 35 of 43

Tool and Method Integration: Example

• Havelund and Shankar abstracted bounded-retransmisison protocol to finite-state

∘ E.g., untransmitted portion of file is chosen from the

uninterpreted enumeration NONE, ONE, and MANY ∘ Cf. downscaled version: file is 1, 2, or 3 messages long

• Model-checked the abstracted protocol using the μ-calculus embedding

• Verified by theorem proving that abstraction preserved properties of interest

∘ But needed 45 invariants to establish this

• Need to integrate with additional tools for generating abstractions and invariants

Tool and Method Integration: Another Example

• N-process mutual exclusion can be recursively reduced to two-way ∘ Abstract first N − 1 processes to a single process ∘ Establish mutual exclusion between that and N’th process

• Proof by abstraction plus induction ∘ With the inductive step established by model checking

• Additional possibilities: use data structures from model checking, with node-equivalence decided by deduction rather than eq-test ∘ Seen, to some extent, in SVC and Queue BDDs

CAV&CADE 1996 37 of 43

Capabilities Needed (Language)

• Formal methodists want to use a specification language, not a bare logic ∘ Rich typing discipline ∘ Computer science data types (numbers, lists, trees) ∘ Attractive syntax ∘ Special notations—e.g., tables

• But they make choices inimical to efficient automation ∘ Set theory ∘ Functions are partial ∘ No definitional constructs

• Need more engagement between the two communities to develop specification languages that allow efficient automated deduction

CAV&CADE 1996 38 of 43

The Three Traditions

[figure: Early; Systems; Integrated; Verification; Systems; Theorem; Provers; Specification; Notations; Theorem Proving Effectiveness; s; s; e; n; e; v; i; s; s; e; r; p; x; E; Systems; Really Useful]

And A Fourth

[figure: State; Exploration; Systems]

Reconciling the Conflicts

• You cannot design a specification language and then hope to add effective mechanization

• And you cannot build a theorem prover and hope to persuade very many people that its logic is a specification language

• The formal method, its specification language, and its tools have to be designed together ∘ Tradeoffs and compromises are necessary ∘ But new opportunities arise, too

Summary

• Automated deduction and automated verification provide many techniques that are impressively effective ∘ When applied to suitable problems

• Few applications of formal methods coincide exactly with these problems

• The need is for integrated systems that bring several techniques together ∘ Integration needs to be tight ∘ Requires major system-building effort

• And the integration needs to be extended through the design

of the specification language

CAV&CADE 1996 42 of 43

The Opportunity

• Successful application of automated deduction to formal methods will enrich both fields ∘ New opportunities for research and use of automated

deduction ∘ Make formal methods a truly useful and practical tool

• Tools are not the most important thing about formal methods ∘ They are the only important thing