h1

h2

h3

h4

h5
h6

FRAPPANT

Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation

CoordinatorRWTH Aachen University
Grant period2018-11-01 - 2024-10-31
Funding bodyEuropean Union
Call numberERC-2017-ADG
Grant number787914
IdentifierG:(EU-Grant)787914

Note: Probabilistic programs describe recipes on how to infer statistical conclusions about data from a complex mixture of uncertain data and real-world observations. They can represent probabilistic graphical models far beyond the capabilities of Bayesian networks and are expected to have a major impact on machine intelligence. Probabilistic programs are ubiquitous. They steer autonomous robots and self-driving cars, are key to describe security mechanisms, naturally code up randomised algorithms for solving NP-hard problems, and are rapidly encroaching AI. Probabilistic programming aims to make probabilistic modeling and machine learning accessible to the programmer. Probabilistic programs, though typically relatively small in size, are hard to grasp, let alone automatically checkable. Are they doing the right thing? What’s their precision? These questions are notoriously hard — even the most elementary question “does a program halt with probability one?” is “more undecidable” than the halting problem — and can (if at all) be answered with statistical evidence only. Bugs thus easily occur. Hard guarantees are called for. The objective of this project is to enable predictable probabilistic programming. We do so by developing formal verification techniques. Whereas program correctness is pivotal in computer science, the formal verification of probabilistic programs is in its infancy. The project aims to fill this barren landscape by developing program analysis techniques, leveraging model checking, deductive verification, and static analysis. Challenging problems such as checking program equivalence, loop-invariant and parameter synthesis, program repair, program robustness and exact inference using weakest precondition reasoning will be tackled. The techniques will be evaluated in the context of probabilistic graphical models, randomised algorithms, and autonomous robots. FRAPPANT will spearhead formally verifiable probabilistic programming.
     

Recent Publications

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

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Dissertation / PhD Thesis  ;  ;
Automated deductive verification of probabilistic programs
Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen () [10.18154/RWTH-2025-00473] = Dissertation, RWTH Aachen University, 2024  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Dissertation / PhD Thesis  ;  ;
Probabilistic model checking and parameter tuning for Bayesian networks
Aachen : RWTH Aachen University 1 Online-Ressource : Illustrationen () [10.18154/RWTH-2025-00411] = Dissertation, RWTH Aachen University, 2024  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book  ;  ;  ;
J-P: MDP. FP. PP: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs
Principles of verification: cycling the probabilistic landscape, [Bd.] Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors Cham : Springer, Lecture notes in computer science 15260, 255-302 () [10.1007/978-3-031-75783-9_11]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book  ;  ;  ;
Symbolic Quantitative Information Flow for Probabilistic Programs
Principles of verification: cycling the probabilistic landscape, [Bd.] Part 1 / Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, Matthias Volk, editors Cham : Springer, Lecture notes in computer science 15260, 128-154 () [10.1007/978-3-031-75783-9_6]  GO  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article/Contribution to a conference proceedings  ;  ;  ;  ;
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
ACM Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2024, PasadenaPasadena, USA, 20 Oct 2024 - 25 Oct 20242024-10-202024-10-25 Proceedings of the ACM on programming languages : (PACMPL) 8(OOPSLA1), 127 () [10.1145/3649844] special issue: "OOPSLA1"  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Preprint  ;  ;  ;  ;
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
ACM Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA24, PasadenaPasadena, USA, 20 Oct 2024 - 25 Oct 20242024-10-202024-10-25 54 Seiten () [10.48550/ARXIV.2307.07314]  GO arXiv  Download fulltext Files  Download fulltextFulltext by arXiv.org BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article/Contribution to a conference proceedings  ;  ;  ;
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Symposium on Principles of Programming Languages, POPL 2024, LondonLondon, UK, 17 Jan 2024 - 19 Jan 20242024-01-172024-01-19 Proceedings of the ACM on programming languages : (PACMPL) 8, 93 () [10.1145/3632935] special issue: "POPL"  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence : Macao, SAR, 19-25 August 2023 / edited by Edith Elkind ; sponsored by International Joint Conferences on Artifical Intelligence (IJCAI), published by International Joint Conferences on Artificial Intelligence
32. International Joint Conference on Artificial Intelligence, IJCAI 2023, MacauMacau, Macau, 19 Aug 2023 - 25 Aug 20232023-08-192023-08-25 Vienna, Austria : International Joint Conferences on Artificial Intelligence () [10.24963/ijcai.2023/635]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Preprint  ;  ;  ;  ;
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
[1]-48 () [10.48550/arXiv.2309.07781]  GO OpenAccess  Download fulltext Files  Download fulltextFulltext by arXiv.org BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article/Contribution to a conference proceedings  ;  ;  ;  ;
A Deductive Verification Infrastructure for Probabilistic Programs
International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2023, CascaisCascais, Portugal, 22 Oct 2023 - 27 Oct 20232023-10-222023-10-27
Object-Oriented Programming, Systems, Languages & Applications, OOPSLA 2023, CascaisCascais, Portugal, 22 Oct 2023 - 27 Oct 20232023-10-222023-10-27 Proceedings of the ACM on programming languages 7(OOPSLA2), 294 () [10.1145/3622870] special issue: "OOPSLA2"  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

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

 Record created 2018-06-26, last modified 2023-02-09
Similar records



Rate this document:

Rate this document:
1
2
3
4
5
 
(Not yet reviewed)