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 Seiten 419-434 Lecture Notes in Computer Science (LNCS) 5350 Springer 2009.


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.


final-version.pdf (pdf, 345 KB)

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence