{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T19:03:42Z","timestamp":1749063822581},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642305979"},{"type":"electronic","value":"9783642305986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30598-6_8","type":"book-chapter","created":{"date-parts":[[2012,6,6]],"date-time":"2012-06-06T09:38:56Z","timestamp":1338975536000},"page":"105-118","source":"Crossref","is-referenced-by-count":2,"title":["An Approach to Model Checking Ada Programs"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Miguel","family":"Faria","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o","family":"Martins","sequence":"additional","affiliation":[]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alves-Foss, J., Taylor, C., Oman, P.: A multi-layered approach to security in high assurance systems. In: Hawaii International Conference on System Sciences, vol.\u00a09, p. 90302b (2004)","DOI":"10.1109\/HICSS.2004.1265709"},{"key":"8_CR2","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-20398-5_6","volume-title":"NASA Formal Methods","author":"J. Belt","year":"2011","unstructured":"Belt, J., Hatcliff, J., Robby, Chalin, P., Hardin, D., Deng, X.: Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 58\u201372. Springer, Heidelberg (2011)"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: Applications to software engineering. Int. J. Softw. Tools Technol. Transf.\u00a09, 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/126551.126552","volume-title":"Proceedings of the Conference on TRI-Ada 1991: Today\u2019s Accomplishments; Tomorrow\u2019s Expectations, TRI-Ada 1991","author":"J.B. Bladen","year":"1991","unstructured":"Bladen, J.B., Spenhoff, D., Blake, S.J.: Ada semantic interface specification (ASIS). In: Proceedings of the Conference on TRI-Ada 1991: Today\u2019s Accomplishments; Tomorrow\u2019s Expectations, TRI-Ada 1991, pp. 6\u201315. ACM, New York (1991)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM Press (1998)","DOI":"10.1145\/298595.298598"},{"key":"8_CR7","unstructured":"Dwyer, M.B., Pasareanu, C.S., Corbett, J.C.: Translating Ada programs for model checking: A tutorial. Technical Report KSU-CIS-TR-98-12, Kansas State University (1998)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Kaiser, C., Pradat-Peyre, J.F., Rousseau, P.: Verifying linear time temporal logic properties of concurrent Ada programs with quasar. Ada Lett.\u00a0XXIV, 17\u201324 (2003)","DOI":"10.1145\/992211.958424"},{"key":"8_CR9","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv.\u00a041, 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"8_CR11","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/3-540-48753-0_2","volume-title":"Reliable Software Technologies - Ada-Europe \u201999","author":"K. Lundqvist","year":"1999","unstructured":"Lundqvist, K., Asplund, L., Michell, S.: A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects. In: Gonz\u00e1lez Harbour, M., de la Puente, J.A. (eds.) Ada-Europe 1999. LNCS, vol.\u00a01622, pp. 12\u201325. Springer, Heidelberg (1999)"},{"key":"8_CR13","unstructured":"Martins, J.: Formal verification of Ada programs: An approach based on model checking. Master\u2019s thesis, Universidade do Minho (2011), \n                    \n                      http:\/\/www.evolve-itea.org\/public\/publications.php"},{"key":"8_CR14","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)"},{"key":"8_CR15","unstructured":"Rossebo, B., Oman, P., Alves-foss, J., Blue, R., Jaszkowiak, P.: Using SPARK-Ada to Model and Verify a MILS Message Router. In: Proceedings of the International Symposium on Secure Software Engineering (2006)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Rushby, J.: The design and verification of secure systems. In: Eighth ACM Symposium on Operating System Principles (SOSP), Asilomar, CA, pp. 12\u201321 (December 1981); ACM Operating Systems Review 15(5)","DOI":"10.1145\/1067627.806586"},{"key":"8_CR17","unstructured":"SPARK Team. SPARK Examiner: The SPARK Ravenscar Profile (January 2008)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Ada 2005 Reference Manual. Language and Standard Libraries","author":"S. Tucker Taft","year":"2006","unstructured":"Tucker Taft, S., Duff, R.A., Brukardt, R.L., Pl\u00f6dereder, E., Leroy, P.: Ada 2005 Reference Manual. LNCS, vol.\u00a04348. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologies \u2013 Ada-Europe 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30598-6_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:46:05Z","timestamp":1620128765000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30598-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642305979","9783642305986"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30598-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}