In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.
Tue 20 JunDisplayed time zone: Eastern Time (US & Canada) change
13:40 - 15:40 | PLDI: Probabilistic AnalysesPLDI Research Papers at Royal Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign | ||
13:40 20mTalk | Lilac: A Modal Separation Logic for Conditional Probability PLDI Research Papers John Li Northeastern University, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University DOI Pre-print | ||
14:00 20mTalk | Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning PLDI Research Papers Alexander Bagnall Ohio University, Gordon Stewart Bedrock Systems, Anindya Banerjee IMDEA Software Institute DOI | ||
14:20 20mTalk | Verified Density Compilation for a Probabilistic Programming Language PLDI Research Papers DOI | ||
14:40 20mTalk | Probabilistic Programming with Stochastic Probabilities PLDI Research Papers Alexander K. Lew Massachusetts Institute of Technology, Matin Ghavami Massachusetts Institute of Technology, Martin Rinard MIT, Vikash K. Mansinghka Massachusetts Institute of Technology DOI | ||
15:00 20mTalk | Automated Expected Value Analysis of Recursive Programs PLDI Research Papers DOI | ||
15:20 20mTalk | Synthesizing Quantum-Circuit Optimizers PLDI Research Papers Amanda Xu University of Wisconsin-Madison, Abtin Molavi University of Wisconsin-Madison, Lauren Pick University of Wisconsin-Madison and University of California, Berkeley, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI Pre-print |