Thesis icon

Thesis

Program analysis with interpolants

Abstract:

This dissertation discusses novel techniques for interpolation-based software model checking, an approximate method which uses Craig interpolation to compute invariants of programs. Our work addresses two aspects of program analyses based on model checking: verification (the construction of correctness proofs for programs) and falsification (the detection of counterexamples that violate the specification). In Hoare's calculus, a proof of correctness comprises assertions which establish that...

Expand abstract

Actions


Access Document


Files:
Publisher copy:
10.1007/11817963_16

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Magdalen College
Role:
Author
More by this author
Division:
MPLS
Department:
Computer Science
Role:
Author

Contributors

Division:
MPLS
Department:
Computer Science
Role:
Supervisor
Publication date:
2010
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
DOI:
Language:
English
Keywords:
Subjects:
UUID:
uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6
Local pid:
ora:4227
Deposit date:
2010-10-08

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP