A Dynamic Logic for Unstructured Programs with Embedded Assertions

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Mattias Ulbrich
In:Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
Verleger:Springer
Reihe:LNCS
Band:6528
Jahr:2011
Seiten:168-182
Preprint/PDF:Ulbrich2010.pdf
DOI:10.1007/978-3-642-18070-5_12

Abstract

We present a program logic for an intermediate verification programming language and provide formal definitions of its syntax and semantics. The language is unstructured, indeterministic, and has embedded assertions. A set of sound rewrite rules which allow symbolic execution of programs is given. We prove the soundness of three inference rules using invariants which can be used to deal with loops during the verification.

Anmerkung

This paper has been awarded the best student paper and presentation award.

BibTeX

@INPROCEEDINGS{Ulbrich2010,
  author = {Mattias Ulbrich},
  title = {A Dynamic Logic for Unstructured Programs with Embedded Assertions},
  booktitle = {Revised Selected Papers, International Conference on Formal Verification
	of Object-Oriented Software (FoVeOOS 2010)},
  year = {2011},
  month = jun,
  editor = {Bernhard Beckert and Claude March{\'e}},
  volume = {6528},
  series = {LNCS},
  pages = {168--182},
  publisher = {Springer},
  note = {This paper has been awarded the best student paper and presentation
	award.},
  abstract = {We present a program logic for an intermediate verification programming
	language and provide formal definitions of its syntax and semantics.
	The language is unstructured, indeterministic, and has embedded assertions.
	A set of sound rewrite rules which allow symbolic execution of programs
	is given. We prove the soundness of three inference rules using invariants
	which can be used to deal with loops during the verification.},
  doi = {10.1007/978-3-642-18070-5_12}
}