Sets with Cardinality Constraints in Satisfiability Modulo Theories

DOI10.1007/978-3-642-18275-4_28zbMath1317.68124OpenAlexW3137545899MaRDI 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

Analysis of algorithms and problem complexity (68Q25) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (7)

Decision Procedures for Region Logic ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Reasoning about algebraic data types with abstractions ⋮ Unnamed Item ⋮ Scala to the Power of Z3: Integrating SMT and Programming ⋮ A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT ⋮ On automation in the verification of software barriers: experience report

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

This page was built for publication: Sets with Cardinality Constraints in Satisfiability Modulo Theories