Result: Verification of sets of infinite state processes using program transformation

Title:
Verification of sets of infinite state processes using program transformation
Authors:
FIORAVANTI, Fabio, PETTOROSSI, Alberto, PROIETTI, Maurizio
Source:
LOPSTR : logic based program synthesis and transformation (Paphos, 28-30 November 2001, selected papers)Lecture notes in computer science. :111-128
Publisher Information:
Berlin: Springer, 2002.
Publication Year:
2002
Physical Description:
print, 28 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Logique monadique, Monadic logic, Lógica monadica, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Simultanéité informatique, Concurrency, Simultaneidad informatica, Transformation programme, Program transformation, Transformación programa, Logique WS2S, Weak second order logic of two successor function, Vérification modèle, Model checking
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
IASI-CNR, Viale Manzoni 30, 00185 Roma, Italy
DISP, University of Roma Tor Vergata, 00133 Roma, Italy
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14525171
Rights:
Copyright 2003 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14525171
Database:
PASCAL Archive

Further Information

We present a method for the verification of safety properties of concurrent systems which consist of finite sets of infinite state processes. Systems and properties are specified by using constraint logic programs, and the inference engine for verifying properties is provided by a technique based on unfold/fold program transformations. We deal with properties of finite sets of processes of arbitrary cardinality, and in order to do so, we consider constraint logic programs where the constraint theory is the Weak Monadic Second Order Theory of k Successors. Our verification method consists in transforming the programs that specify the properties of interest into equivalent programs where the truth of these properties can be checked by simple inspection in constant time. We present a strategy for guiding the application of the unfold/fold rules and realizing the transformations in a semiautomatic way.