@prefix pubblicazioni: . @prefix unitaDiPersonaleInterno: . @prefix prodotto: . unitaDiPersonaleInterno:MATRICOLA42097 pubblicazioni:autoreCNRDi prodotto:ID7012 . @prefix prodottidellaricerca: . @prefix istituto: . istituto:CDS003 prodottidellaricerca:prodotto prodotto:ID7012 . @prefix unitaDiPersonaleEsterno: . unitaDiPersonaleEsterno:ID1288 pubblicazioni:autoreCNRDi prodotto:ID7012 . @prefix modulo: . modulo:ID2271 prodottidellaricerca:prodotto prodotto:ID7012 . @prefix rdf: . prodotto:ID7012 rdf:type prodotto:TIPO1101 . @prefix retescientifica: . prodotto:ID7012 rdf:type retescientifica:ProdottoDellaRicerca . @prefix rdfs: . prodotto:ID7012 rdfs:label "Verification of Sets of Infinite State Systems Using Program Transformation (Articolo in rivista)"@en . @prefix xsd: . prodotto:ID7012 pubblicazioni:anno "2002-01-01T00:00:00+01:00"^^xsd:gYear . @prefix skos: . prodotto:ID7012 skos:altLabel "
Fioravanti, F.; Pettorossi, A.; Proietti, M. (2002)
Verification of Sets of Infinite State Systems Using Program Transformation
in Lecture notes in computer science
"^^rdf:HTML ; pubblicazioni:autori "Fioravanti, F.; Pettorossi, A.; Proietti, M."^^xsd:string ; pubblicazioni:paginaInizio "111"^^xsd:string ; pubblicazioni:paginaFine "128"^^xsd:string ; pubblicazioni:numeroVolume "2372"^^xsd:string . @prefix ns12: . prodotto:ID7012 pubblicazioni:rivista ns12:ID583862 ; skos:note "ISI Web of Science (WOS)"^^xsd:string ; pubblicazioni:titolo "Verification of Sets of Infinite State Systems Using Program Transformation"^^xsd:string ; prodottidellaricerca:abstract "We present a method for the verification of safety properties of concurrent\nsystems which consist of finite sets of infinite state processes. Systems\nand properties are specified by using constraint logic programs, and the\ninference engine for verifying properties is provided by a technique based\non unfold/fold program transformations. We deal with properties of finite\nsets of processes of arbitrary cardinality, and in order to do so, we\nconsider constraint logic programs where the constraint theory is the Weak\nMonadic Second Order Theory of k Successors. Our verification method\nconsists in transforming the programs that specify the properties of\ninterest into equivalent programs where the truth of these properties can\nbe checked by simple inspection in constant time. We present a strategy for\nguiding the application of the unfold/fold rules and realizing the\ntransformations in a semiautomatic way." ; prodottidellaricerca:prodottoDi modulo:ID2271 , istituto:CDS003 ; pubblicazioni:autoreCNR unitaDiPersonaleEsterno:ID1288 , unitaDiPersonaleInterno:MATRICOLA42097 . ns12:ID583862 pubblicazioni:rivistaDi prodotto:ID7012 .