{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:56:00Z","timestamp":1762102560749,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2699"],"award-info":[{"award-number":["N00014-17-1-2699"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>\n            In this paper, we present a new methodology for writing and verifying programs in partially observable environments. We present\n            <jats:italic>belief programming<\/jats:italic>\n            , 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\n            <jats:italic>Epistemic Hoare Logic<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3428268","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Programming and reasoning with partial observability"],"prefix":"10.1145","volume":"4","author":[{"given":"Eric","family":"Atkinson","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Carbin","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"volume-title":"Software, Services, and Systems","author":"Areces Carlos","key":"e_1_2_2_1_1"},{"volume-title":"Moss","year":"2004","author":"Baltag Alexandru","key":"e_1_2_2_3_1"},{"volume-title":"Reactive Probabilistic Programming. In Conference on Programming Language Design and Implementation.","year":"2020","author":"Baudart Guillaume","key":"e_1_2_2_4_1"},{"volume-title":"AAAI Conference on Artificial Intelligence.","year":"2017","author":"Caridroit Thomas","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Souray Chatterjee and Persi Diaconis. 2018. The Sample Size Required in Importance Sampling. Annals of Applied Probability 28 (04 2018 ) 1099-1135. Issue 2.  Souray Chatterjee and Persi Diaconis. 2018. The Sample Size Required in Importance Sampling. Annals of Applied Probability 28 (04 2018 ) 1099-1135. Issue 2.","DOI":"10.1214\/17-AAP1326"},{"key":"e_1_2_2_8_1","series-title":"Series II 9 ( 1938 )","first-page":"326","volume-title":"Calcolo aprossimato per le souzioni dei sistemi di equazioni lineari. La Ricera Scientifica","author":"Cimmino G."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.214546"},{"volume-title":"Carlin","year":"1996","author":"Cowles Mary Kathryn","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Pierre Del Moral Arnaud Doucet and Ajay Jasra. 2006. Sequential Monte Carlo samplers. Journal of the Royal Statistical Society: Series B (Statistical Methodology) 68 (06 2006 ) 411-436. Issue 3.  Pierre Del Moral Arnaud Doucet and Ajay Jasra. 2006. Sequential Monte Carlo samplers. Journal of the Royal Statistical Society: Series B (Statistical Methodology) 68 (06 2006 ) 411-436. Issue 3.","DOI":"10.1111\/j.1467-9868.2006.00553.x"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Edsger W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivations of Programs. Commun. ACM 18 ( 08 1975 ) 453-457. Issue 8.  Edsger W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivations of Programs. Commun. ACM 18 ( 08 1975 ) 453-457. Issue 8.","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12 ( 10 1969 ) 576-580. Issue 10.  C.A.R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12 ( 10 1969 ) 576-580. Issue 10.","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_17_1","unstructured":"JPL Special Review Board. 200"},{"key":"e_1_2_2_18_1","unstructured":"Stefan Kaczmarz. 1937. Angenaherte Auflosung von Systemen linearer Gleichungen. In Bulletin International de l' Academie Polonaise des Sciences et des Lettres. Classe des Sciences Mathematiques et Naturelles. Serie A Sciences Mathematiques.  Stefan Kaczmarz. 1937. Angenaherte Auflosung von Systemen linearer Gleichungen. In Bulletin International de l' Academie Polonaise des Sciences et des Lettres. Classe des Sciences Mathematiques et Naturelles. Serie A Sciences Mathematiques."},{"volume-title":"International Conference on Machine Learning.","author":"Lau Tessa","key":"e_1_2_2_19_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Jun S. Liu. 1996. Metropolized Independent Sampling with Comparisons to Rejection Sampling and Importance Sampling. Statistics and Computing 6 ( 06 1996 ) 113-119.  Jun S. Liu. 1996. Metropolized Independent Sampling with Comparisons to Rejection Sampling and Importance Sampling. Statistics and Computing 6 ( 06 1996 ) 113-119.","DOI":"10.1007\/BF00162521"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Eficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems.  Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Eficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Jan Plaza. 2007. Logics of Public Communications. Synthese 158 (09 2007 ) 165-179.  Jan Plaza. 2007. Logics of Public Communications. Synthese 158 (09 2007 ) 165-179.","DOI":"10.1007\/s11229-007-9168-7"},{"volume-title":"Artificial Intelligence: A Modern Approach (4 ed.). Pearson.","year":"2020","author":"Russel Stuart","key":"e_1_2_2_23_1"},{"volume-title":"Falling Back on Executable Specification Languages. In European Conference Object-Oriented Programming.","year":"2010","author":"Samimi Hesam","key":"e_1_2_2_24_1"},{"volume-title":"Expressing and Verifying Probabilistic Assertions. In Conference on Programming Language Design and Implementation.","year":"2014","author":"Sampson Adrian","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290351"},{"volume-title":"Uncertain Dynamic Systems","author":"Schweppe Fred C.","key":"e_1_2_2_27_1"},{"volume":"197","journal-title":"Edward J. Sondik.","author":"Smallwood Richard D.","key":"e_1_2_2_28_1"},{"volume-title":"Combinatorial Sketching for Finite Programs. In International Conference on Architectural Support for Programming Languages and Operating Systems.","year":"2006","author":"Solar-Lezama Armando","key":"e_1_2_2_29_1"},{"key":"e_1_2_2_30_1","unstructured":"Sparkfun. 2020. GPS Buying Guide-SparkFun Electronics. https:\/\/www.sparkfun.com\/GPS_Guide. Accessed 2020-07-16.  Sparkfun. 2020. GPS Buying Guide-SparkFun Electronics. https:\/\/www.sparkfun.com\/GPS_Guide. Accessed 2020-07-16."},{"volume-title":"Commutative Semantics for Probabilistic Programming. In European Symposium on Programming.","year":"2017","author":"Staton Sam","key":"e_1_2_2_31_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2816262"},{"volume-title":"The Formal Semantics of Programming Languages","author":"Winskel Glynn","key":"e_1_2_2_33_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103669"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428268","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428268","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":32,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428268"],"URL":"https:\/\/doi.org\/10.1145\/3428268","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}