Sciweavers

Share
IJFCS
2008

Reachability Analysis in Verification via Supercompilation

8 years 3 months ago
Reachability Analysis in Verification via Supercompilation
Abstract. We present an approach to verification of parameterized systems, which is based on program transformation technique known as supercompilation. In this approach the statements about safety properties of a system to be verified are translated into the statements about properties of the program that simulates and tests the system. The supercompilation is used then to establish the required properties of the program. In this paper we show that reachability analysis performed by supercompilation can be seen as the proof of a correctness condition by induction. We formulate suitable induction principles and proof strategies and illustrate their use by examples of verification of parameterized protocols.
Alexei Lisitsa, Andrei P. Nemytykh
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2008
Where IJFCS
Authors Alexei Lisitsa, Andrei P. Nemytykh
Comments (0)
books