9 papers
REST: Integrating Term Rewriting with Program Verification (Extended Version)
Zachary Grannan, Niki Vazou, Eva Darulova +1
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables fl…
Dandelion: Certified Approximations of Elementary Functions
Heiko Becker, Mohit Tekriwal, Eva Darulova +2
Elementary function operations such as sin and exp cannot in general be computed exactly on today's digital computers, and thus have to be approximated. The standard approximations…
Deductive Verification of Floating-Point Java Programs in KeY
Rosa Abbasi Boroujeni, Jonas Schiffl, Eva Darulova +2
Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is…
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran +2
Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requ…
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson +4
Recent program synthesis techniques help users customize CAD models(e.g., for 3D printing) by decompiling low-level triangle meshes to Constructive Solid Geometry (CSG) expressions…
Exploiting Errors for Efficiency: A Survey from Circuits to Algorithms
Phillip Stanley-Marbell, Armin Alaghi, Michael Carbin +13
When a computational task tolerates a relaxation of its specification or when an algorithm tolerates the effects of noise in its execution, hardware, programming languages, and sys…