Generalization strategies for the verification of infinite state systems
From MaRDI portal
Publication:5299583
Abstract: We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools. To appear in Theory and Practice of Logic Programming (TPLP).
Recommendations
- Computer Science Logic
- Tools and Algorithms for the Construction and Analysis of Systems
- scientific article; zbMATH DE number 1746451
- Automated Technology for Verification and Analysis
- scientific article; zbMATH DE number 2102702
- scientific article; zbMATH DE number 1499079
- Computer Aided Verification
- Taming the infinite: Verification of infinite-state reactive systems by finitary means
- Formal Verification of Infinite State Systems Using Boolean Methods
- CONCUR 2004 - Concurrency Theory
Cites work
- scientific article; zbMATH DE number 236855 (Why is no real title available?)
- Action language verifier: An infinite-state model checker for reactive software specifications
- Constraint-based verification of parameterized cache coherence protocols
- Decidability of model checking for infinite-state concurrent systems
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- HyTech: A model checker for hybrid systems
- Logic program specialisation through partial deduction: Control issues
- Logic programming and negation: A survey
- MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
- Transformations of CLP modules
- Unfold/fold transformation of stratified programs
Cited in
(13)- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- On recursion-free Horn clauses and Craig interpolation
- scientific article; zbMATH DE number 2084755 (Why is no real title available?)
- Improving reachability analysis of infinite state systems by specialization
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
- Specialization with constrained generalization for software model checking
- Controlling polyvariance for specialization-based verification
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Improving reachability analysis of infinite state systems by specialization
- scientific article; zbMATH DE number 2090119 (Why is no real title available?)
- Program specialization for verifying infinite state systems: an experimental evaluation
- scientific article; zbMATH DE number 1406234 (Why is no real title available?)
- Removing algebraic data types from constrained Horn clauses using difference predicates
This page was built for publication: Generalization strategies for the verification of infinite state systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5299583)
