Runtime Checking for Program Verification

The process of verifying that a program conforms to its specification is often hampered by errors in both the program and the specification. A runtime checker that can evaluate formal specifications can be useful for quickly identifying such errors. This paper describes our preliminary experience with incorporating run-time checking into the Jahob verification system and discusses some lessons we learned in this process. One of the challenges in building a runtime checker for a program verification system is that the language of invariants and assertions is designed for simplicity of semantics and tractability of proofs, and not for run-time checking. Some of the more challenging constructs include existential and universal quantification, set comprehension, specification variables, and formulas that refer to past program states. In this paper, we describe how we handle these constructs in our runtime checker, and describe directions for future work.

Citation

Karen Zee, Viktor Kuncak, Michael Taylor, and Martin Rinard. Runtime checking for program verification. In Workshop on Runtime Verification, volume 4839 of LNCS, 2007.

BibTex Entry

@inproceedings{ZeeETAL07RuntimeCheckingProgramVerification,
  author = {Karen Zee and Viktor Kuncak and Michael Taylor 
 and Martin Rinard},
  title = {Runtime Checking for Program Verification},
  booktitle = {Workshop on Runtime Verification},
  series = {LNCS},
  volume = {4839},
  year = 2007,
  abstract = {
The process of verifying that a program
conforms to its specification is often hampered by errors in
both the program and the specification.  
A runtime checker
that can evaluate formal specifications can be 
useful for quickly identifying such errors.  
This paper describes our preliminary experience with incorporating run-time checking
into the Jahob verification system and discusses 
some lessons we learned in this process.  One of the
challenges in building a runtime checker for a program
verification system is that the language of invariants and
assertions is designed for simplicity of semantics and
tractability of proofs, and not for run-time checking.  Some
of the more challenging constructs include existential and
universal quantification, set comprehension, specification
variables, and formulas that refer to past program states.
In this paper, we describe how we handle these constructs in
our runtime checker, and describe directions for
future work.
}
}