Efficient Symbolic Representations for Arithmetic Constraints in Verification

DOI10.1142/S0129054103001911zbMATH Open1101.68642MaRDI QIDQ5696928FDOQ5696928

Authors: Constantinos Bartzis, Tevfik Bultan 

Publication date: 19 October 2005

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

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

zbMATH Keywords

automatasymbolic model checkingpresburger arithmetic

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

• HyTech: A model checker for hybrid systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (12)

• Symbolic String Verification: Combining String Analysis and Size Analysis
• Title not available (Why is that?)
• Action language verifier: An infinite-state model checker for reactive software specifications
• Title not available (Why is that?)
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• 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
• Title not available (Why is that?)
• Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space

Uses Software

• HyTech
• MONA

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)