{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:41:25Z","timestamp":1764783685272,"version":"3.40.4"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,10,28]],"date-time":"2014-10-28T00:00:00Z","timestamp":1414454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-014-0322-5","type":"journal-article","created":{"date-parts":[[2014,10,27]],"date-time":"2014-10-27T15:49:37Z","timestamp":1414424977000},"page":"695-707","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["SPARK\u00a02014 and GNATprove"],"prefix":"10.1007","volume":"17","author":[{"given":"Duc","family":"Hoang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yannick","family":"Moy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angela","family":"Wallenburg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roderick","family":"Chapman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,28]]},"reference":[{"key":"322_CR1","unstructured":"Barnes, J.: Ada 2012 rationale (2012). http:\/\/www.adacore.com\/knowledge\/technical-papers\/ada-2012-rationale\/"},{"key":"322_CR2","unstructured":"Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis. Third Edition of the SPARK Book (2012)"},{"key":"322_CR3","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7, 212\u2013232 (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"322_CR4","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: SMT\u201908, vol. 367 of ACM ICPS, pp. 1\u20135 (2008)","DOI":"10.1145\/1512464.1512466"},{"key":"322_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81\u201391 (2011)","DOI":"10.1145\/1953122.1953145"},{"key":"322_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., Paskevich, A., March\u00e9, C.: Why3: shepherd your herd of provers. In: Proceedings of the First International Workshop on Intermediate Verification Languages, Boogie (2011)"},{"key":"322_CR7","doi-asserted-by":"crossref","unstructured":"Beckert, B., Gladisch, C., Tyszberowicz, S.S., Yehudai, A.: KeYGenU: combining verification-based and capture and replay techniques for regression unit testing. Int. J. Syst. Assur. Eng. Manag. 2(2), 97\u2013113 (2011)","DOI":"10.1007\/s13198-011-0068-3"},{"key":"322_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV \u201907), vol. 4590 of Lecture Notes in Computer Science, pp. 298\u2013302. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"322_CR9","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, T.: VCC: a practical system for verifying concurrent C. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs \u201909, pp. 23\u201342. Springer, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"322_CR10","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R..: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS \u201906, pp. 322\u2013335. ACM, New York (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"322_CR11","unstructured":"Couchot, J.-F., Giorgetti, A., Stouls, N.: Graph Based Reduction of Program Verification Conditions. In: Sa\u00efdi, H., Shankar, N. (eds.) AFM\u201909, Automated Formal Methods (co-located with CAV\u201909), pp. 40\u201347, Grenoble, France. ACM Press (2009)"},{"key":"322_CR12","doi-asserted-by":"crossref","unstructured":"Chalin, P.: JML support for primitive arbitrary precision numeric types: definition and semantics. J. Object Technol. 3(6), 57\u201379 (2004)","DOI":"10.5381\/jot.2004.3.6.a3"},{"key":"322_CR13","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Engineering a sound assertion semantics for the verifying compiler. IEEE Trans. Softw. Eng. 36(2), 275\u2013287 (2010)","DOI":"10.1109\/TSE.2009.59"},{"key":"322_CR14","doi-asserted-by":"crossref","unstructured":"Claessen, K., Johansson, M., Rosen, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: Fleuriot, J., H\u00f6fner, P., McIver, A., Smaill, A. (eds.) ATx\u201912\/WInG\u201912, vol. 17 of EPiC Series, pp. 16\u201325. EasyChair (2013)","DOI":"10.29007\/3qwr"},{"key":"322_CR15","unstructured":"Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: Proceedings of Embedded Real Time Software and Systems, Toulouse (2012)"},{"key":"322_CR16","doi-asserted-by":"crossref","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Proceedings of the 4th International Conference on Tests and Proofs, TAP\u201910, pp. 6\u201321. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-13977-2_3"},{"key":"322_CR17","doi-asserted-by":"crossref","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: Fontaine, P., Goel, A. (eds.) SMT 2012, vol. 20 of EPiC Series, pp. 22\u201331. EasyChair (2013)","DOI":"10.29007\/3c1n"},{"key":"322_CR18","unstructured":"Dross, C., Efstathopoulos, P., Lesens, D., Mentr\u00e9, D., Moy, Y: Rail, space, security: three case studies for spark 2014. In Proceedings of ERTS (2014)"},{"key":"322_CR19","doi-asserted-by":"crossref","unstructured":"Dross, C., Filli\u00e2tre, J.-C., Moy Y.: Correct code containing containers. In: 5th International Conference on Tests and Proofs (TAP\u201911), Zurich (2011)","DOI":"10.1007\/978-3-642-21768-5_9"},{"key":"322_CR20","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR Workshops, vol. 418 of CEUR Workshop Proceedings. CEUR-WS.org (2008)"},{"key":"322_CR21","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Computer Progr. 69(1\u20133), 35\u201345 (2007)","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"322_CR22","unstructured":"Guitton, J., Kanig, J., Moy, Y.: Why Hi-Lite Ada? In: Proceedings of Boogie 2011, the 1st International Workshop on Intermediate Language Verification (2011)"},{"key":"322_CR23","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201905, pp. 213\u2013223. ACM, New York (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"322_CR24","unstructured":"Hi-Lite: Simplifying the use of formal methods. http:\/\/www.open-do.org\/projects\/hi-lite\/ (2013)"},{"key":"322_CR25","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2012\u2014organizer\u2019s report. Technical Report 2013\u201301, Department of Informatics, Karlsruhe Institute of Technology. http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000034373 (2013)"},{"key":"322_CR26","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16 (2012)","DOI":"10.1145\/2187671.2187678"},{"key":"322_CR27","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580 (October 1969)","DOI":"10.1145\/363235.363259"},{"key":"322_CR28","doi-asserted-by":"crossref","unstructured":"Hoare, T.: The verifying compiler: a grand challenge for computing research. J. ACM 50, 2003 (2003)","DOI":"10.1145\/602382.602403"},{"key":"322_CR29","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, PLDI \u201988, pp. 35\u201346. ACM, New York (1988)","DOI":"10.1145\/53990.53994"},{"key":"322_CR30","doi-asserted-by":"crossref","unstructured":"Kanig, J., Schonberg, E., Dross, C.: Hi-Lite: the convergence of compiler technology and program verification. In: Proceedings of the 2012 ACM conference on High integrity language technology, HILT \u201912, pp. 27\u201334. ACM, New York (2012)","DOI":"10.1145\/2402676.2402690"},{"key":"322_CR31","doi-asserted-by":"crossref","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T. Overview and evaluation of premise selection techniques for large theory mathematics. In: Proceedings of the 6th international joint conference on Automated Reasoning, IJCAR\u201912, pp. 378\u2013392. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31365-3_30"},{"issue":"6","key":"322_CR32","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"322_CR33","unstructured":"Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc, Upper Saddle River (1988)"},{"key":"322_CR34","doi-asserted-by":"crossref","unstructured":"O\u2019Neill, I.: SPARK\u2014a language and tool-set for high-integrity software development. In: Boulanger, J.-L. (ed.) Industrial Use of Formal Methods: Formal Verification. Wiley, New York (2012)","DOI":"10.1002\/9781118561829.ch1"},{"key":"322_CR35","unstructured":"RTCA. DO-178B: software considerations in airborne systems and equipment certification (1992)"},{"key":"322_CR36","unstructured":"RTCA. DO-178C: software considerations in airborne systems and equipment certification (2011)"},{"key":"322_CR37","unstructured":"Schanda, F., Brain, B: Using answer set programming in the development of verified software. In: Dovier, A., Santos Costa, V. (eds.) Technical Communications of the 28th International Conference on Logic Programming (ICLP\u201912), vol. 17 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 72\u201385. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2012)"},{"key":"322_CR38","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G: CUTE: a concolic unit testing engine for c. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-13, pp. 263\u2013272. ACM, New York (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"322_CR39","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM\u201911, pp. 382\u2013398. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"322_CR40","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv 41(4), 19:1\u201319:36 (2009)","DOI":"10.1145\/1592434.1592436"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0322-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0322-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0322-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T15:55:49Z","timestamp":1746460549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0322-5"}},"subtitle":["A competition report from builders of an industrial-strength verifying compiler"],"short-title":[],"issued":{"date-parts":[[2014,10,28]]},"references-count":40,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["322"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0322-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,10,28]]}}}