Deciding Equality Formulas by Small Domains Instantiations
Abstract elided by the publisher.
Related papers
- Deciding Boolean Separation Logic via Small Models TACAS 2024
- Range Allocation for Separation Logic CAV 2004
- Towards Complete Reasoning about Axiomatic Specifications VMCAI 2011
- Decidability of conversion for type theory in type theory POPL 2018
- Decidable verification of uninterpreted programs POPL 2019
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories CAV 2009
- Formula Normalizations in Verification CAV 2023
- An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification POPL 2024