Christoph Matheja will give a talk about his work on Towards an Intermediate Verification Language for Probabilistic Programs. Details below.
SPEAKER
Christoph Matheja, Assit. Prof., DTU.
TITLE
Towards an Intermediate Verification Language for Probabilistic Programs
ABSTRACT
Probabilistic programs offer a structured way to describe computations with access to a source of randomness. They appear naturally in the design of efficient algorithms, security protocols, and, more recently, as modeling languages used in planning and artificial intelligence.
While the semantics of probabilistic programs has been studied since the early 80s, renewed interest in probabilistic models led to new program logics and proof rules targeting probabilistic programs in recent years. However, a comprehensive methodology for reasoning about probabilistic programs is still in its infancy: most of the new proof systems are not automated; few are mechanized. Moreover, combining different proof systems is difficult due to the lack of common foundations.
In this talk, I will present ongoing work on developing an intermediate verification language, similar to Boogie, Dafny, or Viper, for (discrete) probabilistic programs, in which various reasoning techniques can be described and automated.