Wed 18 Nov 2020 05:20 - 05:40 at SPLASH-III - T-6B Chair(s): Olivier Flückiger, Sorav Bansal
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 Times are displayed in time zone: Central Time (US & Canada) change
17:00 - 18:20: T-6BOOPSLA at SPLASH-III +12h Chair(s): Todd MillsteinUniversity of California at Los Angeles, Manu SridharanUniversity of California at Riverside | |||
17:00 - 17:20 Talk | DynamiTe: Dynamic Termination and Non-termination Proofs OOPSLA Ton Chanh LeStevens Institute of Technology, Timos AntonopoulosYale University, Parisa FathololumiStevens Institute of Technology, Eric KoskinenStevens Institute of Technology, ThanhVu NguyenUniversity of Nebraska-Lincoln Link to publication DOI Media Attached | ||
17:20 - 17:40 Talk | Programming and Reasoning with Partial Observability OOPSLA Eric AtkinsonMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology Link to publication DOI Media Attached | ||
17:40 - 18:00 Talk | World Age in Julia: Optimizing Method Dispatch in the Presence of Eval OOPSLA Julia BelyakovaNortheastern University, Benjamin ChungNortheastern University, Jack GelinasNortheastern University, Jameson NashJulia Computing, Ross TateCornell University, Jan VitekNortheastern University / Czech Technical University Link to publication DOI Media Attached | ||
18:00 - 18:20 Talk | Featherweight Go OOPSLA Robert GriesemerGoogle, Raymond HuUniversity of Hertfordshire, Wen KokkeUniversity of Edinburgh, Julien LangeRoyal Holloway University of London, Ian Lance TaylorGoogle, Bernardo ToninhoNova University of Lisbon / NOVA-LINCS, Philip WadlerUniversity of Edinburgh, Nobuko YoshidaImperial College London Link to publication DOI Media Attached |
Wed 18 Nov Times are displayed in time zone: Central Time (US & Canada) change
05:00 - 06:20: T-6BOOPSLA at SPLASH-III Chair(s): Olivier FlückigerNortheastern University, Sorav BansalIIT Delhi | |||
05:00 - 05:20 Talk | DynamiTe: Dynamic Termination and Non-termination Proofs OOPSLA Ton Chanh LeStevens Institute of Technology, Timos AntonopoulosYale University, Parisa FathololumiStevens Institute of Technology, Eric KoskinenStevens Institute of Technology, ThanhVu NguyenUniversity of Nebraska-Lincoln Link to publication DOI Media Attached | ||
05:20 - 05:40 Talk | Programming and Reasoning with Partial Observability OOPSLA Eric AtkinsonMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology Link to publication DOI Media Attached | ||
05:40 - 06:00 Talk | World Age in Julia: Optimizing Method Dispatch in the Presence of Eval OOPSLA Julia BelyakovaNortheastern University, Benjamin ChungNortheastern University, Jack GelinasNortheastern University, Jameson NashJulia Computing, Ross TateCornell University, Jan VitekNortheastern University / Czech Technical University Link to publication DOI Media Attached | ||
06:00 - 06:20 Talk | Featherweight Go OOPSLA Robert GriesemerGoogle, Raymond HuUniversity of Hertfordshire, Wen KokkeUniversity of Edinburgh, Julien LangeRoyal Holloway University of London, Ian Lance TaylorGoogle, Bernardo ToninhoNova University of Lisbon / NOVA-LINCS, Philip WadlerUniversity of Edinburgh, Nobuko YoshidaImperial College London Link to publication DOI Media Attached |