Cardinality constraints for arrays (decidability results and applications)
type: Item
instance of: scholarly article
title: Cardinality constraints for arrays (decidability results and applications)
zbMATH Open document ID: 1377.68125
author: Silvio Ghilardi
author: Francesco Alberti
author: Elena Pagani
published in: Formal Methods in System Design
publication date: 2018-01-08T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68W15
zbMATH DE Number: 6823095
zbMATH Keywords: arrays
zbMATH Keywords: cardinality constraints
zbMATH Keywords: fault-tolerant systems
describes a project that uses: z3
MaRDI profile type: Publication
full work available at URL: s10703-017-0279-6
OpenAlex ID: W2606648105
cites work: Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
cites work: Parameterized Verification of Infinite-State Processes with Global Conditions
cites work: Verifying programs with unreliable channels
cites work: Model checking of systems with many identical timed processes
cites work: Counting Constraints in Flat Array Fragments
cites work: Decision procedures for flat array properties
cites work: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
cites work: Tolerating corrupted communication
cites work: The Heard-Of model: computing in distributed systems with benign faults
cites work: Q4945217
cites work: A Logic-Based Framework for Verifying Consensus Algorithms
cites work: \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
cites work: Carathéodory bounds for integer cones
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: Higher-order quantifier elimination, counter simulations and fault-tolerant systems
cites work: Presburger arithmetic with unary predicates is Π11 complete
cites work: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
cites work: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
cites work: What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
cites work: Automated Deduction – CADE-20
cites work: Deciding Boolean algebra with Presburger arithmetic
cites work: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
cites work: Solving SAT and SAT Modulo Theories
cites work: Decision Procedures for Multisets with Cardinality Constraints
cites work: Collections, Cardinalities, and Relations
cites work: Q4737128
DOI: 10.1007/S10703-017-0279-6
description: scientific article; zbMATH DE number 6823095