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...
| Päätekijät: | , , |
|---|---|
| Muut tekijät: | |
| 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 |