@inbook{f62b23893b7c4687849ff2e6cb80c7d7,
title = "Multi-prover verification of C programs",
abstract = "Our goal is the verification of C programs at the source code level using formal proof tools. Programs are specified using annotations such as pre- and post-conditions and global invariants. An original approach is presented which allows to formally prove that a function implementation satisfies its specification and is free of null pointer dereferencing and out-of-bounds array access. The method is not bound to a particular back-end theorem prover. A significant part of the ANSI C language is supported, including pointer arithmetic and possible pointer aliasing. We describe a prototype tool and give some experimental results.",
keywords = "C programming language, Formal verification and proof, Hoare logic, Pointer programs",
author = "Filli{\^a}tre, \{Jean Christophe\} and Claude March{\'e}",
year = "2004",
month = jan,
day = "1",
doi = "10.1007/978-3-540-30482-1\_10",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "15--29",
editor = "Jim Davies and Wolfram Schulte and Mike Barnett",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}