Sets with Cardinality Constraints in Satisfiability Modulo Theories

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

Mathematics Subject Classification ID

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

• BLAST
• z3

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