SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 13:50 - 14:05 at Zurich G - OOPSLA and Onward! 2020 Papers 2 Chair(s): Michael Coblenz

Computer programs are increasingly being deployed in partially-observable environments. A partially observable environment is an environment whose state is not completely visible to the program, but from which the program receives partial information in the form of observations. Developers typically deal with partial observability by writing a state estimator that, given observations, attempts to deduce the hidden state of the environment. In safety-critical domains, to formally verify safety properties developers may write an environment model. The model captures the relationship between observations and hidden states and is used to prove the software correct.

In this paper, we present a new methodology for writing and verifying programs in partially observable environments. We present belief programming, a programming methodology where developers write an environment model that the program runtime automatically uses to perform state estimation. A belief program dynamically updates and queries a belief state that captures the possible states the environment could be in. To enable verification, we present epistemic Hoare logic that reasons about the possible belief states of a belief program the same way that classical Hoare logic reasons about the possible states of a program. We develop these concepts by defining a semantics and a program logic for a simple core language called BLIMP. In a case study, we show how belief programming could be used to write and verify a controller for the Mars Polar Lander in BLIMP.

Wed 20 Oct

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

13:50 - 15:10
OOPSLA and Onward! 2020 Papers 2SIGPLAN Papers at Zurich G
Chair(s): Michael Coblenz University of Maryland at College Park
13:50
15m
Talk
Programming and Reasoning with Partial Observability
SIGPLAN Papers
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
14:05
15m
Talk
Pomsets with Preconditions: A Simple Model of Relaxed Memory
SIGPLAN Papers
Radha Jagadeesan DePaul University, Alan Jeffrey Roblox, James Riely DePaul University
14:20
15m
Talk
Koord: a language for programming and verifying distributed robotics applications
SIGPLAN Papers
Ritwika Ghosh University of Illinois at Urbana-Champaign, Chiao Hsieh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign
14:35
15m
Paper
Demystifying Dependence
SIGPLAN Papers
James Koppel Massachusetts Institute of Technology, USA, Daniel Jackson MIT
Link to publication Pre-print
14:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers