Object-Oriented Software: Specification and Verification
K. Rustan M. Leino
Research in Software Engineering (RiSE)
Microsoft Research, Redmond, WA
part 0
International Summer School Marktoberdorf
Marktoberdorf, Germany
6 August 2008
•
Theory and techniques for building a basic
program verifier for a language with
references to dynamically allocated objects
•
A specification style and encoding thereof
Verification condition
(logical formula)
Source language
Intermediate verification language
Static program verifier (Boogie)
SMT solver (Z3)
V.C. generator
Inference engine
verification condition
“correct” or list of errors
Boogie
C
vcc
C
HAVOC
Dafny
verifier
Dafny
Bytecode
translator
MSIL
Spec# compiler
Spec#
…
terminates
diverges
goes wrong
•
State
•
Cartesian product of variables
•
Execution trace
•
Nonempty finite sequence of states
•
Infinite sequence of states
•
Nonempty finite sequence of states
followed by special error state
…
(x: int, y: int, z: bool)
•
A
command
describes a set of execution
traces
•
A command is
deterministic
if it describes
at most one
trace from every initial state
•
Spec#, sequential Java, ML, Haskell
otherwise, it is
nondeterministic
•
C, Modula-3, Erlang, Occam
•
A command is
total
if it describes
at least one
trace from every initial state
•
Dijkstra’s
Law of the Excluded Miracle
otherwise, it is
partial
•
Juno-2, LIM, Boogie
Note, example languages do not necessarily fall squarely into the shown category.
•
x := E
•
x := x + 1
•
x := 10
•
havoc
x
•
assert
P
•
assume
P
P
¬
P
P
Dotted lines indicate traces whose length may be greater than 1
Solid lines indicate traces whose length is 1
…
•
x := E
•
x := x + 1
•
x := 10
•
havoc
x
•
S ; T
•
assert
P
•
assume
P
P
¬
P
P
…
Dotted lines indicate traces whose length may be greater than 1
Solid lines indicate traces whose length is 1
•
x := E
•
x := x + 1
•
x := 10
•
havoc
x
•
S ; T
•
assert
P
•
assume
P
•
S
T
P
¬
P
P
…
Dotted lines indicate traces whose length may be greater than 1
Solid lines indicate traces whose length is 1
© 2007 Microsoft Corporation. All rights reserved. Microsoft, Windows, Windows Vista and other product names are or may be registered trademarks and/or trademarks in the U.S. and/or other countries.
The information herein is for informational purposes only and represents the current view of Microsoft Corporation as of the date of this presentation. Because Microsoft must respond to changing market conditions, it should not be interpreted to be a commitment on the part of Microsoft, and Microsoft cannot guarantee the accuracy of any information provided after the date of this presentation.
MICROSOFT MAKES NO WARRANTIES, EXPRESS, IMPLIED OR STATUTORY, AS TO THE INFORMATION IN THIS PRESENTATION.
This resource delves into theory, techniques, and architectures for verifying object-oriented software, focusing on a basic program verifier for dynamically allocated objects. It covers specification styles, verification conditions, modeling execution traces, states, and commands in a variety of languages like Spec#, Java, ML, Haskell, and more. The content explores verification architectures using tools like Dafny, Boogie, and SMT solvers, emphasizing correctness and error detection.
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
Specification and Verification of Object-Oriented Software K. Rustan M. Leino Research in Software Engineering (RiSE) Microsoft Research, Redmond, WA part 0 International Summer School Marktoberdorf Marktoberdorf, Germany 6 August 2008
Contents Theory and techniques for building a basic program verifier for a language with references to dynamically allocated objects A specification style and encoding thereof
Basic verifier architecture Source language Intermediate verification language Verification condition (logical formula)
Verification architecture Spec# Dafny C C Spec# compiler Dafny verifier HAVOC vcc MSIL Bytecode translator Static program verifier (Boogie) Inference engine Boogie V.C. generator verification condition SMT solver (Z3) correct or list of errors
Modeling execution traces terminates diverges goes wrong
States and execution traces State Cartesian product of variables Execution trace Nonempty finite sequence of states Infinite sequence of states Nonempty finite sequence of states followed by special error state (x: int, y: int, z: bool)
Commands A command describes a set of execution traces A command is deterministic if it describes at most one trace from every initial state Spec#, sequential Java, ML, Haskell otherwise, it is nondeterministic C, Modula-3, Erlang, Occam A command is total if it describes at least one trace from every initial state Dijkstra sLaw of the Excluded Miracle otherwise, it is partial Juno-2, LIM, Boogie Note, example languages do not necessarily fall squarely into the shown category.
Command language x := E x := x + 1 assert P P P assume P x := 10 P havoc x Solid lines indicate traces whose length is 1 Dotted lines indicate traces whose length may be greater than 1
Command language x := E x := x + 1 assert P P P assume P x := 10 P havoc x S ; T Solid lines indicate traces whose length is 1 Dotted lines indicate traces whose length may be greater than 1
Command language x := E x := x + 1 assert P P P assume P x := 10 P havoc x S T S ; T Solid lines indicate traces whose length is 1 Dotted lines indicate traces whose length may be greater than 1
