Formal Verification of Large Software SystemsWe introduce a scalable proof structure to facilitate formal verification of large software systems. In our approach, we mechanically synthesize an abstract specification from the software implementation, match its static operational structure to that of the original specification, and organize the proof as the conjunction of a series of lemmas about the specification structure. By setting up a different lemma for each distinct element and proving each lemma independently, we obtain the important benefit that the proof scales easily for large systems. We present details of the approach and an illustration of its application on a challenge problem from the security domain
Document ID
20100018552
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Yin, Xiang (Virginia Univ. Charlottesville, VA, United States)
Knight, John (Virginia Univ. Charlottesville, VA, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium