ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Fri 10 Jun 2022 14:10 - 14:30 at Aurora Borealis 1 - Program Analysis 2 Chair(s): Quentin Stiévenart

This paper presents the first slicing approach for probabilistic programs based on specifications. We show that when probabilistic programs are accompanied by their specifications in the form of pre- and post-condition, we can exploit this semantic information to produce specification-preserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency.

To achieve this goal, our technique is based on the backward propagation of post-conditions via the greatest pre-expectation transformer—the probabilistic counterpart of Dijkstra weakest pre-condition transformer. The technique is termination-sensitive, allowing to preserve the partial as well as the total correctness of probabilistic programs w.r.t. their specifications. It is modular, featuring a local reasoning principle, and is formally proved correct.

As fundamental technical ingredients of our technique, we design and prove sound verification condition generators for establishing the partial and total correctness of probabilistic programs, which are of interest on their own and can be exploited elsewhere for other purposes.

On the practical side, we demonstrate the applicability of our approach by means of illustrative examples and present an algorithm for computing least slices among the space of slices derived by our technique.

Fri 10 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Program Analysis 2Research Papers / Hub Talks at Aurora Borealis 1
Chair(s): Quentin Stiévenart Vrije Universiteit Brussel
Low-Level Bi-AbductionArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalECOOP 2022
Research Papers
Lukáš Holík Brno University of Technology, Petr Peringer Brno University of Technology, Adam Rogalewicz Brno University of Technology, Faculty of Information Technology, Veronika Šoková Brno University of Technology, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna
On the computation of interprocedural weak control closureHub Talk
Hub Talks
Abu Naser Masud Malardalen University
Link to publication DOI
Slicing of Probabilistic Programs based on SpecificationsECOOP 2022
Research Papers
Federico Olmedo University of Chile & IMFD Chile
A Deterministic Memory Allocator for Dynamic Symbolic ExecutionArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Daniel Schemmel Imperial College London, Julian Büning RWTH Aachen University, Frank Busse Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College London, UK