SubsidieMeestersHolistic Rigorous Numerical Verification
The project aims to develop an automated verification and debugging framework for numerical programs that ensures accuracy in finite-precision computations while enhancing usability for developers.
Projectdetails
Introduction
My goal is to make rigorous numerical verification widely applicable and practically usable. Rigorous verification proves at compile-time that a program computes for all valid inputs what it is expected to. It is especially important for numerical programs, which are widely used across application domains and are often safety-critical.
Challenges in Numerical Verification
However, automated verification of numerical programs over finite-precision (e.g. floating-point) numbers is currently limited. Finite precision introduces rounding errors with respect to an ideal, real-valued specification and poses unique challenges for verification of program accuracy and other kinds of desirable properties.
As a result, verification of non-trivial numerical programs today requires extensive expert knowledge and mostly manual proofs. Additionally, when verification fails, e.g. because a program is buggy, developers have little debugging help available.
Proposed Solutions
I will rethink automated verification and debugging techniques for numerical programs from the ground up with accuracy as a core property. I propose a novel approach for accuracy verification based on deductive relational reasoning that will be able to effectively bound the difference between the specified (real-valued) and actually computed (finite-precision) program results.
Features of the Verification Approach
My verification approach will be:
- Modular
- Automated
- Integrated with verification of non-accuracy properties
- Allowing safe program optimizations for real-world programs
To further ensure the practical usability of the verifier, I will develop complementary techniques that will help developers to debug unsuccessful verification attempts by:
- Helping to fix specifications
- Localizing faults in the program
- Communicating effectively with the verifier
Expertise and Background
I will build on my comprehensive expertise with automated rigorous accuracy analysis and optimization of finite-precision arithmetic, and my recent efforts in deductive verification of floating-point runtime errors and numerical specification inference.
Financiële details & Tijdlijn
Financiële details
| Subsidiebedrag | € 1.498.976 |
| Totale projectbegroting | € 1.498.976 |
Tijdlijn
| Startdatum | 1-1-2025 |
| Einddatum | 31-12-2029 |
| Subsidiejaar | 2025 |
Partners & Locaties
Projectpartners
- UPPSALA UNIVERSITETpenvoerder
Land(en)
Vergelijkbare projecten binnen European Research Council
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
A Deductive Verifier for Probabilistic ProgramsThe project aims to commercialize a novel deductive verifier for probabilistic programs by integrating invariant synthesis and program slicing, targeting users and conducting market analysis. | ERC Proof of... | € 150.000 | 2024 | Details |
Verifiably Safe and Correct Deep Neural NetworksThis project aims to develop scalable verification techniques for large deep neural networks to ensure their safety and correctness in critical systems, enhancing reliability and societal benefits. | ERC Starting... | € 1.500.000 | 2023 | Details |
CertiFOX: Certified First-Order Model ExpansionThis project aims to develop methodologies for ensuring 100% correctness in combinatorial optimization solutions by providing end-to-end proof logging from user specifications to solver outputs. | ERC Consolid... | € 1.999.928 | 2024 | Details |
Systematic and computer-aided performance certification for numerical optimizationThe project aims to enhance theoretical foundations of numerical optimization to bridge the gap between theory and practice, developing robust algorithms and certification tools for complex applications. | ERC Starting... | € 1.497.650 | 2024 | Details |
Foundations of transcendental methods in computational nonlinear algebraDevelop new computational methods in nonlinear algebra using algebraic geometry to enhance the precision and reliability of numerical integration and algebraic invariant computation. | ERC Starting... | € 1.393.312 | 2022 | Details |
A Deductive Verifier for Probabilistic Programs
The project aims to commercialize a novel deductive verifier for probabilistic programs by integrating invariant synthesis and program slicing, targeting users and conducting market analysis.
Verifiably Safe and Correct Deep Neural Networks
This project aims to develop scalable verification techniques for large deep neural networks to ensure their safety and correctness in critical systems, enhancing reliability and societal benefits.
CertiFOX: Certified First-Order Model Expansion
This project aims to develop methodologies for ensuring 100% correctness in combinatorial optimization solutions by providing end-to-end proof logging from user specifications to solver outputs.
Systematic and computer-aided performance certification for numerical optimization
The project aims to enhance theoretical foundations of numerical optimization to bridge the gap between theory and practice, developing robust algorithms and certification tools for complex applications.
Foundations of transcendental methods in computational nonlinear algebra
Develop new computational methods in nonlinear algebra using algebraic geometry to enhance the precision and reliability of numerical integration and algebraic invariant computation.