Overview of Program Verification Tools and Techniques
Explore the pillars of program verification, early mechanical verification systems, software quality assurance, and a spectrum of verification tools used for ensuring functional correctness, safety-critical systems, and more. Discover the role of proof assistants and automatic decision procedures in discharging verification conditions effectively.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Understanding Program Verification K. Rustan M. Leino RiSE, Microsoft Research, Redmond PROLE 2009 09/09/2009 San Sebastian, Spain
Software quality assurance A major software engineering concern Costly Relies heavily on testing Increasingly helped by advanced tools Verification-condition generation, symbolic execution, model checking, abstract interpretation, fuzzing, test generation
Spectrum of verification tools Functional correctness Safety-critical systems Algorithms Important libraries Bug finding Common run-time errors Device-driver protocols Concurrency errors lock usage in Windows programs (HAVOC) Examples Praxis customers (Spark Ada) IEEE 1384 protocol (Event-B) Microsoft Hypervisor (VCC) Compiler front-end (ESC/Java) Windows drivers (SLAM)
Pillars of program verification Floyd, 1967 0 n = N s := 1 0 n N s * n! = N! The most general P that satisfies Hoare, 1969 {P} S {Q} 0 < n N s * n! = N! 0 < n? { P } S { Q } s = N! { P } S { Q } is called the weakest precondition of S w.r.t. Q: wp(S, Q) s := s * n 0 < n N s * (n-1)! = N! Dijkstra, 1976 P wp(S, Q) logic formula Executions of S that start in P: do not go wrong, and terminate in Q n := n - 1
Early mechanical verification systems Gypsy Stanford Pascal Verifier
Verification-condition generation Program + specifications Verification condition (logical formula) How to discharge verification condition? Proof assistant ACL2, Coq, Isabelle/HOL, PVS, support for complicated math, higher-order functions Automatic decision procedures SMT solvers like CVC3, Simplify, Z3, program structure gives strong proof hint
Mechanical tool support Proof assistants User interacts at level of prover Automatic program verifiers User interacts at level of program Demos Classic interface Chalice: dining philosophers Integrated interaction Spec#: numeros de telefono, busqueda binaria
Specification language Terms of a logic ESC/Modula-3, KeY, PROCEDURE M(x: MyClass) = BEGIN END M; <*SPEC M(x) REQUIRES 0 <= MyClass.f[ x ] *> Terms are program expressions Eiffel, JML, Spec#, feature M(x: MyClass) is require 0 <= x.f do end //@ requires 0 <= x.f; void M(MyClass x) { } void M(MyClass x) requires 0 <= x.f; { }
Basic verifier architecture Source language Intermediate verification language Verification condition (logical formula)
Boogie a verification tool bus [Barnett, Jacobs, Leino, Moskal, R mmer, et al.] C with HAVOC specifications C with VCC specifications Spec# Dafny Chalice Boogie Isabelle/ HOL Simplify Z3 SMT Lib
Example translation Source language: p.f = x / y; Boogie: assert p null; assert y 0; Heap[p,f] := x / y; Verification condition: (AND (NEQ p null) (NEQ y 0) (IMPLIES (EQ Heap (store Heap p f (/ x y))) TRUE))
Example translation Source language: p.f = x / y; Boogie: assert p null; assert y 0; Heap[p,f] := x / y; Verification condition: (AND (NEQ p null) (NEQ y 0) (IMPLIES (EQ Heap (store Heap p f (/ x y))) TRUE))
Abstraction How to specify the effect of method Play? :RockBand methodPlay() :Organ :Guitar methodStrum() :Drums methodGrind() methodBang() :GtString :GtString :DrawBar :Kick :Snare
Specification style Demo Spec# (ownership) Dafny (dynamic frames)
Specification style summary Spec# handles common cases easily does not support all useful programming idioms somewhat opaque Dafny flexible, transparent primitive, verbose What is a flexible/transparent/frugal specification language?
When things verify Modular verification goes a long way Re-doing or re-playing proofs can be done off-line
When things do not verify Quick turnaround is key For beginners and experts alike Example: Hypervisor verification Want: sub-second response Understanding complaints
Explaining errors visually [joint work with Claire Le Goues] source program program *5 {boolType} *6 {ClassNameType} *7 {$tokenType} *8 {cf_eventType} *9 {var_locglobType} *10 {refType} *11 {class.int} *12 {class.bool} *13 {class.object} *14 {class.set} *15 {class.seq} *16 {#loc.$Heap} *17 {alloc} *18 {conditional_moment} *19 {took_then_branch} *20 {took_else_branch} *21 {loop_register} *22 {loop_entered} *23 {loop_exited} *24 {cev_local} *25 {cev_global} *26 {cev_parameter} *27 {cev_implicit} partitions: *0 -> true *1 -> false FieldType -> { *5 -> *51 *4 -> *52 *10 -> *53 MapType1Type -> { *10 -> *54 else -> #unspecified intermediate else -> #unspecified } FieldTypeInv0 -> { *51 -> *5 *52 -> *4 *53 -> *10 else -> #unspecified } DeclType -> { *29 -> *28 *30 -> *28 else -> #unspecified } $file_name_is -> { *43 *31 -> *0 else -> #unspecified } MapType1Type -> { *10 -> *54 else -> #unspecified } MapType1TypeInv0 -> { *54 -> *10 else -> #unspecified } formula verifier *2 {@true} -> 8:int *3 {@false} -> 9:int *4 {intType} Boogie } MapType1TypeInv0 -> { *54 -> *10 else -> #unspecified } $IsGoodHeap -> { *40 -> *0 *42 -> *0 *39 -> *0 else -> #unspecified } U_2_bool -> { *56 -> *0 else -> #unspecified } MapType1Select -> { *40 *41 *17 -> *56 *40 *41 *30 -> *38 *39 *41 *30 -> *41 *42 *41 *30 -> *38 *42 *41 *17 -> *56 *39 *41 *17 -> *56 else -> #unspecified } dtype -> { *41 -> *28 Z3 counterexample model model tool demo square insert
Verified Software Initiative Hoare, Joshi, Leavens, Misra, Naumann, Shankar, Woodcock, et al. We envision a world in which computer programs are always the most reliable component of any system or device that contains them [Hoare & Misra]
Next steps Continue to: improve program-verification technology do experiments and pay more attention to tool usage: Rapid-response analysis Explanation tools Ceaselessly-analyzing programming environments
Some URLs Boogie, Dafny, Chalice available as open source: http://boogie.codeplex.com Spec# and VCC also available as open source under academic license: http://specsharp.codeplex.com http://vcc.codeplex.com Some papers: http://research.microsoft.com/~leino
