We are happy to announce that RWTH's MOVES group, headed by Prof. Joost-Pieter Katoen, will receive funding from the European Research Council (ERC) for a Proof of Concept Grant to improve Caesar.

Caesar was originally built in part through FRAPPANT, the 2018 ERC Advanced Grant "Formal Reasoning about Probabilistic Programs: Breaking New Ground for Automation". The new ERC Proof of Concept research proposal "A Deductive Verifier for Probabilistic Programs (VERIPROB)" is about applying knowledge from FRAPPANT to build Caesar into a prototype that can be made use of by industry — "to turn science into practice".

See also the press release by the university and the ERC announcement.

On January 14, 2024, I presented Caesar and the basics of our quantitative intermediate language HeyVL at the Dafny 2024 workshop. The workshop was part of the POPL 2024 conference.

The talk starts at timestamp 7:16:23 and ends at timestamp 7:34:00.

The artifact associated with our OOPSLA '23 publication A Deductive Verification Infrastructure for Probabilistic Programs has received the Distinguished Artifact award, praising exceptionally high quality. The artifact consists the tool Caesar together with benchmark examples.

The artifact has a page in the ACM Digital Library and can be downloaded from Zenodo.

HeyVL and Caesar were accepted at OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs by Schröer et al. The artifact received the reusable badge, which is the highest possible badge.

The preprint is available on arxiv: https://arxiv.org/abs/2309.07781.

You can find more information on our publications page.

Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.