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...

Täydet tiedot

Bibliografiset tiedot
Päätekijät: Zee, Karen, Kuncak, Viktor, Rinard, Martin C.
Muut tekijät: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Aineistotyyppi: Artikkeli
Kieli:en_US
Julkaistu: Association for Computing Machinery 2010
Linkit:http://hdl.handle.net/1721.1/51822
https://orcid.org/0000-0001-8095-8523