63 citations · 83 across the 11 of their papers we have counts for
17 papers
Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers
Rosa Abbasi, Eva Darulova
SMT solvers are essential in various domains, including program verification and synthesis. Although their correctness and performance have been extensively studied, performance te…
Verifying Floating-Point Programs in Stainless
Andrea Gilot, Axel Bergström, Eva Darulova
We extend the Stainless deductive verifier with floating-point support, providing the first automated verification support for floating-point numbers for a subset of Scala that inc…
Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages
Andrea Gilot, Tobias Wrigstad, Eva Darulova
Reasoning about floating-point arithmetic is notoriously hard. While static and dynamic analysis techniques or program repair have made significant progress, more work is still nee…
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…
Sound Approximation of Programs with Elementary Functions
Eva Darulova, Anastasia Volkova
Elementary function calls are a common feature in numerical programs. While their implementions in library functions are highly optimized, their computation is nonetheless very exp…
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…
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…
Precise but Natural Specification for Robot Tasks
Ivan Gavran, Brendon Boldt, Eva Darulova +1
We present Flipper, a natural language interface for describing high-level task specifications for robots that are compiled into robot actions. Flipper starts with a formal core la…
On Sound Relative Error Bounds for Floating-Point Arithmetic
Anastasiia Izycheva, Eva Darulova
State-of-the-art static analysis tools for verifying finite-precision code compute worst-case absolute error bounds on numerical errors. These are, however, often not a good estima…
Sound Mixed-Precision Optimization with Rewriting
Eva Darulova, Einar Horn, Saksham Sharma
Finite-precision arithmetic computations face an inherent tradeoff between accuracy and efficiency. The points in this tradeoff space are determined, among other factors, by differ…
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Heiko Becker, Nikita Zyuzin, Raphael Monat +3
Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepa…
Towards a Compiler for Reals
Eva Darulova, Viktor Kuncak
Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. In many domai…
On Sound Compilation of Reals
Eva Darulova, Viktor Kuncak
Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming…