Publikation
Adding Change Impact Analysis to the Formal Verification of C Programs
Serge Autexier; Christoph Lüth
In: Dominique Méry; Stephan Merz (Hrsg.). Proceedings 8th International Conference on Integrated Formal Methods (iFM 2010). International Conference on Integrated Formal Methods (IFM-2010), October 11-14, Nancy, France, Pages 59-73, Lecture Notes in Computer Science (LNCS), Vol. 6396, Springer, 10/2010.
Zusammenfassung
Handling changes to programs and specifications efficiently is a
particular challenge in formal software verification. Change impact
analysis is an approach to this challenge where the effects of changes
made to a document (such as a program or specification)
are described in terms of rules on a semantic
representation of the document. This allows to describe and delimit the
effects of syntactic changes semantically.
This paper presents an application of generic change impact analysis to
formal software verification, using the GMOC and SAMS tools. We adapt
the GMOC tool for generic change impact analysis to the SAMS
verification framework for the formal verification of C programs, and
show how a few simple rules are sufficient to capture the essence of
change management.