{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:02Z","timestamp":1763467982541,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":22,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_6","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"175-191","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["Formal Verification of Partition Management for the AAMP7G Microprocessor"],"prefix":"10.1007","author":[{"given":"Matthew M.","family":"Wilding","sequence":"first","affiliation":[]},{"given":"David A.","family":"Greve","sequence":"additional","affiliation":[]},{"given":"Raymond J.","family":"Richards","sequence":"additional","affiliation":[]},{"given":"David S.","family":"Hardin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"key":"6_CR1_6","unstructured":"Alves-Foss J, Taylor C (2004) An analysis of the GWV security policy. In: Proceedings of the fifth international workshop on ACL2 and its applications, Austin, TX, Nov. 2004"},{"issue":"3","key":"6_CR2_6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/MM.1982.290992","volume":"2","author":"D Best","year":"1982","unstructured":"Best D, Kress C, Mykris N, Russell J, Smith W (1982) An advanced-architecture CMOS\/SOS microprocessor. IEEE Micro 2(3):11\u201326","journal-title":"IEEE Micro"},{"key":"6_CR3_6","unstructured":"Common Criteria for Information Technology Security Evaluation (CCITSE) (1999) Available at http:\/\/www.radium.ncsc.mil\/tpep\/library\/ccitse\/ccitse.html"},{"key":"6_CR4_6","unstructured":"Greve D (2004) Address enumeration and reasoning over linear address spaces. In: Proceedings of ACL2\u201904, Austin, TX, Nov. 2004"},{"key":"6_CR5_6","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-1-4419-1539-9_9","volume-title":"Design and verification of microprocessor systems for high-assurance applications","author":"D Greve","year":"2010","unstructured":"Greve D (2010) Information security modeling and analysis. In Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 249\u2013299"},{"key":"6_CR6_6","first-page":"89","volume-title":"Computer-aided reasoning: ACL2 case studies","author":"D Greve","year":"2000","unstructured":"Greve D, Wilding M, Hardin D (2000) High-speed, analyzable simulators. In: Kaufmann M, Manolios P, Moore JS (eds) Computer-aided reasoning: ACL2 case studies. Kluwer, Dordrecht, pp 89\u2013106"},{"key":"6_CR7_6","unstructured":"Greve D, Wilding M, Vanfleet M (2003) A separation kernel formal security policy. In: Proceedings of ACL2\u201903"},{"key":"6_CR8_6","unstructured":"Greve D, Richards R, Wilding M (2004) A summary of intrinsic partitioning verification. In: Proceedings of ACL2\u201904, Austin, TX, Nov. 2004"},{"key":"6_CR9_6","series-title":"of LNCS","first-page":"39","volume-title":"CAV\u201998","author":"D Hardin","year":"1998","unstructured":"Hardin D, Wilding M, Greve D (1998), Transforming the theorem prover into a digital design tool: from concept car to off-road vehicle. In: Hu A, Vardi M (eds) CAV\u201998, vol 1427 of LNCS. Springer, Berlin, pp 39\u201344"},{"key":"6_CR10_6","doi-asserted-by":"crossref","unstructured":"Hardin D, Smith E, Young W (2006) A robust machine code proof framework for highly secure applications. In: Proceedings of ACL2\u201906, Seattle, WA, Aug. 2006","DOI":"10.1145\/1217975.1217978"},{"key":"6_CR11_6","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht"},{"key":"6_CR12_6","doi-asserted-by":"crossref","unstructured":"Matthews J, Moore JS, Ray S, Vroon D (2006) Verification condition generation via theorem proving. In: Proceedings of LPAR\u201906, vol 4246 of LNCS, pp 362\u2013376","DOI":"10.1007\/11916277_25"},{"key":"6_CR13_6","series-title":"of LNCS","first-page":"289","volume-title":"CHARME 2003","author":"JS Moore","year":"2003","unstructured":"Moore JS (2003) Inductive assertions and operational semantics. In Geist D (ed) CHARME 2003, vol 2860 of LNCS. Springer, Berlin, pp 289\u2013303"},{"key":"6_CR14_6","series-title":"LNCS.","first-page":"9","volume-title":"Proceedings of PADL 2002","author":"JS Moore","year":"2002","unstructured":"Moore JS, Boyer R (2002) Single-threaded objects in ACL2. In: Proceedings of PADL 2002, vol 2257 of LNCS. Springer, Berlin, pp 9\u201327"},{"key":"6_CR15_6","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-1-4419-1539-9_10","volume-title":"Design and verification of microprocessor systems for high-assurance applications","author":"R Richards","year":"2010","unstructured":"Richards R (2010) Modeling and security analysis of a commercial real-time operating system kernel. In Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 301\u2013322"},{"key":"6_CR16_6","unstructured":"Richards R, Greve D, Wilding M, Vanfleet M (2004) The common criteria, formal methods, and ACL2. In: Proceedings of the fifth international workshop on ACL2 and its applications, Austin, TX, Nov. 2004"},{"key":"6_CR17_6","unstructured":"Rockwell Collins, Inc. (2003) AAMP7r1 reference manual"},{"key":"6_CR18_6","unstructured":"Rockwell Collins, Inc. (2005) Rockwell Collins receives MILS certification from NSA on microprocessor. Rockwell Collins press release, 24 August 2005. http:\/\/www.rockwellcollins.com\/news\/page6237.html"},{"key":"6_CR19_6","unstructured":"RTCA, Inc. (2000) Design assurance guidance for airborne electronic hardware, RTCA\/DO-254"},{"key":"6_CR20_6","doi-asserted-by":"crossref","unstructured":"Rushby J (1981) Design and verification of secure systems. In: Proceedings of the eighth symposium on operating systems principles, vol 15, December 1981","DOI":"10.1145\/800216.806586"},{"key":"6_CR21_6","unstructured":"Rushby J (1999) Partitioning for safety and security: requirements, mechanisms, and assurance. NASA contractor report CR-1999\u2013209347"},{"key":"6_CR22_6","volume-title":"Proceedings of dependable computing for critical applications \u2013 DCCA-7","author":"M Wilding","year":"1999","unstructured":"Wilding M, Hardin D, Greve D (1999) Invariant performance: a statement of task isolation useful for embedded application integration. In: Weinstock C, Rushby J (eds) Proceedings of dependable computing for critical applications \u2013 DCCA-7. IEEE Computer Society Dependable Computing Series"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T21:12:38Z","timestamp":1674076358000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_6","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}