This program is tentative and subject to change.

Wed 23 Oct 2024 14:20 - 14:40 at San Gabriel - Formal Methods 1 Chair(s): Benjamin Delaware

We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i)~obtain a weakest pre calculus for hyper Hoare logic and (ii)~enable reasoning about so-called \emph{hyperquantities} which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.

This program is tentative and subject to change.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Formal Methods 1OOPSLA 2024 at San Gabriel
Chair(s): Benjamin Delaware Purdue University
13:40
20m
Talk
Realistic Realizability: Specifying ABIs You Can Count On
OOPSLA 2024
Andrew Wagner Northeastern University, Zachary Eisbach Northeastern University, Amal Ahmed Northeastern University, USA
14:00
20m
Talk
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
OOPSLA 2024
Robert Schenck DIKU, University of Copenhagen, Nikolaj Hey Hinnerskov DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Magnus Madsen Aarhus University, Martin Elsman University of Copenhagen
14:20
20m
Talk
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
OOPSLA 2024
Linpeng Zhang University College London, Noam Zilberstein Cornell University, Benjamin Lucien Kaminski Saarland University; University College London, Alexandra Silva Cornell University
14:40
20m
Talk
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
OOPSLA 2024
Yichuan Li Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University
15:00
20m
Talk
Weighted Context-Free-Language Ordered Binary Decision Diagrams
OOPSLA 2024
Meghana Aparna Sistla The University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Thomas Reps University of Wisconsin-Madison