| Autor: |
VOGELS, FRÉDÉRIC, JACOBS, BART, PIESSENS, FRANK |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science (LMCS); 2015, Vol. 11 Issue 3, p1-57, 57p |
| Abstrakt: |
VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFast's operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
