Linear Arithmetic with Stars

DOI10.1007/978-3-540-70545-1_25zbMath1155.68406OpenAlexW1493089824MaRDI QIDQ3512499

Viktor Kuncak, Ruzica Piskac

Publication date: 15 July 2008

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_25

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability (number-theoretic aspects) (11U05) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

On the complexity of timed pattern matching, Recent advances on reachability problems for valence systems (invited talk), Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars, MUNCH - Automated Reasoner for Sets and Multisets, Certified Reasoning with Infinity, Decision Procedures for Automating Termination Proofs, Combining Theories with Shared Set Operations, Efficient automated reasoning about sets and multisets with cardinality constraints

Uses Software

• UCLID

Cites Work

• Multitree automata that count
• Carathéodory bounds for integer cones
• Semigroups, Presburger formulas, and languages
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• On the complexity of integer programming
• Lazy abstraction
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Automated Verification of Shape and Size Properties Via Separation Logic
• Decision Procedures for Multisets with Cardinality Constraints
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item