{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:15Z","timestamp":1750220835710,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T00:00:00Z","timestamp":1565222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,8]]},"DOI":"10.1145\/3331545.3342593","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"139-145","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal verification of spacecraft control programs (experience report)"],"prefix":"10.1145","author":[{"given":"Andrey","family":"Mokhov","sequence":"first","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georgy","family":"Lukyanov","sequence":"additional","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Lechner","sequence":"additional","affiliation":[{"name":"RUAG Space, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,8,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/571922.571958"},{"key":"e_1_3_2_1_3_1","volume-title":"a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23 (9","author":"Brady Edwin","year":"2013","unstructured":"Edwin Brady . 2013. Idris , a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23 (9 2013 ), 552\u2013593. Issue 05. Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23 (9 2013), 552\u2013593. Issue 05."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-005-0004-8"},{"key":"e_1_3_2_1_5_1","volume-title":"Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems ( 2008 ), 337\u2013340. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems (2008), 337\u2013340."},{"key":"e_1_3_2_1_7_1","unstructured":"Stephen Diehl. 2017. Monads to Machine Code. https:\/\/web.archive.org\/ web\/20171207020256\/http:\/\/www.stephendiehl.com\/posts\/monads_ machine_code.html .  Stephen Diehl. 2017. Monads to Machine Code. https:\/\/web.archive.org\/ web\/20171207020256\/http:\/\/www.stephendiehl.com\/posts\/monads_ machine_code.html ."},{"key":"e_1_3_2_1_8_1","volume-title":"SBV: SMT Based Verification in Haskell","author":"Erkok Levent","year":"2019","unstructured":"Levent Erkok . 2019 . SBV: SMT Based Verification in Haskell . http:\/\/ leventerkok.github.io\/sbv\/ Levent Erkok. 2019. SBV: SMT Based Verification in Haskell. http:\/\/ leventerkok.github.io\/sbv\/"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_10_1","unstructured":"Tikhon Jelvis. 2016. Analyzing Programs with Z3 (video recording of Compose Conference talk). https:\/\/web.archive.org\/web\/20170205204536\/http: \/\/jelv.is\/talks\/compose-2016\/ .  Tikhon Jelvis. 2016. Analyzing Programs with Z3 (video recording of Compose Conference talk). https:\/\/web.archive.org\/web\/20170205204536\/http: \/\/jelv.is\/talks\/compose-2016\/ ."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.11950"},{"key":"e_1_3_2_1_13_1","unstructured":"MIT. 2017. A formal specification of the RISC-V ISA written in Haskell. https:\/\/github.com\/mit-plv\/riscv-semantics .  MIT. 2017. A formal specification of the RISC-V ISA written in Haskell. https:\/\/github.com\/mit-plv\/riscv-semantics ."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133912"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_3_2_1_19_1","unstructured":"Lewis Wall. 2017. An ASM Monad. https:\/\/web.archive.org\/web\/ 20190519181416\/http:\/\/wall.org\/~lewis\/2013\/10\/15\/asm-monad.html .  Lewis Wall. 2017. An ASM Monad. https:\/\/web.archive.org\/web\/ 20190519181416\/http:\/\/wall.org\/~lewis\/2013\/10\/15\/asm-monad.html ."}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Berlin Germany","acronym":"ICFP '19"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342593","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331545.3342593","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:39Z","timestamp":1750202019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331545.3342593"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,8]]},"references-count":17,"alternative-id":["10.1145\/3331545.3342593","10.1145\/3331545"],"URL":"https:\/\/doi.org\/10.1145\/3331545.3342593","relation":{},"subject":[],"published":{"date-parts":[[2019,8,8]]},"assertion":[{"value":"2019-08-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}