{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:48:46Z","timestamp":1771573726648,"version":"3.50.1"},"publisher-location":"Cham","reference-count":127,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319919072","type":"print"},{"value":"9783319919089","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_18","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T09:05:00Z","timestamp":1570179900000},"page":"345-373","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":85,"title":["Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MSPEC.2017.7802740","volume":"54","author":"E Ackerman","year":"2017","unstructured":"Ackerman, E.: Hail, robo-taxi!. IEEE Spectr. 54(1), 26\u201329 (2017)","journal-title":"IEEE Spectr."},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification-The KeY Book: From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M. (eds.): Deductive Software Verification-The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-24372-1_3","volume-title":"Automated Technology for Verification and Analysis","author":"J Alglave","year":"2011","unstructured":"Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software verification tools really work. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 28\u201342. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_3"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-33693-0_6","volume-title":"Integrated Formal Methods","author":"M Ameri","year":"2016","unstructured":"Ameri, M., Furia, C.A.: Why just boogie? Translating between intermediate verification languages. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79\u201395. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_6"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-07317-0_5","volume-title":"Formal Methods for Executable Software Models","author":"A Amighi","year":"2014","unstructured":"Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172\u2013216. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_5"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-12736-1_14","volume-title":"Programming Languages and Systems","author":"A Amighi","year":"2014","unstructured":"Amighi, A., Blom, S., Huisman, M.: Resource protection using atomics. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 255\u2013274. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12736-1_14"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Huisman, M.: VerCors: a layered approach to practical verification of concurrent software. In: 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP, Heraklion, Crete, Greece, pp. 495\u2013503. IEEE Computer Society (2016)","DOI":"10.1109\/PDP.2016.107"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3"},{"key":"18_CR12","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"18","DOI":"10.4204\/EPTCS.102.4","volume":"102","author":"Christoph Baumann","year":"2012","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Proceedings of the 7th Conference on Systems Software Verification. EPTCS, vol. 102, pp. 18\u201332 (2012)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-15201-1_1","volume-title":"Software Engineering and Formal Methods","author":"B Beckert","year":"2015","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 3\u201319. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_1"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Beckert, B., Klebanov, V., Ulbrich, M.: Regression verification for Java using a secure information flow calculus. In: Monahan, R. (ed.) Proceedings of the 17th Workshop on Formal Techniques for Java-Like Programs, FTfJP, Prague, Czech Republic, pp. 6:1\u20136:6. ACM (2015)","DOI":"10.1145\/2786536.2786544"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-24756-2_12","volume-title":"Integrated Formal Methods","author":"B Beckert","year":"2004","unstructured":"Beckert, B., Schlager, S.: Software verification with integrated data type refinement for integer arithmetic. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 207\u2013226. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24756-2_12"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE, Seattle, WA, USA, pp. 326\u2013337. ACM (2016)","DOI":"10.1145\/2950290.2950351"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-47166-2_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195\u2013211. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14"},{"issue":"3","key":"18_CR19","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1008700623084","volume":"16","author":"N Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, N., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.E.: Verifying temporal properties of reactive systems: a step tutorial. Formal Methods Syst. Des. 16(3), 227\u2013270 (2000)","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"FM 2014: Formal Methods","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127\u2013131. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_9"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M., Kiniry, J.: How do developers use APIs? A case study in concurrency. In: International Conference on Engineering of Complex Computer Systems (ICECCS), Singapore, pp. 212\u2013221. IEEE Computer Society (2013)","DOI":"10.1109\/ICECCS.2013.39"},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376\u2013388 (2014)","journal-title":"Sci. Comput. Program."},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-22969-0_6","volume-title":"Software Engineering and Formal Methods","author":"S Blom","year":"2015","unstructured":"Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84\u201398. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_6"},{"key":"18_CR24","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages (2011)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Long Beach, California, USA, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., R\u00fcmmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: 22nd IEEE Symposium on Computer Arithmetic, ARITH 2015, Lyon, France, pp. 160\u2013167. IEEE (2015)","DOI":"10.1109\/ARITH.2015.26"},{"issue":"1\u20133","key":"18_CR28","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theoret. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"18_CR29","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes, S., O\u2019Hearn, P.: Concurrent separation logic. ACM SIGLOG News 3(3), 47\u201365 (2016)","journal-title":"ACM SIGLOG News"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-46508-1_8","volume-title":"Transactions on Foundations for Mastering Change I","author":"R Bubel","year":"2016","unstructured":"Bubel, R., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Owe, O., Schaefer, I., Yu, I.C.: Proof repositories for compositional verification of evolving software systems. In: Steffen, B. (ed.) Transactions on Foundations for Mastering Change I. LNCS, vol. 9960, pp. 130\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46508-1_8"},{"key":"18_CR31","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974, pp. 308\u2013312. Elsevier\/North-Holland, Amsterdam (1974)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459\u2013465. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_33"},{"key":"18_CR33","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35, 583\u2013599 (2005)","journal-title":"Softw. Pract. Exp."},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-319-23820-3_21","volume-title":"Runtime Verification","author":"JM Chimento","year":"2015","unstructured":"Chimento, J.M., Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 297\u2013305. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_21"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-662-46081-8_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Christakis","year":"2015","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: An experimental evaluation of deliberate unsoundness in a static program analyzer. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 336\u2013354. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_19"},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"18_CR37","doi-asserted-by":"publisher","first-page":"79","DOI":"10.4204\/EPTCS.149.8","volume":"149","author":"David R. Cok","year":"2014","unstructured":"Cok, D.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) 1st Workshop on Formal Integrated Development Environment, (F-IDE). EPTCS, vol. 149, pp. 79\u201392 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"DR Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108\u2013128. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_6"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S Gouw de","year":"2015","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_16"},{"key":"18_CR40","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"18_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BFb0015468","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software","author":"P Deussen","year":"1995","unstructured":"Deussen, P., Hansmann, A., K\u00e4ufl, T., Klingenbeck, S.: The verification system Tatzelwurm. In: Broy, M., J\u00e4hnichen, S. (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 285\u2013298. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0015468"},{"key":"18_CR42","volume-title":"A Discipline of Programming","author":"E Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"18_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517\u2013526. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35"},{"key":"18_CR44","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-18467-8_27","volume-title":"ICT Systems Security and Privacy Protection","author":"QH Do","year":"2015","unstructured":"Do, Q.H., Bubel, R., H\u00e4hnle, R.: Exploit generation for information flow leaks in object-oriented programs. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 401\u2013415. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-18467-8_27"},{"issue":"6","key":"18_CR45","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and verifythis competition. STTT 17(6), 677\u2013694 (2015)","journal-title":"STTT"},{"issue":"1\u20133","key":"18_CR46","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","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. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"18_CR47","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. 4590, pp. 173\u2013177. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21"},{"key":"18_CR48","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math 19, 19\u201331 (1967)","journal-title":"Proc. Symp. Appl. Math"},{"key":"18_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"18_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184\u2013191. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13"},{"key":"18_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-16780-3_99","volume-title":"8th International Conference on Automated Deduction","author":"R H\u00e4hnle","year":"1986","unstructured":"H\u00e4hnle, R., Heisel, M., Reif, W., Stephan, W.: An interactive verification system based on dynamic logic. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 306\u2013315. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16780-3_99"},{"key":"18_CR52","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-53946-1_4","volume-title":"Formal Techniques for Safety-Critical Systems","author":"E Kamburjan","year":"2017","unstructured":"Kamburjan, E., H\u00e4hnle, R.: Uniform modeling of railway operations. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 55\u201371. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-53946-1_4"},{"key":"18_CR53","unstructured":"H\u00e4hnle, R., Menzel, W., Schmitt, P.: Integrierter deduktiver Software-Entwurf. K\u00fcnstliche Intelligenz, pp. 40\u201341, December 1998"},{"key":"18_CR54","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"David Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing. MIT Press, Cambridge (2000)"},{"key":"18_CR55","series-title":"Informatik-Fachberichte","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-73005-4_22","volume-title":"GWAI-87 11th German Workshop on Artifical Intelligence","author":"M Heisel","year":"1987","unstructured":"Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Morik, K. (ed.) GWAI-87 11th German Workshop on Artifical Intelligence. Informatik-Fachberichte, vol. 152, pp. 201\u2013210. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/978-3-642-73005-4_22"},{"key":"18_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-11164-3_21","volume-title":"Runtime Verification","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., Bubel, R., H\u00e4hnle, R.: Symbolic execution debugger (SED). In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 255\u2013262. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_21"},{"key":"18_CR57","doi-asserted-by":"crossref","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: An empirical evaluation of two user interfaces of an interactive program verifier. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE), Singapore, pp. 403\u2013413. ACM Press, September 2016","DOI":"10.1145\/2970276.2970303"},{"key":"18_CR58","doi-asserted-by":"crossref","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: The interactive verification debugger: effective understanding of interactive proof attempts. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE), Singapore, pp. 846\u2013851. ACM Press, September 2016","DOI":"10.1145\/2970276.2970292"},{"key":"18_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-10181-1_4","volume-title":"Integrated Formal Methods","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., K\u00e4sdorf, S., H\u00e4hnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55\u201370. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_4"},{"issue":"6","key":"18_CR60","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/s10009-014-0322-5","volume":"17","author":"D Hoang","year":"2015","unstructured":"Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove: a competition report from builders of an industrial-strength verifying compiler. STTT 17(6), 695\u2013707 (2015)","journal-title":"STTT"},{"issue":"10","key":"18_CR61","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. Commun. ACM 12(10), 576\u2013580, 583 (1969)","journal-title":"Communications of the ACM"},{"key":"18_CR62","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"18_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-19835-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60\u201364. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_7"},{"issue":"2","key":"18_CR64","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"PV Homeier","year":"1995","unstructured":"Homeier, P.V., Martin, D.F.: A mechanically verified verification condition generator. Comput. J. 38(2), 131\u2013141 (1995)","journal-title":"Comput. J."},{"key":"18_CR65","unstructured":"Huisman, M.: Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, University of Nijmegen (2001)"},{"key":"18_CR66","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-49812-6_7","volume-title":"Deductive Software Verification - The KeY Book","author":"M Huisman","year":"2016","unstructured":"Huisman, M., Ahrendt, W., Grahl, D., Hentschel, M.: Formal specification with the Java modeling language. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M. (eds.) Deductive Software Verification - The KeY Book. LNCS, vol. 10001, pp. 193\u2013241. Springer, Cham (2016)"},{"key":"18_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46428-X_20"},{"key":"18_CR68","unstructured":"Huisman, M., Monahan, R., M\u00fcller, P., Poll, E.: VerifyThis 2016: a program verification competition. Technical report TR-CTIT-16-07, Centre for Telematics and Information Technology, University of Twente, Enschede (2016)"},{"issue":"3","key":"18_CR69","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/s001650050052","volume":"11","author":"A Ireland","year":"1999","unstructured":"Ireland, A., Jackson, M., Reid, G.: Interactive proof critics. Formal Asp. Comput. 11(3), 302\u2013325 (1999)","journal-title":"Formal Asp. Comput."},{"key":"18_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45309-1_19","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2001","unstructured":"Jacobs, B.: A formalisation of Java\u2019s exception mechanism. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 284\u2013301. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45309-1_19"},{"key":"18_CR71","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Austin, TX, USA, pp. 271\u2013282. ACM (2011)","DOI":"10.1145\/1926385.1926417"},{"key":"18_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"18_CR73","doi-asserted-by":"crossref","unstructured":"Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault, A., Guan, N. (eds.) International Conference on Embedded Software, EMSOFT, Amsterdam, Netherlands, pp. 127\u2013136. IEEE (2015)","DOI":"10.1109\/EMSOFT.2015.7318268"},{"key":"18_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"issue":"4","key":"18_CR75","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C Jones","year":"1983","unstructured":"Jones, C.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"18_CR76","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Asp. Comput. 23(3), 267\u2013288 (2011)","journal-title":"Formal Asp. Comput."},{"key":"18_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-27705-4_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"IT Kassios","year":"2012","unstructured":"Kassios, I.T., M\u00fcller, P., Schwerhoff, M.: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 196\u2013208. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_16"},{"key":"18_CR78","unstructured":"Kaufmann, M., Moore, J.S.: Design goals for ACL2. In: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, pp. 92\u2013117 (1994)"},{"key":"18_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-75336-0_16","volume-title":"Trustworthy Global Computing","author":"JR Kiniry","year":"2007","unstructured":"Kiniry, J.R., Morkan, A.E., Cochran, D., Fairmichael, F., Chalin, P., Oostdijk, M., Hubbers, E.: The KOA remote voting system: a summary of work to date. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 244\u2013262. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75336-0_16"},{"issue":"3","key":"18_CR80","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Asp. Comput."},{"key":"18_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-319-47166-2_32","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"N Kosmatov","year":"2016","unstructured":"Kosmatov, N., March\u00e9, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461\u2013478. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_32"},{"key":"18_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33693-0_2","volume-title":"Integrated Formal Methods","author":"L Kov\u00e1cs","year":"2016","unstructured":"Kov\u00e1cs, L.: Symbolic computation and automated reasoning for program analysis. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 20\u201327. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_2"},{"key":"18_CR83","unstructured":"Larsson, D., H\u00e4hnle, R.: Symbolic fault injection. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop (Verify) in Connection with CADE-21 Bremen, Germany, vol. 259, pp. 85\u2013103. CEUR Workshop Proceedings (2007)"},{"key":"18_CR84","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Technical report 98-06y, Iowa State University, Department of Computer Science (2003). Revised June 2004"},{"key":"18_CR85","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML Reference Manual, May 2013. Draft revision 2344"},{"issue":"1","key":"18_CR86","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2007.02.059","volume":"190","author":"H Lehner","year":"2007","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL. Electr. Notes Theor. Comput. Sci. 190(1), 35\u201350 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_7"},{"key":"18_CR88","unstructured":"Leino, K., Nelson, G., Saxe, J.: ESC\/Java user\u2019s manual. Technical report SRC 2000\u2013002, Compaq System Research Center (2000)"},{"key":"18_CR89","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"18_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/BFb0026441","volume-title":"Compiler Construction","author":"KRM Leino","year":"1998","unstructured":"Leino, K.R.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302\u2013305. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0026441"},{"key":"18_CR91","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings of the 1st Workshop on Formal Integrated Development Environment, F-IDE, Grenoble, France. EPTCS, vol. 149, pp. 3\u201315 (2014)","DOI":"10.4204\/EPTCS.149.0"},{"key":"18_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-319-21690-4_22","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2015","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: Fine-grained caching of verification results. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380\u2013397. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_22"},{"issue":"6","key":"18_CR93","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-010-0172-1","volume":"23","author":"M Leuschel","year":"2011","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683\u2013709 (2011)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"18_CR94","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(1), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR95","unstructured":"Litvintchouk, S.D., Pratt, V.R.: A proof-checker for dynamic logic. In: Reddy, R. (ed.) Proceedings of the 5th International Joint Conference on Artificial Intelligence, pp. 552\u2013558. William Kaufmann, Cambridge (1977)"},{"key":"18_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-18275-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Logozzo","year":"2011","unstructured":"Logozzo, F.: Practical verification for the working programmer with CodeContracts and abstract interpretation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 19\u201322. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_3"},{"issue":"2","key":"18_CR97","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/MS.1985.230345","volume":"2","author":"DC Luckham","year":"1985","unstructured":"Luckham, D.C., von Henke, F.W.: An overview of Anna, a specification language for Ada. IEEE Softw. 2(2), 9\u201322 (1985)","journal-title":"IEEE Softw."},{"issue":"1\u20132","key":"18_CR98","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certificationof JAVA\/JAVACARD programs annotated in JML. J. Log. Algebr. Program. 58(1\u20132), 89\u2013106 (2004)","journal-title":"J. Log. Algebr. Program."},{"issue":"10","key":"18_CR99","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"18_CR100","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"18_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-319-45943-1_4","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"M Mohsen","year":"2016","unstructured":"Mohsen, M., Jacobs, B.: One step towards automatic inference of formal specifications using automated VeriFast. In: ter Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS\/AVoCS -2016. LNCS, vol. 9933, pp. 56\u201364. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45943-1_4"},{"key":"18_CR102","unstructured":"Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) Proceedings of the 4th Interenational Verification Workshop in connection with CADE-21, Bremen, Germany. CEUR Workshop Proceedings, vol. 259. CEUR-WS.org (2007)"},{"key":"18_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-29613-5_8","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"W Mostowski","year":"2016","unstructured":"Mostowski, W.: Dynamic frames based verification method for concurrent Java programs. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 124\u2013141. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29613-5_8"},{"key":"18_CR104","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"18_CR105","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, University of Cambridge (1998)"},{"issue":"1\u20133","key":"18_CR106","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR107","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1975","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica J. 6, 319\u2013340 (1975)","journal-title":"Acta Informatica J."},{"key":"18_CR108","doi-asserted-by":"crossref","unstructured":"Paganelli, G., Ahrendt, W.: Verifying (in-)stability in floating-point programs by increasing precision, using SMT solving. In: Bj\u00f8rner, N., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, 23\u201326 September 2013, pp. 209\u2013216. IEEE Computer Society (2013)","DOI":"10.1109\/SYNASC.2013.35"},{"key":"18_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-41135-4_8","volume-title":"Tests and Proofs","author":"G Petiot","year":"2016","unstructured":"Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: Your proof fails? Testing helps to find the reason. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 130\u2013150. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41135-4_8"},{"key":"18_CR110","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"18_CR111","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-319-19249-9_26","volume-title":"FM 2015: Formal Methods","author":"N Polikarpova","year":"2015","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 414\u2013434. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_26"},{"key":"18_CR112","unstructured":"Praxis Critical Systems. SPARK\u2013The SPADE Ada Kernel, 3.2 edition (1996)"},{"key":"18_CR113","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/BFb0000503","volume-title":"Algebraic Methodology and Software Technology","author":"K Robinson","year":"1997","unstructured":"Robinson, K.: The B method and the B toolkit. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 576\u2013580. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0000503"},{"issue":"1","key":"18_CR114","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54\u201375 (2007)","journal-title":"Sci. Comput. Program."},{"key":"18_CR115","unstructured":"RTCA. DO-178C, Software Considerations in Airborne Systems and Equipment Certification, January 2012"},{"key":"18_CR116","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-662-43652-3_2","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS, vol. 8477, pp. 9\u201324. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_2"},{"key":"18_CR117","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-47846-3_5","volume-title":"Formal Methods and Software Engineering","author":"D Scheurer","year":"2016","unstructured":"Scheurer, D., H\u00e4hnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 57\u201373. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_5"},{"issue":"1","key":"18_CR118","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-016-0446-x","volume":"19","author":"B Steffen","year":"2017","unstructured":"Steffen, B.: The physics of software tools: SWOT analysis and vision. Softw. Tools Technol. Transf. (STTT) 19(1), 1\u20137 (2017)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"issue":"4","key":"18_CR119","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"18_CR120","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-662-46681-0_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Tschannen","year":"2015","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566\u2013580. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53"},{"key":"18_CR121","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: Black, A.P., Millstein, T.D. (eds.) Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA, Portland, OR, USA, pp. 691\u2013707. ACM (2014)","DOI":"10.1145\/2714064.2660243"},{"key":"18_CR122","unstructured":"Ulbrich, M.: Dynamic logic for an intermediate language: verification, interaction and refinement. Ph.D. thesis, Karlsruhe Institute of Technology (2013)"},{"key":"18_CR123","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40"},{"key":"18_CR124","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA 2013. ACM (2013)","DOI":"10.1145\/2509136.2509532"},{"key":"18_CR125","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"issue":"13","key":"18_CR126","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concur. Comput.: Pract. Exp. 13(13), 1173\u20131214 (2001)","journal-title":"Concur. Comput.: Pract. Exp."},{"issue":"5","key":"18_CR127","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s10009-012-0250-1","volume":"14","author":"PYH Wong","year":"2012","unstructured":"Wong, P.Y.H., Albert, E., Muschevici, R., Proen\u00e7a, J., Sch\u00e4fer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT 14(5), 567\u2013588 (2012)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,24]],"date-time":"2021-01-24T04:35:33Z","timestamp":1611462933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":127,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}