{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:25:47Z","timestamp":1750220747678,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2020,9,30]],"date-time":"2020-09-30T00:00:00Z","timestamp":1601424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["1948936"],"award-info":[{"award-number":["1948936"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2020,9,30]]},"abstract":"<jats:p>Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This article presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware.<\/jats:p>\n          <jats:p>The verification approach is demonstrated on an industrial case study. We present a REDuced instruction set for Fixed-point and INteger arithmetic (REDFIN), a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs.<\/jats:p>","DOI":"10.1145\/3391900","type":"journal-article","created":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T12:39:02Z","timestamp":1594125542000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Spacecraft Control Programs"],"prefix":"10.1145","volume":"19","author":[{"given":"Georgy","family":"Lukyanov","sequence":"first","affiliation":[{"name":"Newcastle University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Mokhov","sequence":"additional","affiliation":[{"name":"Newcastle University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Lechner","sequence":"additional","affiliation":[{"name":"RUAG Space GmbH, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_2_1","volume-title":"Camil Demetrescu, and Irene Finocchi.","author":"Baldoni Roberto","year":"2018","unstructured":"Roberto Baldoni , Emilio Coppa , Daniele Cono D\u2019Elia , Camil Demetrescu, and Irene Finocchi. 2018 . A survey of symbolic execution techniques. ACM Computing Surveys 51, 3, Article 50 (2018). Roberto Baldoni, Emilio Coppa, Daniele Cono D\u2019Elia, Camil Demetrescu, and Irene Finocchi. 2018. A survey of symbolic execution techniques. ACM Computing Surveys 51, 3, Article 50 (2018)."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/571922.571958"},{"key":"e_1_2_1_4_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--593. Issue 5. Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23 (9 2013), 552--593. Issue 5."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-005-0004-8"},{"key":"e_1_2_1_6_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--340. 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--340."},{"key":"e_1_2_1_8_1","unstructured":"Stephen Diehl. 2017. Monads to Machine Code. Retrieved from https:\/\/web.archive.org\/web\/20171207020256\/http:\/\/www.stephendiehl.com\/posts\/monads_machine_code.html.  Stephen Diehl. 2017. Monads to Machine Code. Retrieved from https:\/\/web.archive.org\/web\/20171207020256\/http:\/\/www.stephendiehl.com\/posts\/monads_machine_code.html."},{"key":"e_1_2_1_9_1","volume-title":"SBV: SMT Based Verification in Haskell.","author":"Erkok Levent","year":"2019","unstructured":"Levent Erkok . 2019 . SBV: SMT Based Verification in Haskell. Retrieved from http:\/\/leventerkok.github.io\/sbv\/. Levent Erkok. 2019. SBV: SMT Based Verification in Haskell. Retrieved from http:\/\/leventerkok.github.io\/sbv\/."},{"key":"e_1_2_1_10_1","volume-title":"Myreen","author":"Fox Anthony","year":"2010","unstructured":"Anthony Fox and Magnus O . Myreen . 2010 . A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proceedings of the International Conference on Interactive Theorem Proving. Springer , 243--258. Anthony Fox and Magnus O. Myreen. 2010. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proceedings of the International Conference on Interactive Theorem Proving. Springer, 243--258."},{"key":"e_1_2_1_11_1","unstructured":"Tikhon Jelvis. 2016. Analyzing Programs with Z3 (video recording of Compose Conference talk). Retrieved from http:\/\/jelv.is\/talks\/compose-2016.  Tikhon Jelvis. 2016. Analyzing Programs with Z3 (video recording of Compose Conference talk). Retrieved from http:\/\/jelv.is\/talks\/compose-2016."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.11950"},{"key":"e_1_2_1_14_1","unstructured":"MIT. 2017. A formal specification of the RISC-V ISA written in Haskell. Retrieved from https:\/\/github.com\/mit-plv\/riscv-semantics.  MIT. 2017. A formal specification of the RISC-V ISA written in Haskell. Retrieved from https:\/\/github.com\/mit-plv\/riscv-semantics."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342593"},{"key":"e_1_2_1_17_1","volume-title":"OOPSLA","author":"Reid Alastair","year":"2017","unstructured":"Alastair Reid . 2017. Who guards the guards? Formal validation of the arm V8-m architecture specification. ACM Programming Languages 1 , OOPSLA ( 2017 ), 88:1--88:24. Alastair Reid. 2017. Who guards the guards? Formal validation of the arm V8-m architecture specification. ACM Programming Languages 1, OOPSLA (2017), 88:1--88:24."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_2_1_21_1","unstructured":"Lewis Wall. 2017. An ASM Monad. Retrieved from http:\/\/wall.org\/ lewis\/2013\/10\/15\/asm-monad.html.  Lewis Wall. 2017. An ASM Monad. Retrieved from http:\/\/wall.org\/ lewis\/2013\/10\/15\/asm-monad.html."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3391900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3391900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:48Z","timestamp":1750199928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3391900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,30]]},"references-count":19,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,9,30]]}},"alternative-id":["10.1145\/3391900"],"URL":"https:\/\/doi.org\/10.1145\/3391900","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2020,9,30]]},"assertion":[{"value":"2019-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}