SubsidieMeestersA 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.
Projectdetails
Introduction
Program correctness is a central problem in computer science. Code inspection and testing can reveal many program bugs, but subtle errors need a rigorous analysis. A fully automated analysis is impossible: deciding whether a program terminates on a given input is undecidable.
Thanks to unremitting developments in program verification and incredible advancements in satisfiability checking, program verification is nowadays supported by software tools in industrial practice. Meta and Amazon Web Services use program verification tools on a daily basis.
Probabilistic Programming
In the advent of AI, probabilistic programming emerged as a popular paradigm combining programming with learning from (big) data. Since 2018, the UN uses such probabilistic programs to predict the location and classify seismological activities on the earth. Other application areas include:
- Security
- Planning in AI
- Cognitive science
- Neural network training
Characteristics of Probabilistic Programs
Probabilistic programs are fundamentally different. Due to randomness, they sometimes terminate and sometimes not. Their outcome depends on coin flips. They may terminate with probability one while having an infinite expected run time. Classical program verification techniques no longer apply.
The ERC Project FRAPPANT
The ERC project FRAPPANT has resulted in proof calculi for probabilistic programs, equipped with powerful proof rules, and identified a relatively complete syntax for quantitative properties. This has led to a prototypical deductive verifier for an “assembler” programming language, a software tool for which no equivalent exists.
Successful analyses of intricate programs showed its potential.
Project Goals
The proposed project aims to explore the commercial and innovative aspects of our deductive verifier. It takes the necessary innovative steps to enable commercialization by including:
- Invariant synthesis
- Program slicing
- Supporting the popular probabilistic programming language STAN
Its potential will be investigated by engaging potential users and conducting a market analysis.
Financiële details & Tijdlijn
Financiële details
| Subsidiebedrag | € 150.000 |
| Totale projectbegroting | € 150.000 |
Tijdlijn
| Startdatum | 1-11-2024 |
| Einddatum | 30-4-2026 |
| Subsidiejaar | 2024 |
Partners & Locaties
Projectpartners
- RHEINISCH-WESTFAELISCHE TECHNISCHE HOCHSCHULE AACHENpenvoerder
Land(en)
Vergelijkbare projecten binnen European Research Council
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Holistic Rigorous Numerical VerificationThe 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. | ERC Starting... | € 1.498.976 | 2025 | Details |
Program Intelligence, Declaratively and SymbolicallyThe PINDESYM project aims to advance automatic program understanding by integrating symbolic reasoning and machine learning into a unified declarative analysis framework. | ERC Advanced... | € 2.395.875 | 2024 | Details |
Formalised Reasoning about Expectations: Composable, Automated, Speedy, TrustworthyFoRECAST aims to develop theoretical foundations and tools for composable automatic differentiation and Bayesian inference, enhancing probabilistic programming for complex modeling applications. | ERC Starting... | € 1.500.000 | 2025 | Details |
Realizing the Promise of Higher-Order SMT and Superposition for Interactive VerificationThe Nekoka project aims to enhance higher-order SMT and λ-superposition for automated proof assistance, integrating them into tools for software verification and mathematical formalization. | ERC Consolid... | € 2.000.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 |
Holistic 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.
Program Intelligence, Declaratively and Symbolically
The PINDESYM project aims to advance automatic program understanding by integrating symbolic reasoning and machine learning into a unified declarative analysis framework.
Formalised Reasoning about Expectations: Composable, Automated, Speedy, Trustworthy
FoRECAST aims to develop theoretical foundations and tools for composable automatic differentiation and Bayesian inference, enhancing probabilistic programming for complex modeling applications.
Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification
The Nekoka project aims to enhance higher-order SMT and λ-superposition for automated proof assistance, integrating them into tools for software verification and mathematical formalization.
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.
Vergelijkbare projecten uit andere regelingen
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Integrated Safety for Deeply Embedded Systems Software (ISAFE)Het ISAFE-project ontwikkelt een geïntegreerde aanpak voor de kwalificatie van softwaretools in veiligheid kritische systemen, gericht op het voldoen aan veiligheidsstandaarden en het verbeteren van softwareontwikkeling. | Mkb-innovati... | € 160.200 | 2016 | Details |
Integrated Safety for Deeply Embedded Systems Software (ISAFE)
Het ISAFE-project ontwikkelt een geïntegreerde aanpak voor de kwalificatie van softwaretools in veiligheid kritische systemen, gericht op het voldoen aan veiligheidsstandaarden en het verbeteren van softwareontwikkeling.