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:

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author

Contributors

Role:
Supervisor
Publication date:
2010
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
URN:
uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6
Local pid:
ora:4227

Terms of use


Metrics


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