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...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery
2010
|
| Online Access: | http://hdl.handle.net/1721.1/51822 https://orcid.org/0000-0001-8095-8523 |