Controlling polyvariance for specialization-based verification

DOI10.3233/FI-2013-845MaRDI QIDQ2841959zbMATH OpenOpenAlexFDO

Authors Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni

Publication date 30 July 2013

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2013-845

zbMATH Keywords

constraint logic programminggeneralizationpolyvarianceprogram specializationunfold/fold transformationverification of infinite state reactive systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Improving reachability analysis of infinite state systems by specialization
• Improving reachability analysis of infinite state systems by specialization
• Program specialization for verifying infinite state systems: an experimental evaluation
• Generalization strategies for the verification of infinite state systems
• Software model checking by program specialization

Cited in

(11)

• Inferring safe Maude programs with ÁTAME
• Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system
• Polycheck: dynamic verification of iteration space transformations on affine programs
• Program specialization for verifying infinite state systems: an experimental evaluation
• Using real relaxations during program specialization
• scientific article; zbMATH DE number 7453197 (Why is no real title available?)
• Anti-unification in constraint logic programming
• Removing Superfluous Versions in Polyvariant Specialization of Prolog Programs
• Improving reachability analysis of infinite state systems by specialization
• Improving reachability analysis of infinite state systems by specialization
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

This page was built for publication: Controlling polyvariance for specialization-based verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2841959)