Lockstep Composition for Unbalanced Loops
May 2020 - Present
Florida State University
- Developing a novel technique for equivalence checking of programs where programs can have different structures
- Checking the equivalence of a program with its optimized version for (specific) compiler/hand loop optimizations (Loop Vectorization, Loop Unswitching, Loop Peeling)
- Uses Abstraction-Refinement for program reasoning, and SMT-based Model Checking for proof generation