1、Synthesis and Verification Formal and Semi-Formal Verification,Contract #: TJ-684,October 14, 2018,2,Accomplishments!,Yuan Lu (now at BroadComm Inc.) and Marius Minea (now PostDoc at Berkeley) graduated in the year 2000!,Automatic Abstraction by Counterexample-guided Refinement,Edmund M. Clarke Yuan
2、 Lu Pankaj Chauhan Anubhav GuptaJoint work with Orna Grumberg, Somesh Jha, Helmut Veith,684.004: Abstraction in Model Checking,Description: Counterexample-guided Abstraction Refinement Goals: To provide a new abstraction technique to verify large designs.,October 14, 2018,4,684.004: Abstraction in M
3、odel Checking,Plans and directions for the current year (2000): Experiment with other abstraction refinement techniques Experiment on benchmark and industrial designs Abstraction in the context of bounded model checking Experiment on industrial designs (PCI bus protocol),October 14, 2018,5,October 1
4、4, 2018,6,684.004: Abstraction in Model Checking,Accomplishments for the current year (2000): Yuan Lu graduated! Automatic abstraction generation Release of aSMV tool Extensive experimentation with impressive results,684.004: Abstraction in Model Checking,Plans and directions for the next year (2001
5、): Extending the methodology to include all ACTL countertexamples Using SAT for refinement of large state spaces,October 14, 2018,7,684.004: Abstraction in Model Checking Milestones,Automatic abstraction function generation (31-Dec-2000) Development of hierarchical verification algorithms (31-Dec-20
6、00) Extending the methodology to include all ACTL* counterexamples and implementation (31-Dec-2001) Using SAT based techniques for refinement of large state spaces (31-March-2001),October 14, 2018,8,684.004: Abstraction in Model Checking Deliverables,Report on hierarchical model checking without fla
7、ttening for hierarchical circuit descriptions (Planned 31-Dec-2000) Report on model checking of hierarchically structured SMV and StateCharts for embedded systems and mixed hardware designs (Planned 31-Dec-2001) Report/Paper on Extension of methodology for all counterexamples (Planned 31-Dec-2001) N
8、ew version of aSMV with this feature (Planned 30-March-2001) Report/Paper on refinement using large state spaces (Planned 31-June-2001) New version of aSMV with SAT based refinement (Planned 31-Dec-2002),October 14, 2018,9,October 14, 2018,10,Existential Abstraction,M,Mh,Given an abstraction functio
9、n h : S Sh, the concrete states are grouped and mapped into abstract states,M Mh and Mh |= M |= ,October 14, 2018,11,Our Abstraction Methodology (CAV2000),October 14, 2018,12,Highlights of Our Methodology,Impressive results, on average, 3.5x time, 17x space improvements! A large Fujitsu multimedia p
10、rocessor verified Handles all ACTL* loop/path counterexample But. What about non-loop/non-path counterexamples? What if infeasible to check validity of counterexamples?,October 14, 2018,13,General Counterexamples for ACTL*,Not all the counterexamples in ACTL* are linear (path or loop).How to refine
11、the abstraction when a counterexample is not linear?What are counterexamples?How to generate “readable” counterexamples?,October 14, 2018,14,Tree-like Counterexamples,What does the counterexample for (AG p) (AF q) look like?(AG p) (AF q), (EF p) (EG q),October 14, 2018,15,Counterexamples for ACTL,Th
12、eorem All ACTL formulas have tree-like counterexamples.Why tree-like counterexamples ?easy to diagnosedecomposable to simple paths and loops,October 14, 2018,16,Generate Counterexamples for ACTL,We propose an algorithm to generate tree-like counterexamples for ACTLTraverse the parse tree of the form
13、ula in DFS orderGenerate path or loop counterexamples for each node in the parse tree.Glue all the sub-counterexamples for the total,Symbolic!,October 14, 2018,17,Using SAT for Abstraction Refinement,Problem Domain: Hardware circuits with more than 5000 latches! Path/loop counterexamples onlyI : Pri
14、mary Inputs R: Visible Variables A: Invisible Variables V = R U A |R| |V|,C,L,I,R,R,A,A,October 14, 2018,18,Spurious Path Counterexample,Th is spurious,The concrete states mapped to the failure state are partitioned into 3 sets,October 14, 2018,19,Checking the Validity of Counterexample,Describe the
15、 abstract counterexample using propositional formulaFeed the formula to SAT checker Size of SAT problem is linear in the circuit size For a spurious trace, dead end states Si,0 are obtained Set of dad states is could be empty,October 14, 2018,20,Example of Approximation,October 14, 2018,21,Modified
16、Refinement Methodology,October 14, 2018,22,Heuristics for Refinement,Use GRASP (Sakellah et. al.)/Chaff(Mallik et.al.) for checking validity of counterexample Modify these procedures to identify important variables Most backtracked to variable Largest transitive fanout in implication graph(IG) Uniqu
17、e Implication Points Variables from conflicting clauses ,October 14, 2018,23,Implementation Details,visible boolean x; ,Modified NuSMV,Intermediate Block,Modified GRASP/Chaff,Mh|= ,New vars,Th, M,Th, M, Bad, DeadEnd,Sat?, Auxiliary Info,October 14, 2018,24,Future Work,Generate non-path/non-loop coun
18、terexamples Refinement using those counterexamples Formalize and evaluate the heuristics for picking up visible variables using GRASP/Chaff Experiments!,Model Checking and Theorem Proving: A Unified Framework,Sergey Berezin Edmund M. Clarke,October 14, 2018,26,684.005: Combining Model Checking with
19、Theorem Proving,Description: An approach to unifying Model Checking and Theorem Proving in a single framework Goals: Design a framework to combine new state-of-the-art model checking and theorem proving techniques efficiently Develop a tool that supports this framework,October 14, 2018,27,684.005: C
20、ombining Model Checking with Theorem Proving,Plans and directions for the current year (2000):Verify a large hardware example (like PCI bus) Study how the combination of model checking and theorem proving improves both techniques Continue the development of the implementation,October 14, 2018,28,684
21、.005: Combining Model Checking with Theorem Proving,Accomplishments for the current year (2000): Formulated a framework that unifies model checking and theorem proving in a very general way Came up with a new methodology for efficient specialization of theorem proving to particular problem domains I
22、mplemented a “prover generator“ as a new version of SyMP based on the above methodology Implemented the necessary components of the proof system for combining model checking and theorem proving as an instance of a prover generated by SyMP Verified an example of an IBM cache coherence protocol,Octobe
23、r 14, 2018,29,684.005: Combining Model Checking with Theorem Proving,Plans and directions for the next year (2001): Include several powerful reduction rules into the default proof-system of SyMP (like various forms of abstraction, compositional reasoning techniques, etc.) Verify a few more examples
24、using these reduction rulesImplement one or more other proof systems (either completely different or specialized and more automated versions of the default system) in the tool and demonstrate that it works as a prover generator,October 14, 2018,30,684.005: Combining Model Checking with Theorem Provi
25、ng Milestones,Implementation of the tools core, detailed tool design, preliminary experiments on known hardware examples like Tomasulos algorithm (30-Sep-1999) Experimental alpha release of the tool (31-Dec-1999) Extensions to the verification methodology and experiments on larger examples (30-Jun-2
26、000) Extensions to the theorem prover and the model checking back-end (30-Jun-2001),October 14, 2018,31,684.005: Combining Model Checking with Theorem Proving Deliverables,Prototype of the tool for combining model checking and theorem proving (Completed: 16-Feb-2000), Related Publication(s):P000258
27、, P000259 Release of tool for combining model checking and theorem proving (Completed: 10-Jan-2001), P001813 Doctoral dissertation on combining model checking and theorem proving for hardware verification (Planned: 30-Aug-2001) Report on verification methodology for complex hardware using model chec
28、king and theorem proving (Planned: 31-Dec-2001),Model Checking and Theorem Proving: A Unified Framework,Sergey Berezin Computer Science Department Carnegie Mellon University,October 14, 2018,33,Example: IBM Cache Coherence Protocol,Cache1,Home Node,Cache2,Cachen,.,Shared:,P1,Pn,P2,ExclGranted:,.,Sha
29、red,reqExcl,grantExcl,invalidate,invAck,Excl,reqShared,grantShared,Cachen,October 14, 2018,34,Coherence Property,At any point in time,if any cache is Exclusivethen all the other caches are Invalid: AG c1,c2: c1 != c2 & c1.state = Exclusive c2.state = Invalid,October 14, 2018,35,Coding the Model in S
30、yMP,module Mtype Index = begindatatype State = Invalid | Shared | ExclstateVar (cache: Index - State), (channel: Index - Message),(exclGranted: bool), (Shared: Index - bool)init(cache) := fn _ = Invalid;init(exclGranted) := falsechoose i:channel(i) = Invalidate = next(cache) := (fn x = if x=i then I
31、nvalid else cache x endif)| !exclGranted & channel(i) = reqExcl =next(channel i) := grantExclnext(exclGranted) := trueendchoosetheorem coherence = self |= AG(forall i,j: i!=j & cache(i) = Excl - cache(j) = Invalid) end,October 14, 2018,36,Formal Verification Options,Both have strong and weak points.
32、,Can we combine best features of the two?,October 14, 2018,37,Combining MC & TP,Add expressiveness to efficient decision procedures Cancel out drawbacks of both techniques Perhaps, find something new in the middle ground.,October 14, 2018,38,Modifying Gentzens Sequent,Theorem proving uses Gentzens S
33、equent format:,A1, A2, = B1, B2, ,The model from model checking has to be translated into HOL to fit into this sequent. But we can add the model to the sequent:,M; A1, A2, = B1, B2, ,Also, make the logic temporal, not just HOL.,October 14, 2018,39,Adding Model Checking,Model checking becomes just an
34、other rule:,Other transformations from model checking are added as rules, e.g. Cone of Influence reduction:,October 14, 2018,40,Other Types of Rules,Induction on time:,October 14, 2018,41,Verifying Cache Coherence,Property in First-Order CTL:AG(c1,c2: c1 != c2 & c1.state = Exclusive c2.state = Inval
35、id) How to prove: Find an inductive invariant Induction on time (the AG Induct rule) Skolemize, split choose statement, abstract-split (eliminate skolem constants), compute cone of influence, model check Verified in our tool SyMP,October 14, 2018,42,New Methodology: Features,Adequate representation
36、for the problem domain Right level of abstraction Rules perform exactly the transformations we have in mind while doing verification Specialized rules for temporal logic Efficient use of model structure Model checking and theorem proving at the same prompt Interactive proof construction Full user co
37、ntrol with possibility of automation,October 14, 2018,43,Overall Picture,Specification language,User Interface,October 14, 2018,44,Generalizing Further,What made it possible to integrate Model Checking and Theorem Proving? Customized sequent and proof system Adequate representation for the problem d
38、omain How about other problem domains? (Security protocols, Software verification, highly specialized hardware, etc.) The same guidelines should work (*) But do I have to code it all from scratch again? There is certainly some common core that can be reused,October 14, 2018,45,Architecture with Shar
39、ed Core,October 14, 2018,46,SyMP: Symbolic Model Prover,“Theorem prover generator” Common proof management core Common interactive user interface Plug-in proof systems well-defined interface to custom proof system modules Each proof system defines custom sequent and custom set of rules Currently imp
40、lemented proof systems: Default: combines MC & TP Athena: security protocol verification (in progress),October 14, 2018,47,Verified Example: IBM Cache Coherence,Coded in Default proof system in SyMP Verified coherence of the Home Node Other lemmas are still in progress Proof: 139 elementary steps (p
41、roof rules) about half of them are model check rules,October 14, 2018,48,Conclusion,New methodology for combining model checking and theorem proving New framework for specializing theorem proving to various problem domains In particular, MC + TP is one such problem domain A tool SyMP that implements
42、 the framework Implementation of MC + TP system in the tool Many existing methodologies can be expressed in the framework and implemented in SyMP,October 14, 2018,49,Future Work,Finish the default proof system Ideally, it should include all basic theorem proving for FO temporal logic and most of kno
43、wn model checking transformations Implement more proof systems for other problem domains Athena is being implemented for security protocols Plans for software verification system Plans for toy systems: natural deduction, CFG, etc. Improve proof search techniques,Using Fourier Analysis for Abstractio
44、n-Refinement in Model Checking,Anubhav Gupta Edmund M. Clarke,October 14, 2018,51,684.007: Model Checking Without BDDs,Description: Symbolic model checking without BDDs using alternative data structures and algorithms.Goals: To develop an alternative method of doing model checking without BDDs.,Octo
45、ber 14, 2018,52,684.007: Model Checking Without BDDs,Plans and directions for the current year (2000):Explore the use of SAT procedures and BEDs for fixpoint computations.,October 14, 2018,53,684.007: Model Checking Without BDDs,Accomplishments for the current year (2000): Implemented a full CTL mod
46、el checker that combines SAT procedures with BEDs for fixpoint computations. Proposed a new methodology that uses “learning algorithms” for identifying important variables in hardware circuits. Came up with a new approach for counterexample-guided abstraction-refinement that views refinement as the
47、standard “AI classification problem”.,October 14, 2018,54,684.007: Model Checking Without BDDs,Plans and directions for the next year (2001): Implement a tool that identifies important variables in a circuit and uses this information to generate good BDD and SAT-split orderings. Formalize a countere
48、xample-guided abstraction-refinement framework based on the Fourier Transform. Implement a counterexample-guided abstraction-refinement framework based on the Fourier Transform and other learning algorithms.,October 14, 2018,55,684.007: Model Checking Without BDDs Milestones,Verifier that combines f
49、ixed point computation for mode checking with a sat-solver (31-Jan-2001). Formalize counterexample-guided abstraction-refinement framework based on the Fourier Transform (15-May-2001). Implement counterexample-guided abstraction-refinement framework based on the Fourier Transform and other learning algorithms and perform experiments (31-Nov-2001). Generates good BDD and SAT splitting-orders based on important variables in the circuit (31-Mar-2002).,
