POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

We put forward an approach to the semantics of probabilistic program- ming centered on an action-based language equipped with a small-step operational semantics. This approach provides benefits in terms of both clarity and effective implementation. Discrete and continuous distributions can be freely mixed, un- bounded loops are allowed. In measure-theoretic terms, a product of Markov kernels is used to formalize the small-step operational semantics. A distinctive feature of this approach is that it directly leads to an exact sampling algorithm that can be efficiently SIMD-parallelized. An observational semantics is also in- troduced based on a probability space of infinite sequences, along with a finite approximation theorem. Preliminary experiments with a proof-of-concept imple- mentation based on TensorFlow show that our approach compares favourably to state-of-the-art tools for probabilistic programming and inference.

Tue 16 Jan

Displayed time zone: London change

14:00 - 15:30
Session 7: Probabilistic and Quantum Programs, Neural NetworksVMCAI at Marconi Room
Chair(s): Andreas Podelski University of Freiburg
14:00
20m
Talk
Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
VMCAI
Michele Boreale UniversitĂ  di Firenze, Luisa Collodi University of Florence
14:20
20m
Talk
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
VMCAI
Yuxin Deng East China Normal University, Huiling Wu East China Normal University, Ming Xu East China Normal University
14:40
20m
Talk
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
VMCAI
Jiaxu Tian East China Normal University, Dapeng Zhi East China Normal University, Si Liu ETH Zurich, Peixin Wang University of Oxford, Guy Katz Hebrew University, Min Zhang East China Normal University
15:00
20m
Talk
Verification of Neural Networks’ Local Differential Classification Privacy
VMCAI
Roie Reshef Technion, Anan Kabaha Technion, Israel Institute of Technology, Olga Seleznova Technion, Dana Drachsler Cohen Technion
15:20
10m
Talk
AGNES: Abstraction-guided Framework for Deep Neural Networks Security
VMCAI