{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T05:23:40Z","timestamp":1749792220780},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642135491"},{"type":"electronic","value":"9783642135507"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13550-7_7","type":"book-chapter","created":{"date-parts":[[2010,6,15]],"date-time":"2010-06-15T15:14:12Z","timestamp":1276614852000},"page":"97-110","source":"Crossref","is-referenced-by-count":1,"title":["Program Verification in SPARK and ACSL: A Comparative Case Study"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Brito","sequence":"first","affiliation":[]},{"given":"Jorge","family":"Sousa Pinto","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","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":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# Programming System: Challenges and Directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 144\u2013152. Springer, Heidelberg (2008)"},{"key":"7_CR3","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language. CEA and INRIA. Preliminary design, version 1.4 (October 29, 2008)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/ESSCIRC.2009.5325955","volume-title":"Proceedings of TPHOLs 2009","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 1\u201322. Springer, Heidelberg (2009)"},{"key":"7_CR5","unstructured":"Conchon, S., Contejean, E., Kanig, J.: Ergo: a Theorem Prover for Polymorphic First-order Logic Modulo Theories, LRI, Univ. Paris-Sud\/CNRS, and INRIA (2006)"},{"issue":"3","key":"7_CR6","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis For Computer Programming. Communications of the ACM\u00a012, 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/1345169.1345177","volume-title":"AFM 2007: Proceedings of the second workshop on Automated formal methods","author":"P.B. Jackson","year":"2007","unstructured":"Jackson, P.B., Ellis, B.J., Sharp, K.: Using SMT Solvers to Verify High-integrity Programs. In: AFM 2007: Proceedings of the second workshop on Automated formal methods, pp. 60\u201368. ACM Press, New York (2007)"},{"key":"7_CR10","first-page":"573","volume-title":"Proceedings of ASE 2007","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T.: Tutorial on JML, the Java Modeling Language. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Proceedings of ASE 2007, p. 573. ACM, New York (2007)"},{"key":"7_CR11","volume-title":"Proceedings of PLPV 2007","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C.: Jessie: an Intermediate Language for Java and C Verification. In: Stump, A., Xi, H. (eds.) Proceedings of PLPV 2007. ACM, New York (2007)"},{"key":"7_CR12","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.2 (2008)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Applying \u201cDesign by Contract\u201d. IEEE Computer\u00a025(10) (1992)","DOI":"10.1109\/2.161279"},{"issue":"5","key":"7_CR14","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/359104.359110","volume":"22","author":"J.C. Reynolds","year":"1979","unstructured":"Reynolds, J.C.: Reasoning about arrays. Commun. ACM\u00a022(5), 290\u2013299 (1979)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologiey \u2013 Ada-Europe 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13550-7_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:39:56Z","timestamp":1606185596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13550-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642135491","9783642135507"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13550-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}