Solving LIA^ using approximations

DOI10.1007/978-3-030-39322-9_17MaRDI QIDQ784151zbMATH OpenOpenAlexFDO

Authors Maxwell Levatich, Nikolaj Bjørner, Ružica Piskač, Sharon Shoham

Publication date 5 August 2020

Full work available at URL https://doi.org/10.1007/978-3-030-39322-9_17

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Linear Arithmetic with Stars
• Computer Aided Verification
• Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
• Geometric decision procedures and the VC dimension of linear arithmetic theories
• scientific article; zbMATH DE number 1979549

Cited in

(6)

• Efficient automated reasoning about sets and multisets with cardinality constraints
• Succinct ordering and aggregation constraints in algebraic array theories
• Geometric decision procedures and the VC dimension of linear arithmetic theories
• Bounded satisfiability checking of \(\mathrm{FOL}^*\) formulas with aggregations
• Verifying SQL queries using theories of tables and relations
• Integrating cardinality constraints into constraint logic programming with sets

This page was built for publication: Solving \(\mathrm{LIA}^\star\) using approximations

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