Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 11:45 - 12:07 at Olympia - Modular Verification Chair(s): Friedrich Steimann

In this work, we consider the almost-sure termination problem for probabilistic programs that asks
whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the
foundation for modular analysis. Extension of this rule to almost-sure termination of probabilistic programs is quite tricky, and a probabilistic variant was proposed by Fioriti and Hermanns in POPL 2015.
While the proposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed modular rule is still not sound for almost-sure termination of probabilistic programs.

Besides establishing unsoundness of the previous rule, our contributions are as follows:
First, we present a sound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel notion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales that are linear and show that they
can be synthesized in polynomial time. Finally, we present experimental results on a variety of benchmarks and several natural examples that model various types of
nested while loops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure termination property.

Wed 23 Oct

Displayed time zone: Beirut change

11:00 - 12:30
Modular VerificationOOPSLA at Olympia
Chair(s): Friedrich Steimann Fernuni Hagen
11:00
22m
Research paper
Modular Verification of Heap Reachability Properties in Separation Logic
OOPSLA
Link to publication DOI Pre-print File Attached
11:22
22m
Talk
Modular Verification of Web Page Layout
OOPSLA
Pavel Panchekha University of Utah, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle, Shoaib Kamil Adobe
DOI
11:45
22m
Talk
Modular Verification for Almost-Sure Termination of Probabilistic Programs
OOPSLA
Mingzhang Huang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST Austria
DOI
12:07
22m
Talk
Leveraging Rust Types for Modular Specification and Verification
OOPSLA
Vytautas Astrauskas ETH Zurich, Switzerland, Peter Müller ETH Zurich, Federico Poli ETH Zurich, Switzerland, Alexander J. Summers ETH Zurich
DOI Pre-print