Summary
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. However, automated verification of numerical programs over finite-precision (e.g. floating-point) numbers is currently limited. Finite precision introduces rounding errors w.r.t. 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.
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. My verification approach will be modular, automated, integrate with verification of non-accuracy properties and allow 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, localize faults in the program and communicate effectively with the verifier.
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.
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. My verification approach will be modular, automated, integrate with verification of non-accuracy properties and allow 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, localize faults in the program and communicate effectively with the verifier.
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.
Unfold all
/
Fold all
More information & hyperlinks
| Web resources: | https://cordis.europa.eu/project/id/101163629 |
| Start date: | 01-01-2025 |
| End date: | 31-12-2029 |
| Total budget - Public funding: | 1 498 976,00 Euro - 1 498 976,00 Euro |
Cordis data
Original description
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. However, automated verification of numerical programs over finite-precision (e.g. floating-point) numbers is currently limited. Finite precision introduces rounding errors w.r.t. 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.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. My verification approach will be modular, automated, integrate with verification of non-accuracy properties and allow 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, localize faults in the program and communicate effectively with the verifier.
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.
Status
SIGNEDCall topic
ERC-2024-STGUpdate Date
24-11-2024
Images
No images available.
Geographical location(s)
