{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T11:56:50Z","timestamp":1710935810039},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T00:00:00Z","timestamp":1266537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,11]]},"DOI":"10.1007\/s10009-010-0138-x","type":"journal-article","created":{"date-parts":[[2010,2,18]],"date-time":"2010-02-18T06:00:04Z","timestamp":1266472804000},"page":"467-481","source":"Crossref","is-referenced-by-count":17,"title":["Improved usability and performance of SMT solvers for debugging specifications"],"prefix":"10.1007","volume":"12","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,19]]},"reference":[{"issue":"3","key":"138_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/373243.360220","volume":"36","author":"C. Flanagan","year":"2001","unstructured":"Flanagan C., Saxe J.B.: Avoiding exponential explosion: generating compact verification conditions. SIGPLAN Not. 36(3), 193\u2013205 (2001)","journal-title":"SIGPLAN Not."},{"issue":"6","key":"138_CR2","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K.R.M. Leino","year":"2005","unstructured":"Leino K.R.M.: Efficient weakest preconditions. Inform. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inform. Process. Lett."},{"issue":"4","key":"138_CR3","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/s10817-006-9026-1","volume":"35","author":"C. Barrett","year":"2005","unstructured":"Barrett C., de Moura L., Stump A.: Design and results of the 1st satisfiability modulo theories competition (SMT-COMP 2005). J. Autom. Reason. 35(4), 373\u2013390 (2005)","journal-title":"J. Autom. Reason."},{"key":"138_CR4","unstructured":"The SMT-COMP web site provides results of the SMT competition and links to the system descriptions of the participants. http:\/\/smtcomp.org"},{"key":"138_CR5","volume-title":"Z: An Introduction to Formal Methods","author":"A. Diller","year":"1994","unstructured":"Diller A.: Z: An Introduction to Formal Methods. 2nd edn. Wiley, New York (1994)","edition":"2"},{"key":"138_CR6","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer B.: Object-oriented Software Construction. Prentice Hall, New York, NY (1988)"},{"key":"138_CR7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens G.T., Baker A.L., Ruby C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"138_CR8","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual. Available from http:\/\/www.jmlspecs.org (May 2008)"},{"key":"138_CR9","unstructured":"JML web site. http:\/\/www.jmlspecs.org"},{"key":"138_CR10","doi-asserted-by":"crossref","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.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), vol. 3362 of Lecture Notes in Computer Science, pp. 49\u201369. Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"138_CR11","unstructured":"Spec# web site. http:\/\/research.microsoft.com\/SpecSharp"},{"key":"138_CR12","doi-asserted-by":"crossref","unstructured":"Luckham, D.C., von Henke, F.W., Krieg-Br\u00fcckner, B., Owe, O.: ANNA\u2014A Language for Annotating Ada Programs, Reference Manual, vol. 260 of Lecture Notes in Computer Science. Springer (1987)","DOI":"10.1007\/3-540-17980-1"},{"key":"138_CR13","unstructured":"ACSL web site. http:\/\/www.frama-c.cea.fr\/acsl.html"},{"key":"138_CR14","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70. Microsoft Research (2005)"},{"key":"138_CR15","unstructured":"Why web site. http:\/\/why.lri.fr"},{"key":"138_CR16","unstructured":"The SMTLIB web site hosts benchmarks for SMT solvers and defines a common SMT input language. http:\/\/combination.cs.uiowa.edu\/smtlib"},{"issue":"3","key":"138_CR17","doi-asserted-by":"crossref","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 52(3), 365\u2013473 (2005)","journal-title":"J ACM"},{"key":"138_CR18","unstructured":"Rushby, J.: Tutorial: automated formal methods with PVS, SAL, and Yices. In: Fourth IEEE International Conference on Software Engineering and Formal Methods, 2006 (SEFM 2006), 11\u201315 September 2006"},{"key":"138_CR19","unstructured":"Yices web site. http:\/\/yices.csl.sri.com"},{"key":"138_CR20","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, Proceedings of 19th International Conference (CAV 2007) Berlin, Germany, 3\u20137 July 2007, vol. 4590 of Lecture Notes in Computer Science, pp 298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"138_CR21","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"138_CR22","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference, Version 2.4. SRI International (2001)"},{"key":"138_CR23","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover, vol. 828 of Lecture Notes in Computer Science. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"138_CR24","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML: progress and issues in building and using ESC\/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L.,Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), vol. 3362 of Lecture Notes in Computer Science, pp. 108\u2013128. Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"138_CR25","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"138_CR26","unstructured":"KeY web site. http:\/\/www.key-project.org"},{"key":"138_CR27","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Ernst, M.D., Jensen, T.P. (eds.) Program Analysis for Software Tools and Engineering (PASTE). ACM (September 2005)","DOI":"10.1145\/1108792.1108813"},{"key":"138_CR28","unstructured":"Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC\/Java User\u2019s Manual. Technical Note. Compaq Systems Research Center (October 2000)"},{"key":"138_CR29","unstructured":"CodeSonar\u00ae web site. http:\/\/www.grammatech.com\/products\/codesonar"},{"key":"138_CR30","doi-asserted-by":"crossref","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: A Developer-oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods: International Symposium of Formal Methods Europe, vol. 2805 of Lecture Notes in Computer Science, pp. 422\u2013439. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_24"},{"key":"138_CR31","first-page":"2002","volume":"45","author":"J.J. Cook","year":"2002","unstructured":"Cook J.J.: Reverse Execution of Java Bytecode. Comput. J. 45, 2002 (2002)","journal-title":"Comput. J."},{"key":"138_CR32","unstructured":"Lewis, B.: Debugging Backwards in Time (2003)"},{"key":"138_CR33","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical Report. Department of Computer Science, The University of Iowa (2006). Available at http:\/\/www.SMT-LIB.org"},{"key":"138_CR34","unstructured":"OpenJDK web site. http:\/\/openjdk.java.net"},{"key":"138_CR35","doi-asserted-by":"crossref","unstructured":"Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: DAC \u201994: Proceedings of the 31st Annual Conference on Design Automation, ACM, pp. 596\u2013602. New York, NY, USA (1994)","DOI":"10.1145\/196244.196575"},{"key":"138_CR36","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: CAV \u201997: Proceedings of the 9th International Conference on Computer Aided Verification, vol. 1254 of Lecture Notes in Computer Science, pp. 279\u2013290. Springer, London, UK (1997)","DOI":"10.1007\/3-540-63166-6_28"},{"key":"138_CR37","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS \u201907: Proceedings of the 2007 Conference on Specification and Verification of Component-based Systems, ACM, pp. 23\u201330. New York, NY, USA (2007)","DOI":"10.1145\/1292316.1292319"},{"key":"138_CR38","doi-asserted-by":"crossref","unstructured":"Egyed, A.: Instant consistency checking for the UML. In: ICSE \u201906: Proceedings of the 28th International Conference on Software Engineering, ACM, pp. 381\u2013390. New York, NY, USA (2006)","DOI":"10.1145\/1134285.1134339"},{"key":"138_CR39","doi-asserted-by":"crossref","unstructured":"Smaragdakis, Y., Csallner, C., Subramanian, R.: Scalable satisfiability checking and test data generation from modeling diagrams. Autom. Softw. Eng. 16(1) (2009)","DOI":"10.1007\/s10515-008-0044-6"},{"key":"138_CR40","unstructured":"Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting. Available at http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=77373 (2008)"}],"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-010-0138-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0138-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0138-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:26Z","timestamp":1559100326000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0138-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,19]]},"references-count":40,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,11]]}},"alternative-id":["138"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0138-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,19]]}}}