La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

De
49 pages
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 ...
Voir plus Voir moins

Vous aimerez aussi

Shuvendu Lahiri

Software Reliability Research
Microsoft Research, Redmond
5

HAVOC toolkit

Challenges for scalable and automated verification
6

From a state satisfying P, if S executes, then either: Either S does not terminate, or S terminates in a state satisfying Q
7
Select(f1,b) = 5f2 = Store(f1,a,5)Select(f2,a) + Select(f2,b) = 10
is valid
theory of equality: f, =
theory of arithmetic: 5, 10, +
theory of arrays:
[Nelson & Oppen ’79]
Select, Store
8
-com
e
e
o
cs
Phenomenal progress in the past few years Yices [Dutretre&deMoura’06], Z3 [deMoura&Bjorner’07]
9
if E holds, terminate; otherwise, go wrong assumeE if E holds, terminate; otherwise, block S ; T execute S, then T gotoAorB; change point of control to block A or block B, choosing blindly
10
var y: int;
var a: [int] int;
start:
y := 10;
a[y] := 20;
y := a[10];
// array variable
// assignment to scalar
// sugar for a := update(a, y, 20) ;
11
Else:
After:
goto
; After
assume¬P ; [[T]]; gotoAfter
12
assumeP; S;assertQ
Task: Transform a program withassume/saestr a formula Known asVerification Condition(VC) generation
into
13
14
if it terminates, terminates in Q
15
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin