An Integrated Proof Language for Imperative Programs

We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge...

Full description

Bibliographic Details
Main Authors: Zee, Karen (Contributor), Kuncak, Viktor (Author), Rinard, Martin C. (Contributor)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Association for Computing Machinery, 2010-02-24T21:00:42Z.
Subjects:
Online Access:Get fulltext