Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise

Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V. (2013). Controlling polyvariance for specialization-based verification. FUNDAMENTA INFORMATICAE, 124(Special Issue on CILC-11), 483-502 [10.3233/FI-2013-845].

Controlling polyvariance for specialization-based verification

PETTOROSSI, ALBERTO;
2013-01-01

Abstract

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise
2013
Pubblicato
Rilevanza internazionale
Articolo
Esperti anonimi
Settore ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
English
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V. (2013). Controlling polyvariance for specialization-based verification. FUNDAMENTA INFORMATICAE, 124(Special Issue on CILC-11), 483-502 [10.3233/FI-2013-845].
Fioravanti, F; Pettorossi, A; Proietti, M; Senni, V
Articolo su rivista
File in questo prodotto:
File Dimensione Formato  
FPPS_ControllingPolyvariance_FundInf-13.pdf

solo utenti autorizzati

Licenza: Copyright dell'editore
Dimensione 185.93 kB
Formato Adobe PDF
185.93 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/76487
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact