Unbounded model-checking with interpolation for regular language constraints

DOI10.1007/978-3-642-36742-7_20MaRDI QIDQ5326331zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Graeme Gange, Jorge Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-36742-7_20

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic automata constraint solving
• A decision procedure for regular membership and length constraints over unbounded strings
• Solving String Theories Involving Regular Membership Predicates Using SAT
• An efficient SMT solver for string constraints
• Towards more efficient methods for solving regular-expression heavy string constraints

Cited in

(7)

• A complete refinement procedure for regular separability of context-free languages
• Design and implementation of bounded-length sequence variables
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Automated Technology for Verification and Analysis
• Reasoning About Regular Properties: A Comparative Study
• Dashed strings for string constraint solving
• Tools and Algorithms for the Construction and Analysis of Systems

Describes a project that uses

Uses Software

• MAGIC
• FOCI
• HAMPI

This page was built for publication: Unbounded model-checking with interpolation for regular language constraints

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