xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 14:00 - 14:30 at Seminar Room G007 - Logic and Verification II

We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2) weighting execution traces. Weights can be numbers but also other objects like words from an alphabet, polynomials, formal power series, or cardinal numbers. We argue that weighted programming as a paradigm can be used to specify mathematical models beyond probability distributions (as is done in probabilistic programming). We develop weakest-precondition- and weakest-liberal-precondition-style calculi à la Dijkstra for reasoning about mathematical models specified by weighted programs. We present several case studies. For instance, we use weighted programming to model the ski rental problem — an optimization problem. We model not only the optimization problem itself, but also the best deterministic online algorithm for solving this problem as weighted programs. By means of weakest-precondition-style reasoning, we can determine the competitive ratio of the online algorithm on source code level.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Logic and Verification IIOOPSLA at Seminar Room G007
13:30
30m
Research paper
On incorrectness logic for Quantum programs
OOPSLA
Peng Yan University of Technology Sydney, Hanru Jiang Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, China, Nengkun Yu Stony Brook University, USA
DOI
14:00
30m
Research paper
Weighted programming: a programming paradigm for specifying mathematical models
OOPSLA
Kevin Batz RWTH Aachen University, Adrian Gallus RWTH Aachen University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
DOI
14:30
30m
Talk
Wildcards Need Witness Protection
OOPSLA
DOI
Hide past events