Proceedings-Artikel
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, 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.