@inproceedings{GS97,
title = { Construction of abstract state graphs with {PVS} },
author = {Graf, Susanne and Saidi, Hassen},
month = {jun},
year = {1997},
booktitle = {Conference on Computer Aided Verification CAV'97, Haifa},
series = {LNCS},
volume = {1254},
team = {DCS},
abstract = {In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover, called predicate abstraction. Given a parallel composition of sequential processes and predicates <i>P1 ... Pn</i> on the program variables defining an abstract domain, we construct an abstract state graph, starting in the state defined by the values of the predicates <i>P1 ... Pn</i> in the initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each <i>i</i> if <i>Pi</i> or <i>not Pi</i> is a postcondition of it. This allows an abstract state space exploration for arbitrary programs. Using this method, we have automatically verified a bounded retransmission protocol which cannot be proved using backward analysis without providing strong auxiliary invariants. },
}
