Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Construction of Abstract State Graphs with PVS

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. 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.
Liste complète des métadonnées

https://hal.univ-grenoble-alpes.fr/hal-01974178
Contributeur : Susanne Graf <>
Soumis le : mardi 8 janvier 2019 - 16:10:49
Dernière modification le : vendredi 17 juillet 2020 - 11:48:06

Identifiants

  • HAL Id : hal-01974178, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

113