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. },


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4005810