Linear Arithmetic with Stars

DOI10.1007/978-3-540-70545-1_25zbMATH Open1155.68406OpenAlexW1493089824MaRDI QIDQ3512499FDOQ3512499

Authors Ružica Piskač, Viktor Kuncak

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) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability (number-theoretic aspects) (11U05)

Recommendations

• Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
• scientific article; zbMATH DE number 512972
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1979549
• Deciding Boolean algebra with Presburger arithmetic

Cites work

• scientific article; zbMATH DE number 1629957 (Why is no real title available?)
• scientific article; zbMATH DE number 1863374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090313 (Why is no real title available?)
• scientific article; zbMATH DE number 3416946 (Why is no real title available?)
• Automated Verification of Shape and Size Properties Via Separation Logic
• Carathéodory bounds for integer cones
• Combining WS1S and HOL
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Decision Procedures for Multisets with Cardinality Constraints
• Efficient E-Matching for SMT Solvers
• Lazy abstraction
• Multitree automata that count
• On the complexity of integer programming
• Semigroups, Presburger formulas, and languages
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

Cited in

(12)

• On the complexity of timed pattern matching
• MUNCH -- automated reasoner for sets and multisets
• Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
• Geometric decision procedures and the VC dimension of linear arithmetic theories
• Reasoning on data words over numeric domains
• Combining theories with shared set operations
• Efficient automated reasoning about sets and multisets with cardinality constraints
• On Intersection Problems for Polynomially Generated Sets
• Decision Procedures for Automating Termination Proofs
• Recent advances on reachability problems for valence systems (invited talk)
• Succinct ordering and aggregation constraints in algebraic array theories
• Certified reasoning with infinity

Describes a project that uses

Uses Software

• UCLID

This page was built for publication: Linear Arithmetic with Stars

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