Program specialization for verifying infinite state systems: an experimental evaluation

DOI10.1007/978-3-642-20551-4_11MaRDI QIDQ3003492zbMATH OpenOpenAlexFDO

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

Publication date 27 May 2011

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-20551-4_11

Mathematics Subject Classification ID

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

Recommendations

• Generalization strategies for the verification of infinite state systems
• Controlling polyvariance for specialization-based verification
• Improving reachability analysis of infinite state systems by specialization
• Improving reachability analysis of infinite state systems by specialization
• scientific article; zbMATH DE number 2084755

Cites work

• Action language verifier: An infinite-state model checker for reactive software specifications
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• Constraint-based deductive model checking
• Constraint-based verification of parameterized cache coherence protocols
• Convex hull abstractions in specialization of CLP programs
• Decidability of model checking for infinite-state concurrent systems
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• scientific article; zbMATH DE number 1615252 (Why is no real title available?)
• scientific article; zbMATH DE number 1629966 (Why is no real title available?)
• scientific article; zbMATH DE number 1696790 (Why is no real title available?)
• scientific article; zbMATH DE number 1696809 (Why is no real title available?)
• scientific article; zbMATH DE number 1232244 (Why is no real title available?)
• scientific article; zbMATH DE number 1953286 (Why is no real title available?)
• scientific article; zbMATH DE number 1973221 (Why is no real title available?)
• scientific article; zbMATH DE number 1538039 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 1424027 (Why is no real title available?)
• HyTech: A model checker for hybrid systems
• Logic programming and negation: A survey
• MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
• Myths about the mutual exclusion problem
• Tabled evaluation with delaying for general logic programs
• Unfold/fold transformation of stratified programs

Cited in

(11)

• Temporal property verification as a program analysis task
• scientific article; zbMATH DE number 1615252 (Why is no real title available?)
• Controlling polyvariance for specialization-based verification
• Specialization with constrained generalization for software model checking
• scientific article; zbMATH DE number 2084755 (Why is no real title available?)
• scientific article; zbMATH DE number 2090119 (Why is no real title available?)
• Using real relaxations during program specialization
• scientific article; zbMATH DE number 1406234 (Why is no real title available?)
• Software model checking by program specialization
• Improving reachability analysis of infinite state systems by specialization
• Improving reachability analysis of infinite state systems by specialization

Describes a project that uses

Uses Software

• HyTech
• ECCE

This page was built for publication: Program specialization for verifying infinite state systems: an experimental evaluation

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