CORPORA · COntext-free model checking for Recursive PrObabilistic pRogrAms
Horizon Europe — Marie Skłodowska-Curie Actions
- Duration
- 2023-09-01 → 2025-08-31
- EU contribution
- €183,601
- Participants
- 1
- Scheme
- HORIZON-TMA-MSCA-PF-EF
Lines connect the coordinator with its partners.
Results in brief
COntext-free model checking for Recursive PrObabilistic pRogrAms
The CORPORA project tackles the challenge of verifying the reliability and safety of software systems that rely on advanced probabilistic reasoning. Probabilistic programs are increasingly used to model and implement complex decision-making under uncertainty, from autonomous systems and cybersecurity protocols to cognitive science models. However, existing verification techniques are ill-equipped to analyse programs that incorporate nested conditioning and other intricate stochastic phenomena, which are essential to accurately represent real-world processes. CORPORA has developed cutting-edge verification techniques and tools that enable scalable, mathematically rigorous analysis of probabilistic programs with recursive and nested structures. By integrating probabilistic model checking with expressive temporal logics based on context-free languages, the project delivers a novel theoretical and algorithmic foundation for reasoning about stochastic systems at a level of precision previously unattainable. The resulting open-source tools allow researchers and practitioners to detect design flaws, prove safety and correctness properties, and optimize decision-making systems.
Data: CORDIS, © European Union
Project objective
IoT and embedded systems are powered by increasingly sophisticated software components, employing machine learning to create devices that perform activities once exclusively carried out by humans. Since these activities may involve significant risks and responsibilities, ensuring the correctness and safety of involved software components is crucial. Probabilistic Programs (PPs) are often employed in AI-powered software, particularly to exploit Bayesian inference, and to model randomized algorithms. Thus, studying verification of PPs can enable verification techniques for ensuring safety and correctness of AI-powered programs. PPs are computer programs that, besides ordinary programming constructs, may contain random choices, and variable assignments according to a random distribution.The CORPORA (COntext-free model checking for Recursive PrObabilistic pRogrAms) project aims at developing new techniques for the verification of Recursive Probabilistic Programs, one of the most expressive classes of PPs. Recursive PPs may contain recursive procedures. Since procedures are governed by a stack, they exhibit a context-free behavior in execution traces: verification of procedural programs has motivated the study of model checking pushdown formalisms. The need for specifying properties concerning the stacks contents has led to the introduction of ad-hoc specification formalisms, including temporal logics featuring context-free-aware modalities, such as CaRet, NWTL and POTL, the latter being introduced by the applicant during his Ph.D.The CORPORA project will extend the context-free model checking framework to recursive PPs, and its research objectives will encompass the theoretical and practical study of model checking thereof. The projects expected results include a model checker for context-free properties of recursive PPs, which will enable the practical evaluation of the techniques developed in the project.
Original text from CORDIS.
Participants
- TECHNISCHE UNIVERSITAET WIEN · WienCoordinatorAustria
Links
- View on CORDIS
- DOI: 10.3030/101107303
- https://ec.europa.eu/research/participants/documents/downloadPublic?documentIds=080166e507ff1908&appId=PPGMS
- https://ec.europa.eu/research/participants/documents/downloadPublic?documentIds=080166e520333c26&appId=PPGMS
Data: CORDIS, © European Union