Transformational Verification of Parameterized Protocols Using Array Formulas. (Articolo in rivista)

Type

• Prodotto della ricerca (Classe)
• Articolo in rivista (Classe)

Label

• Transformational Verification of Parameterized Protocols Using Array Formulas. (Articolo in rivista) (literal)

Anno

• 2006-01-01T00:00:00+01:00 (literal)

Alternative label

• Pettorossi, A.; Proietti, M.; Senni, V. (2006)
  Transformational Verification of Parameterized Protocols Using Array Formulas.
  in Lecture notes in computer science
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• Pettorossi, A.; Proietti, M.; Senni, V. (literal)

Pagina inizio

• 23 (literal)

Pagina fine

• 43 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume

• 3901 (literal)

Rivista

• Lecture notes in computer science (Rivista)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note

• In: Patricia M. Hill (Ed.): Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, Revised Selected Papers. Springer (literal)

Note

• SCImago (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni

• Pettorossi, A. DISP, Università Tor Vergata, Roma; IASI-CNR (literal)

Titolo

• Transformational Verification of Parameterized Protocols Using Array Formulas. (literal)

Abstract

• We propose a method for the specification and the automated verification of temporal properties of parameterized protocols. Our method is based on logic programming and program transformation. We specify the properties of parameterized protocols by using an extension of stratified logic programs. This extension allows premises of clauses to contain first order formulas over arrays of parameterized length. A property of a given protocol is proved by applying suitable unfold/fold transformations to the specification of that protocol.We demonstrate our method by proving that the parameterized Peterson's protocol among N processes, for any N >=2, ensures the mutual exclusion property. (literal)

Prodotto di

• Istituto di analisi dei sistemi ed informatica \"Antonio Ruberti\" (IASI) (Istituto)

Autore CNR

• Valerio Senni (Persona)
• Alberto Pettorossi (Persona)
• MAURIZIO PROIETTI (Persona)

Incoming links:

Autore CNR di

• MAURIZIO PROIETTI (Persona)
• Valerio Senni (Persona)
• Alberto Pettorossi (Persona)

Prodotto

• Istituto di analisi dei sistemi ed informatica \"Antonio Ruberti\" (IASI) (Istituto)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi

• Lecture notes in computer science (Rivista)