@InProceedings{   10.5555/646920.709171,
  Author        = "Fioravanti, Fabio and Pettorossi, Alberto and Proietti, Maurizio",
  Abstract      = "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.",
  Address       = "Berlin, Heidelberg",
  BookTitle     = "Selected Papers from the 11th International Workshop on Logic Based Program Synthesis and Transformation",
  date-added    = "2021-03-10 15:54:26 +0100",
  date-modified = "2021-03-10 15:54:26 +0100",
  ISBN          = "3540439153",
  numpages      = "18",
  Pages         = "111--128",
  Publisher     = "Springer-Verlag",
  Series        = "LOPSTR '01",
  Title         = "Verification of Sets of Infinite State Processes Using Program Transformation",
  Year          = "2001",
  File          = "Verification of Sets of Infinite State Processes Using Program Transformation - Verification\_of\_Sets\_of\_Infinite\_State\_P - r.pdf"
}

@InProceedings{ 10.5555/646920.709171, Author = "Fioravanti, Fabio and Pettorossi, Alberto and Proietti, Maurizio", Abstract = "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.", Address = "Berlin, Heidelberg", BookTitle = "Selected Papers from the 11th International Workshop on Logic Based Program Synthesis and Transformation", date-added = "2021-03-10 15:54:26 +0100", date-modified = "2021-03-10 15:54:26 +0100", ISBN = "3540439153", numpages = "18", Pages = "111--128", Publisher = "Springer-Verlag", Series = "LOPSTR '01", Title = "Verification of Sets of Infinite State Processes Using Program Transformation", Year = "2001", File = "Verification of Sets of Infinite State Processes Using Program Transformation - Verification_of_Sets_of_Infinite_State_P - r.pdf" }