Generalization strategies for the verification of infinite state systems
From MaRDI portal
Publication:5299583
DOI10.1017/S1471068411000627zbMATH Open1267.68080arXiv1110.0999OpenAlexW2124412120MaRDI QIDQ5299583FDOQ5299583
Authors: Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni 
Publication date: 26 June 2013
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
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).
Full work available at URL: https://arxiv.org/abs/1110.0999
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
program verificationconstraint logic programsinfinite state systemsprogram specializationcomputational tree logicgeneralization strategies
Cites Work
- HyTech: A model checker for hybrid systems
- Title not available (Why is that?)
- Decidability of model checking for infinite-state concurrent systems
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- Logic programming and negation: A survey
- Logic program specialisation through partial deduction: Control issues
- Unfold/fold transformation of stratified programs
- Transformations of CLP modules
- Constraint-based verification of parameterized cache coherence protocols
- Action language verifier: An infinite-state model checker for reactive software specifications
- MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
Cited In (11)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- On recursion-free Horn clauses and Craig interpolation
- Title not available (Why is that?)
- Improving reachability analysis of infinite state systems by specialization
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Improving reachability analysis of infinite state systems by specialization
- Title not available (Why is that?)
- Program specialization for verifying infinite state systems: an experimental evaluation
- Title not available (Why is that?)
- 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)
