iccad08-tutorial-ALL [Compatibility Mode]

Program verification using Verrification--Connditioon geenerraationnShuvendu LahiriSoftware Reliability ResearchMicrosoft Research, Redmond5Outline From Programs to SMT formulas Straight line programs Annotations Loops and Procedures Modeeling loww-levell CC proggrrams HAVOC toolkit Challenges for scalable and automated verification6Program Correctness: Hoare Triple Hoare triple{P} S {Q}P, Q : predicates/propertyS : a prrogramm From a state satisfying P, if S executes, then either: Either S does not terminate, or S terminates in a state satisfying Q7Program verification Formula{ b.f = 5 } a.f = 5 { a.f + b.f = 10 }is valid iffSelect(f1,b) = 5 ∧ f2 = Store(f1,a,5) ⇒ Select(f2,a) + Select(f2,b) = 10is validtheory of equality: f, =theory of arithmetic: 5, 10, +theory of arrays: Select, Store• [Nelson & Oppen ’79]8Satisfiability-Modulo-Theory (SMT) Boolean satisfiability solving + theoryreasoning Ground theoriesEquality, arithmetic, Select/Store NP-cocomplletete loggics Phenomenal progress in the past few yearsYices [Dutretre&deMoura’06], Z3 [deMoura&Bjorner’07]9Simple prog. language (BoogiePL)[Leino et al.‘05] Commandsx := E evaluate E and change x to that valuehavoc x change x to an arbitrary valueasssert E if E holds, terminate; otherwise, go wrongassume E if E holds, terminate; otherwise, blockS ; T execute S, then Tgoto A or B; change point of control to block A or ...