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

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

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)

Cites Work

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

Cited In (12)

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

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)