Cardinality constraints for arrays (decidability results and applications)
From MaRDI portal
Publication:1688541
DOI10.1007/s10703-017-0279-6zbMath1377.68125OpenAlexW2606648105MaRDI QIDQ1688541
Silvio Ghilardi, Elena Pagani, Francesco Alberti
Publication date: 8 January 2018
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-017-0279-6
Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)
Related Items
NP satisfiability for arrays as powers, Reasoning about vectors: satisfiability modulo a theory of sequences, Interpolation Results for Arrays with Length and MaxDiff, On algebraic array theories, Unnamed Item, Higher-order quantifier elimination, counter simulations and fault-tolerant systems, Reasoning about vectors using an SMT theory of sequences
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Decision procedures for flat array properties
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Deciding Boolean algebra with Presburger arithmetic
- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- Model checking of systems with many identical timed processes
- Verifying programs with unreliable channels
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- The Heard-Of model: computing in distributed systems with benign faults
- Carathéodory bounds for integer cones
- Counting Constraints in Flat Array Fragments
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- PSync: a partially synchronous language for fault-tolerant distributed algorithms
- A Logic-Based Framework for Verifying Consensus Algorithms
- What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
- Solving SAT and SAT Modulo Theories
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Collections, Cardinalities, and Relations
- Presburger arithmetic with unary predicates is Π11 complete
- Automated Deduction – CADE-20
- Tolerating corrupted communication
- Parameterized Verification of Infinite-State Processes with Global Conditions
- Decision Procedures for Multisets with Cardinality Constraints
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
