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) 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.

Projekte

final-version.pdf (pdf, 345 KB)

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