Counterexample-Guided Correlation Algorithm for Translation Validation
summary
An algorithm constructs product CFGs that correlate sets of source paths with assembly paths using pathset correlation to avoid exponential path blowup, and it uses a counterexample-guided best-first search that prunes and ranks 232 candidate product-CFGs down to ~8.9 expansions on average. The tool uses SMT solver models returned during invariant inference as concrete counterexamples, proves equivalence for 85 TSVC functions and 16 LORE patterns, and finds three real bugs in diet libc.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:52Product program construction
- 2:58Pathset correlation
- 5:17Counterexample-guided search
- 11:51Experimental results
- 14:57Conclusion
related talks
59mCompiler-assisted Translation Validation
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
53mFrom Within: Compiler Testing and Validation via Compilers
15mDetecting and explaining (in-)equivalence of context-free grammars
27mProducing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
17mExploring Locally Bounded Translation Validation
18mTowards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…)
53mLocknote: How Badly Do We Want Correct Compilers?