Sets with Cardinality Constraints in Satisfiability Modulo Theories
From MaRDI portal
Publication:3075499
DOI10.1007/978-3-642-18275-4_28zbMath1317.68124MaRDI QIDQ3075499
Viktor Kuncak, Philippe Suter, Robin Steiger
Publication date: 15 February 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.185.3278
68Q25: Analysis of algorithms and problem complexity
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Unnamed Item, Scala to the Power of Z3: Integrating SMT and Programming, Adding decision procedures to SMT solvers using axioms with triggers, Reasoning about algebraic data types with abstractions, On automation in the verification of software barriers: experience report, A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT, Decision Procedures for Region Logic
Uses Software
Cites Work
- Unnamed Item
- Deciding Boolean algebra with Presburger arithmetic
- Model-based Theory Combination
- The first order properties of products of algebraic systems
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Cardinality Abstraction for Declarative Networking Applications
- HyperConsistency Width for Constraint Satisfaction: Algorithms and Complexity Results
- Combining Theories with Shared Set Operations
- Building a Calculus of Data Structures
- Collections, Cardinalities, and Relations
- Programming by Refinement, as Exemplified by the SETL Representation Sublanguage
- Decision procedures for algebraic data types with abstractions
- A combination framework for tracking partition sizes
- Verification, Model Checking, and Abstract Interpretation
- Combined Satisfiability Modulo Parametric Theories