{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:10:41Z","timestamp":1760044241226},"reference-count":40,"publisher":"American Institute of Aeronautics and Astronautics (AIAA)","issue":"10","content-domain":{"domain":["arc.aiaa.org"],"crossmark-restriction":true},"short-container-title":["Journal of Aerospace Information Systems"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.2514\/1.i010178","type":"journal-article","created":{"date-parts":[[2014,10,1]],"date-time":"2014-10-01T09:55:47Z","timestamp":1412157347000},"page":"702-713","update-policy":"http:\/\/dx.doi.org\/10.2514\/aiaa_crossmarkpolicy","source":"Crossref","is-referenced-by-count":11,"title":["Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges"],"prefix":"10.2514","volume":"11","author":[{"given":"Khalil","family":"Ghorbal","sequence":"first","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]},{"given":"Erik","family":"Zawadzki","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]},{"given":"Geoffrey J.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]},{"given":"Peter","family":"Capell","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213"}]}],"member":"1387","reference":[{"key":"r3","doi-asserted-by":"publisher","DOI":"10.2514\/1.24677"},{"key":"r4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_8"},{"key":"r5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_27"},{"key":"r6","doi-asserted-by":"publisher","DOI":"10.2514\/6.2010-3385"},{"key":"r7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"r9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"r11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4"},{"key":"r12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"r13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"r14","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2011.6083138"},{"key":"r15","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2012.25"},{"key":"r16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"r17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"r21","doi-asserted-by":"publisher","DOI":"10.2307\/2372560"},{"key":"r23","doi-asserted-by":"publisher","DOI":"10.1109\/9.664154"},{"key":"r24","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn070"},{"key":"r25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_19"},{"key":"r26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_34"},{"key":"r27","doi-asserted-by":"publisher","DOI":"10.1115\/1.3662552"},{"issue":"1","key":"r28","first-page":"17","volume":"19","author":"Kochenderfer M. J.","year":"2012","journal-title":"Lincoln Laboratory Journal","ISSN":"http:\/\/id.crossref.org\/issn\/0896-4130","issn-type":"print"},{"key":"r29","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman M. L.","year":"2009"},{"key":"r30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_54"},{"key":"r31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_17"},{"key":"r32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_46"},{"key":"r33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_15"},{"key":"r35","unstructured":"\u201cSoftware Considerations in Airborne Systems and Equipment Certification,\u201d RTCA STD DO-178C, Washington, D.C. 2012."},{"key":"r36","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"r37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_34"},{"key":"r38","doi-asserted-by":"publisher","DOI":"10.1109\/6979.898217"},{"key":"r39","doi-asserted-by":"publisher","DOI":"10.2514\/6.2005-6047"},{"key":"r40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73445-1_13"},{"key":"r41","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0079-8"},{"key":"r42","doi-asserted-by":"publisher","DOI":"10.1109\/6979.898224"},{"key":"r45","doi-asserted-by":"publisher","DOI":"10.2514\/6.2000-4268"},{"key":"r46","doi-asserted-by":"publisher","DOI":"10.2514\/atcq.15.1.1"},{"key":"r47","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.851439"},{"key":"r48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"r49","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_5"},{"key":"r50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_43"},{"key":"r51","doi-asserted-by":"publisher","DOI":"10.2514\/1.21562"}],"container-title":["Journal of Aerospace Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/arc.aiaa.org\/doi\/pdf\/10.2514\/1.I010178","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,1]],"date-time":"2021-03-01T07:21:52Z","timestamp":1614583312000},"score":1,"resource":{"primary":{"URL":"https:\/\/arc.aiaa.org\/doi\/10.2514\/1.I010178"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":40,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["10.2514\/1.I010178"],"URL":"https:\/\/doi.org\/10.2514\/1.i010178","relation":{},"ISSN":["2327-3097"],"issn-type":[{"value":"2327-3097","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10]]},"assertion":[{"value":"2013-09-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-06-14","order":1,"name":"revised","label":"Revised","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-28","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}