Efficient Symbolic Representations for Arithmetic Constraints in Verification

DOI10.1142/S0129054103001911MaRDI QIDQ5696928zbMATH OpenFDO

Authors Constantinos Bartzis, Tevfik Bultan

Publication date 19 October 2005

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

zbMATH Keywords

automatasymbolic model checkingpresburger arithmetic

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• scientific article; zbMATH DE number 1962792
• Efficient image computation in infinite state model checking.
• scientific article; zbMATH DE number 1956595
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• scientific article; zbMATH DE number 2090515

Cites work

• scientific article; zbMATH DE number 1692895 (Why is no real title available?)
• scientific article; zbMATH DE number 3412171 (Why is no real title available?)
• HyTech: A model checker for hybrid systems

Cited in

(12)

• Symbolic String Verification: Combining String Analysis and Size Analysis
• scientific article; zbMATH DE number 1962792 (Why is no real title available?)
• Action language verifier: An infinite-state model checker for reactive software specifications
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• scientific article; zbMATH DE number 2086591 (Why is no real title available?)
• Structural Presburger digit vector automata
• Efficient image computation in infinite state model checking.
• Automata-based symbolic string analysis for vulnerability detection
• The convex hull of a regular set of integer vectors is polyhedral and effectively computable
• LTL over integer periodicity constraints
• scientific article; zbMATH DE number 1956595 (Why is no real title available?)
• Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space

Describes a project that uses

Uses Software

• MONA
• HyTech

This page was built for publication: Efficient Symbolic Representations for Arithmetic Constraints in Verification

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