Construction of Abstract State Graphs with PVS - Université Grenoble Alpes
Communication Dans Un Congrès Année : 1997

Construction of Abstract State Graphs with PVS

Susanne Graf
Hassen Saidi
  • Fonction : Auteur
  • PersonId : 1041331

Résumé

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. Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ1, ..., g4 l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕi or ¬ϕi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.
Fichier non déposé

Dates et versions

hal-01974178 , version 1 (08-01-2019)

Identifiants

  • HAL Id : hal-01974178 , version 1

Citer

Susanne Graf, Hassen Saidi. Construction of Abstract State Graphs with PVS. Computer Aided Verification, Jun 1997, Haifa, Israel. pp.72--83. ⟨hal-01974178⟩
100 Consultations
0 Téléchargements

Partager

More