Advertisement
Published in:
2007 | OriginalPaper | Chapter
Designing Verification Conditions for Software
Author : K. Rustan M. Leino
Published in: Automated Deduction – CADE-21
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Software verification technology has the potential to improve the quality of software. The basic technique is to generate verification conditions for a given program and to discharge these proof obligations using a theorem prover. Encoding the verification conditions is a delicate process, not just because it must capture the intended programming semantics, but also because it must yield formulas that a theorem prover can process effectively.
In this talk, I will discuss the process of generating verification conditions in the program verifier for the object-oriented language Spec#. I will highlight design decisions we have made in modeling programs and targeting SMT solvers, lessons we have learned, and challenges that remain ahead.