EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations
No abstract available.
Related papers
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions CAV 1999
- BDD Based Procedures for a Theory of Equality with Uninterpreted Functions CAV 1998
- Dependently-Typed Programming with Logical Equality Reflection ICFP 2023
- How to safely use extensionality in Liquid Haskell Haskell 2022
- Revisiting Positive Equality TACAS 2004
- M-Lisp: A Representation-Independent Dialect of Lisp with Reduction Semantics TOPLAS 1992
- Logical inference techniques for loop parallelization PLDI 2012
- Decidable verification of uninterpreted programs POPL 2019