Verification of Source Code Transformations by Program Equivalence Checking
Abstract elided by the publisher.
Related papers
- Automatic Generation of Debug Headers through BlackBox Equivalence Checking CGO 2022
- PolyCheck: dynamic verification of iteration space transformations on affine programs POPL 2016
- Formally Verifying a Transformation from MLTL Formulas to Regular Expressions TACAS 2025
- Graphiti: Bridging Graph and Relational Database Queries PLDI 2025
- Sigma*: symbolic learning of input-output specifications POPL 2013
- VeriEQ: Finding Verilog Simulators and Synthesizers Bugs with Equivalence Circuit Transformation OOPSLA 2026
- Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations TOPLAS 2014
- Formal verification of practical MPI programs PPoPP 2009