Sciweavers

Share
IFM
2010
Springer

Adding Change Impact Analysis to the Formal Verification of C Programs

8 years 11 months ago
Adding Change Impact Analysis to the Formal Verification of C Programs
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.
Serge Autexier, Christoph Lüth
Added 13 Feb 2011
Updated 13 Feb 2011
Type Journal
Year 2010
Where IFM
Authors Serge Autexier, Christoph Lüth
Comments (0)
books