6 citations · 8 across the 2 of their papers we have counts for
2 papers
cs.PL2023★ 2 cited
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Jason Gross, Andres Erbsen, Jade Philipoom +2
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof…
cs.PL2022★ 6 cited
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Jason Gross, Andres Erbsen, Jade Philipoom +2
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to im…