Second Order Quantifier Elimination: Towards Verification Applications

No abstract is available for this paper.

• Publication year

  2017

• Venue

  SOQE

• Publication date

  2017-12-01

• Fields of study

  Mathematics, Computer Science

• Identifiers

  No identifiers available.

• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

  2017influential reference
• Cardinality constraints for arrays (decidability results and applications)

  2017influential reference
• Counting Constraints in Flat Array Fragments

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

  2016cited by this paper
• Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies

  2016cited by this paper
• The SeaHorn Verification Framework

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

  2015cited by this paper
• Counterexample-Guided Quantifier Instantiation for Synthesis in SMT

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

  2014cited by this paper
• The nuXmv Symbolic Model Checker

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

  2013cited by this paper
• Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms

  2013cited by this paper
• Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper

  2012cited by this paper
• Lazy Abstraction with Interpolants for Arrays

  2012cited by this paper
• Software Model Checking via IC3

  2012cited by this paper
• Generalized Property Directed Reachability

  2012cited by this paper
• μZ- An Efficient Engine for Fixed Points with Constraints

  2011cited by this paper
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

  2010cited by this paper
• MCMT: A Model Checker Modulo Theories

  2010cited by this paper
• Interpolation and Symbol Elimination

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

  2006cited by this paper
• Constraint-Based Verification of Parameterized Cache Coherence Protocols

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

  2002cited by this paper
• Predicate abstraction for software verification

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

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

  1999cited by this paper
• Introduction to higher order categorical logic

  1988cited by this paper
• INTRODUCTION TO HIGHER ORDER CATEGORICAL LOGIC (Cambridge Studies in Advanced Mathematics 7)

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

  1987cited by this paper
• An introduction to mathematical logic and type theory - to truth through proof

  1986cited by this paper
• Introduction to higher order categorical logic

  1986cited by 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

  2017cites this paper
• What is a neutral criterion of ontological commitment

  2017cites this paper