{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T19:03:47Z","timestamp":1749063827350},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319119359"},{"type":"electronic","value":"9783319119366"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_3","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T19:11:50Z","timestamp":1414177910000},"page":"24-30","source":"Crossref","is-referenced-by-count":2,"title":["A Bounded Model Checker for SPARK Programs"],"prefix":"10.1007","author":[{"given":"Cl\u00e1udio Belo","family":"Louren\u00e7o","sequence":"first","affiliation":[]},{"given":"Maria Jo\u00e3o","family":"Frade","sequence":"additional","affiliation":[]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Altran Praxis. SPARK - The SPADE Ada Kernel (including RavenSPARK), Edition 7.2 (December 2011)"},{"issue":"4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10817-010-9172-3","volume":"45","author":"D. Angeletti","year":"2010","unstructured":"Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J. Autom. Reason.\u00a045(4), 397\u2013414 (2010)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A. Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf.\u00a011(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR4","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-31762-0_2","volume-title":"Formal Verification of Object-Oriented Software","author":"T. Bormer","year":"2012","unstructured":"Bormer, T., et al.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 3\u201321. Springer, Heidelberg (2012)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: ASE 2009. IEEE Computer Society (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2006.12.032","volume":"174","author":"A. Griesmayer","year":"2007","unstructured":"Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for C programs. Electronic Notes in Theoretical Computer Science\u00a0174(4), 95\u2013111 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-29860-8_32","volume-title":"Runtime Verification","author":"J. Jaffar","year":"2012","unstructured":"Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded symbolic execution for program verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol.\u00a07186, pp. 396\u2013411. Springer, Heidelberg (2012)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: Experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Louren\u00e7o, C.B.: A Bounded Model Checker for SPARK Programs. Master\u2019s thesis, University of Minho (2013)","DOI":"10.1007\/978-3-319-11936-6_3"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-87873-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"B.W. Weide","year":"2008","unstructured":"Weide, B.W., et al.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 84\u201398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T07:20:29Z","timestamp":1559028029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}