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 Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
10:35 - 12:03: Reasoning about Probabilistic ProgramsResearch Papers at Sala I Chair(s): Jan HoffmannCarnegie Mellon University | |||
10:35 - 10:57 Talk | Formal Verification of Higher-Order Probabilistic Programs Research Papers Tetsuya SatoUniversity at Buffalo, SUNY, USA, Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Justin HsuUniversity of Wisconsin-Madison, USA Link to publication DOI Media Attached File Attached | ||
10:57 - 11:19 Talk | A Separation Logic for Concurrent Randomized Programs Research Papers Link to publication DOI Media Attached File Attached | ||
11:19 - 11:41 Talk | Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs Research Papers Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaRWTH Aachen University, Thomas NollRWTH Aachen University Link to publication DOI Media Attached File Attached | ||
11:41 - 12:03 Talk | Trace Abstraction Modulo Probability Research Papers Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison Link to publication DOI Media Attached |