Cardinality constraints for arrays (decidability results and applications)

No abstract is available for this paper.

• Publication year

  2017

• Venue

  Formal methods in system design

• Publication date

  2017-04-21

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/s10703-017-0279-6
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Art of Multiprocessor Programming

  2021cited by this paper
• Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

  2017cited by this paper
• Cardinalities and universal quantifiers for verifying parameterized systems

  2016cited by this paper
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT

  2016cited by this paper
• Counting Constraints in Flat Array Fragments

  2016cited by this paper
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms

  2015cited by this paper
• The Need for Language Support for Fault-Tolerant Distributed Systems

  2015cited by this paper
• SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms

  2015cited by this paper
• On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability

  2014cited by this paper
• A Logic-Based Framework for Verifying Consensus Algorithms

  2014cited by this paper
• Parameterized model checking of fault-tolerant distributed algorithms by abstraction

  2013cited by this paper
• Collections, Cardinalities, and Relations

  2010cited by this paper
• The Heard-Of model: computing in distributed systems with benign faults

  2009cited by this paper
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

  2009cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Decision Procedures for Multisets with Cardinality Constraints

  2008cited by this paper
• Regular Model Checking without Transducers

  2007cited by this paper
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

  2007cited by this paper
• Tolerating corrupted communication

  2007cited by this paper
• Deciding Boolean Algebra with Presburger Arithmetic

  2006cited by this paper
• Carathéodory bounds for integer cones

  2006cited by this paper
• Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

  2006cited by this paper
• An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic

  2005cited by this paper
• Model checking of systems with many identical timed processes

  2003cited by this paper
• Arithmetic, first-order logic, and counting quantifiers

  2002cited by this paper
• Combining Sets with Integers

  2002cited by this paper
• On the verification of broadcast protocols

  1999cited by this paper
• On the Veri cation of Broadcast

  1999cited by this paper
• Constraint-Based Analysis of Broadcast Protocols

  1999cited by this paper
• General decidability theorems for infinite-state systems

  1996cited by this paper
• Verifying programs with unreliable channels

  1993cited by this paper
• Presburger arithmetic with unary predicates is Π11 complete

  1991cited by this paper
• Simulating authenticated broadcasts to derive simple fault-tolerant algorithms

  1987influential reference
• Optimal clock synchronization

  1985cited by this paper
• A low-overhead coherence solution for multiprocessors with private cache memories

  1984cited by this paper
• Noname manuscript No. (will be inserted by the editor) Approximated Parameterized Verification of Infinite-state Processes with Global Conditions

  year unknowncited by this paper
• Università Della Svizzera Italiana Usi Technical Report Series in Informatics Decision Procedures for Flat Array Properties

  year unknowncited by this paper

• Encoding and Reasoning About Arrays in Set Theory

  2025cites this paper
• Succinct ordering and aggregation constraints in algebraic array theories

  2024cites this paper
• Combinatory Array Logic with Sums

  2023cites this paper
• Interpolation Results for Arrays with Length and MaxDiff

  2023cites this paper
• The Complexity of Satisfiability Checking for Symbolic Finite Automata

  2023cites this paper
• On algebraic array theories

  2023cites this paper
• Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences

  2023cites this paper
• The Complexity of Checking Non-Emptiness in Symbolic Tree Automata

  2023cites this paper
• Reasoning About Vectors using an SMT Theory of Sequences

  2022cites this paper
• General Interpolation and Strong Amalgamation for Contiguous Arrays

  2022cites this paper
• Integrating Cardinality Constraints into Constraint Logic Programming with Sets

  2021cites this paper
• log: Set Formulas as Programs

  2021cites this paper
• NP Satisfiability for Arrays as Powers

  2021cites this paper
• Verifying Safety of Parameterized Heard-Of Algorithms

  2020cites this paper
• Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems

  2020cites this paper
• Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

  2017influential citation
• Second Order Quantifier Elimination: Towards Verification Applications

  2017influential citation
• Journal of Logical and Algebraic Methods in Programming

  year unknowncites this paper