Home | deutsch  | Legals | Sitemap | KIT

A Dynamic Logic for Unstructured Programs with Embedded Assertions

A Dynamic Logic for Unstructured Programs with Embedded Assertions
Author(s):

Mattias Ulbrich

Links:
Source:

International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011

Date: June 2010

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.

Award

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},
editor = {Bernhard Beckert and Claude March{\'e}},
booktitle = {Revised Selected Papers, International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS 2010)},
volume = {6528},
series = {LNCS},
pages = {168--182},
publisher = {Springer},
year = {2011}
}