SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 17:20 - 17:40 at SPLASH-III - T-6B Chair(s): Todd Millstein, Manu Sridharan
Wed 18 Nov 2020 05:20 - 05:40 at SPLASH-III - T-6B Chair(s): Sorav Bansal, Olivier Fl├╝ckiger

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 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. We present an implementation of BLIMP called CBLIMP and evaluate it to determine the feasibility of belief programming.

Tue 17 Nov

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

17:00 - 18:20
T-6BOOPSLA at SPLASH-III +12h
Chair(s): Todd Millstein University of California at Los Angeles, Manu Sridharan University of California at Riverside
17:00
20m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
OOPSLA
Ton Chanh Le Stevens Institute of Technology, Timos Antonopoulos Yale University, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, ThanhVu Nguyen University of Nebraska-Lincoln
Link to publication DOI Media Attached
17:20
20m
Talk
Programming and Reasoning with Partial Observability
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Media Attached
17:40
20m
Talk
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
OOPSLA
Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Jack Gelinas Northeastern University, Jameson Nash Julia Computing, Ross Tate Cornell University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Media Attached
18:00
20m
Talk
Featherweight Go
OOPSLA
Robert Griesemer Google, Raymond Hu University of Hertfordshire, Wen Kokke University of Edinburgh, Julien Lange Royal Holloway University of London, Ian Lance Taylor Google, Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Philip Wadler University of Edinburgh, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached

Wed 18 Nov

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

05:00 - 06:20
T-6BOOPSLA at SPLASH-III
Chair(s): Sorav Bansal IIT Delhi, Olivier Fl├╝ckiger Northeastern University
05:00
20m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
OOPSLA
Ton Chanh Le Stevens Institute of Technology, Timos Antonopoulos Yale University, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, ThanhVu Nguyen University of Nebraska-Lincoln
Link to publication DOI Media Attached
05:20
20m
Talk
Programming and Reasoning with Partial Observability
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Media Attached
05:40
20m
Talk
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
OOPSLA
Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Jack Gelinas Northeastern University, Jameson Nash Julia Computing, Ross Tate Cornell University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Media Attached
06:00
20m
Talk
Featherweight Go
OOPSLA
Robert Griesemer Google, Raymond Hu University of Hertfordshire, Wen Kokke University of Edinburgh, Julien Lange Royal Holloway University of London, Ian Lance Taylor Google, Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Philip Wadler University of Edinburgh, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached