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. 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 |
|---|---|---|---|---|
MANUNKIND: Determinants and Dynamics of Collaborative ExploitationThis project aims to develop a game theoretic framework to analyze the psychological and strategic dynamics of collaborative exploitation, informing policies to combat modern slavery. | ERC STG | € 1.497.749 | 2022 | Details |
Elucidating the phenotypic convergence of proliferation reduction under growth-induced pressureThe UnderPressure project aims to investigate how mechanical constraints from 3D crowding affect cell proliferation and signaling in various organisms, with potential applications in reducing cancer chemoresistance. | ERC STG | € 1.498.280 | 2022 | Details |
Uncovering the mechanisms of action of an antiviral bacteriumThis project aims to uncover the mechanisms behind Wolbachia's antiviral protection in insects and develop tools for studying symbiont gene function. | ERC STG | € 1.500.000 | 2023 | Details |
The Ethics of Loneliness and SociabilityThis project aims to develop a normative theory of loneliness by analyzing ethical responsibilities of individuals and societies to prevent and alleviate loneliness, establishing a new philosophical sub-field. | ERC STG | € 1.025.860 | 2023 | Details |
MANUNKIND: Determinants and Dynamics of Collaborative Exploitation
This project aims to develop a game theoretic framework to analyze the psychological and strategic dynamics of collaborative exploitation, informing policies to combat modern slavery.
Elucidating the phenotypic convergence of proliferation reduction under growth-induced pressure
The UnderPressure project aims to investigate how mechanical constraints from 3D crowding affect cell proliferation and signaling in various organisms, with potential applications in reducing cancer chemoresistance.
Uncovering the mechanisms of action of an antiviral bacterium
This project aims to uncover the mechanisms behind Wolbachia's antiviral protection in insects and develop tools for studying symbiont gene function.
The Ethics of Loneliness and Sociability
This project aims to develop a normative theory of loneliness by analyzing ethical responsibilities of individuals and societies to prevent and alleviate loneliness, establishing a new philosophical sub-field.
Vergelijkbare projecten uit andere regelingen
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Fast Proofs for Verifying ComputationsThe FASTPROOF project aims to enhance computational proof-systems by minimizing interaction, reducing proving time to linear complexity, and optimizing memory usage, while relying on cryptographic assumptions. | ERC STG | € 1.435.000 | 2022 | 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 COG | € 2.000.000 | 2023 | 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 ADG | € 2.395.875 | 2024 | 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 COG | € 1.999.928 | 2024 | Details |
Fast Proofs for Verifying Computations
The FASTPROOF project aims to enhance computational proof-systems by minimizing interaction, reducing proving time to linear complexity, and optimizing memory usage, while relying on cryptographic assumptions.
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.
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.
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.