Generalization strategies for the verification of infinite state systems

DOI10.1017/S1471068411000627zbMath1267.68080arXiv1110.0999OpenAlexW2124412120MaRDI QIDQ5299583

Maurizio Proietti, Valerio Senni, Alberto Pettorossi, Fabio Fioravanti

Publication date: 26 June 2013

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1110.0999

zbMATH Keywords

program verificationconstraint logic programsinfinite state systemsprogram specializationcomputational tree logicgeneralization strategies

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items (4)

Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Proving correctness of imperative programs by linearizing constrained Horn clauses ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates

Cites Work

• Unnamed Item
• Transformations of CLP modules
• Action language verifier: An infinite-state model checker for reactive software specifications
• Unfold/fold transformation of stratified programs
• HyTech: A model checker for hybrid systems
• 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
• MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
• Logic programming and negation: A survey
• Logic program specialisation through partial deduction: Control issues

This page was built for publication: Generalization strategies for the verification of infinite state systems