Datensatz #1024264 - RWTH Publications

G:(EU-Grant) 101158076

VERIPROB: a deductive verifier for probabilistic programs Andere Formen:A deductive verifier for probabilistic programs

Grant period	2024-11-01 - 2026-04-30
Funding body	European Union
	CORDIS
Grant number	101158076
Further information:	Homepage
Identifier	G:(EU-Grant)101158076

Note: 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. 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, and neural network training. 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 has resulted in proof calculi for probabilistic programs, equipped with powerful proof rules, and identified a relative 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 a commercialisation by including invariant synthesis and program slicing and supporting the popular probabilistic programming language STAN. Its potential will be investigated engaging potential users, and a market analysis.

Recent Publications

All known publications ...
Download: BibTeX | EndNote XML, Text | RIS |

Contribution to a book/Contribution to a conference proceedings Haase, D. (Corresponding author)RWTH* ; Batz, K. ; Gallus, A. ; Kaminski, B. L. ; Katoen, J.-P.RWTH* ; Klinkenberg, L.RWTH* ; Winkler, T.RWTH*
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
2026Programming languages and systems : 35th European Symposium on Programming, ESOP 2026 : held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026 : proceedings, part I / Robbert Krebbers, editor
35. European Symposium on Programming, ESOP 2026, TurinTurin, Italy, 14 Apr 2026 - 16 Apr 20262026-04-142026-04-16
29. International Joint Conferences on Theory and Practice of Software, ETAPS 2026, TurinTurin, Italy, 11 Apr 2026 - 16 Apr 20262026-04-112026-04-16 Cham : Springer, Lecture notes in computer science 16501, Advanced Research in Computing and Software Science 314-343 (2026) [10.1007/978-3-032-22720-1_12]2026 OpenAccess Files BibTeX | EndNote: XML, Text | RIS

Contribution to a book/Contribution to a conference proceedings Schroer, P. (Corresponding author)RWTH* ; Katoen, J.-P.RWTH*
Highly Incremental: A Simple Programmatic Approach for Many Objectives
2026Formal Methods : 27th International Symposium, FM 2026, Tokyo, Japan, May 18–22, 2026, Proceedings, Part I / edited by Augusto Sampaio, Marielle Stoelinga
27. International Symposium on Formal Methods, FM 2026, TokyoTokyo, Japan, 18 May 2026 - 22 May 20262026-05-182026-05-22 Cham : Springer Nature Switzerland, Lecture Notes in Computer Science 16556, 559-577 (2026) [10.1007/978-3-032-26204-2_29]2026 OpenAccess Files BibTeX | EndNote: XML, Text | RIS