Publication
Certifiable specification and verification of C programs
Christoph Lüth; Dennis Walter
In: FM 2009: Formal Methods. International Symposium on Formal Methods (FM-2009), November 2-6, Eindhoven, Netherlands, Pages 419-434, Lecture Notes in Computer Science (LNCS), Vol. 5350, Springer, 2009.
Abstract
A novel approach to the specification and verification of C programs
through an annotation language that is a mixture between JML and the
language of Isabelle/HOL is proposed. This yields three benefits:
specifications are concise and close to the underlying mathematical
model; existing Isabelle theories can be reused; and the leap of
faith from specification language to encoding in a logic is small.
This is of particular relevance for software certification, and
verification in application areas such as robotics.