Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 10:57 - 11:19 at Sala I - Reasoning about Probabilistic Programs Chair(s): Jan Hoffmann

We present a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate our logic, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.

Slides (talk.pdf)171KiB

Wed 16 Jan

Displayed time zone: Belfast change

10:35 - 12:03
Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan Hoffmann Carnegie Mellon University
10:35
22m
Talk
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
A Separation Logic for Concurrent Randomized Programs
Research Papers
Joseph Tassarotti Carnegie Mellon University, Robert Harper
Link to publication DOI Media Attached File Attached
11:19
22m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Research Papers
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
Link to publication DOI Media Attached File Attached
11:41
22m
Talk
Trace Abstraction Modulo Probability
Research Papers
Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison
Link to publication DOI Media Attached