{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:01:55Z","timestamp":1767772915748,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243714"},{"type":"electronic","value":"9783642243721"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24372-1_3","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T09:41:14Z","timestamp":1317289274000},"page":"28-42","source":"Crossref","is-referenced-by-count":22,"title":["Making Software Verification Tools Really Work"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Adve, S., Hill, M.: Weak Ordering \u2013 A New Definition. In: ISCA (1990)","DOI":"10.1145\/325164.325100"},{"key":"3_CR2","unstructured":"Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Tech. Rep. 2000-14, Microsoft Research (February 2000)"},{"key":"3_CR3","first-page":"35","volume-title":"FMCAD","author":"T. Ball","year":"2010","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: FMCAD, pp. 35\u201342. IEEE, Los Alamitos (2010)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-14295-6_11","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2010","unstructured":"Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 119\u2013122. Springer, Heidelberg (2010)"},{"key":"3_CR5","first-page":"1","volume-title":"Principles of Programming Languages (POPL)","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Principles of Programming Languages (POPL), pp. 1\u20133. ACM, New York (2002)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"3_CR7","unstructured":"Ball, T., Rajamani, S.K.: SLIC: a specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2001)"},{"key":"3_CR8","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":"3_CR9","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), http:\/\/www.smt-lib.org"},{"key":"3_CR10","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010)"},{"key":"3_CR11","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: BLAST documentation, http:\/\/www.sosy-lab.org\/~dbeyer\/blast_doc\/ (retrieved July 11, 2011)"},{"issue":"5-6","key":"3_CR12","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. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: cPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"issue":"2-4","key":"3_CR14","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"3_CR16","first-page":"69","volume-title":"FMCAD","author":"A. Brillout","year":"2009","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD, pp. 69\u201376. IEEE, Los Alamitos (2009)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Information and Computation (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM) (2003)","DOI":"10.1145\/876638.876643"},{"key":"3_CR20","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., Kr\u00f6ning, 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_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD), 105\u2013127 (2004)","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"3_CR22","volume-title":"EuroSys","author":"P. Collingbourne","year":"2011","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys. ACM, New York (2011)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"3_CR24","unstructured":"Satisfiability: Suggested Format (1993), ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"SAS","author":"A. Donaldson","year":"2011","unstructured":"Donaldson, A., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 351\u2013368. Springer, Heidelberg (2011)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"Computer Aided Verification","author":"A. Donaldson","year":"2011","unstructured":"Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 356\u2013371. Springer, Heidelberg (2011)"},{"issue":"1","key":"3_CR27","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-011-0124-2","volume":"39","author":"A.F. Donaldson","year":"2011","unstructured":"Donaldson, A.F., Kroening, D., Ruemmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods in System Design\u00a039(1), 83\u2013113 (2011)","journal-title":"Formal Methods in System Design"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Fraser, K., Harris, T.: Concurrent Programming Without Locks. ACM Trans. Comput. Syst. 25(2) (2007)","DOI":"10.1145\/1233307.1233309"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Hoare, C., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: A manifesto. ACM Comput. Surv. 41, article 22 (October 2009)","DOI":"10.1145\/1592434.1592439"},{"key":"3_CR33","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)"},{"issue":"5","key":"3_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivancic","year":"2005","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-69850-0_3","volume-title":"25 Years of Model Checking","author":"R.P. Kurshan","year":"2008","unstructured":"Kurshan, R.P.: Verification technology transfer. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 46\u201364. Springer, Heidelberg (2008)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M.Z. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"issue":"7","key":"3_CR38","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput.\u00a046(7), 779\u2013782 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR39","first-page":"1441","volume-title":"VLDB","author":"I. Manolescu","year":"2007","unstructured":"Manolescu, I., Manegold, S.: Performance evaluation and experimental assessment \u2013 conscience or curse of database research? In: VLDB, pp. 1441\u20131442. ACM, New York (2007)"},{"key":"3_CR40","unstructured":"McKenney, P.: http:\/\/www.rdrop.com\/users\/paulmck\/RCU\/"},{"key":"3_CR41","first-page":"295","volume-title":"RE","author":"H. Post","year":"2009","unstructured":"Post, H., Sinz, C., Merz, F., Gorges, T., Kropf, T.: Linking functional requirements and software verification. In: RE, pp. 295\u2013302. IEEE Computer Society, Los Alamitos (2009)"},{"key":"3_CR42","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Steffen, B.: Major threat: From formal methods without tools to tools without formal methods. In: ICECCS, p. 15. IEEE Computer Society, Los Alamitos (2004), panel discussion","DOI":"10.1109\/ICECCS.2004.1310899"},{"key":"3_CR45","unstructured":"Veldhuizen, T.L.: C++ templates are Turing complete. Tech. rep. (2003), http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.14.3670 (retrieved July 11, 2011)"},{"key":"3_CR46","first-page":"463","volume-title":"CHI Extended Abstracts","author":"M.L. Wilson","year":"2011","unstructured":"Wilson, M.L., Mackay, W., Chi, E., Bernstein, M., Russell, D., Thimbleby, H.: RepliCHI \u2013 CHI should be replicating and validating results more: discuss. In: CHI Extended Abstracts, pp. 463\u2013466. ACM, New York (2011)"}],"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-642-24372-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T06:03:36Z","timestamp":1741759416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24372-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243714","9783642243721"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24372-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}