{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:04:59Z","timestamp":1740096299504,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642389153"},{"type":"electronic","value":"9783642389160"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38916-0_4","type":"book-chapter","created":{"date-parts":[[2013,6,9]],"date-time":"2013-06-09T22:13:47Z","timestamp":1370816027000},"page":"56-75","source":"Crossref","is-referenced-by-count":4,"title":["A Metric for Testing Program Verification Systems"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Thorsten","family":"Bormer","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Wagner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-13977-2_4","volume-title":"Tests and Proofs","author":"K.Y. Ahn","year":"2010","unstructured":"Ahn, K.Y., Denney, E.: Testing first-order logic axioms in program verification. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 22\u201337. Springer, Heidelberg (2010)"},{"key":"4_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/11591191_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Roth, A., Sasse, R.: Automatic validation of transformation rules for Java verification against a rewriting semantics. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 412\u2013426. Springer, Heidelberg (2005)"},{"key":"4_CR3","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB), \n                  \n                    http:\/\/www.smt-lib.org\/"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-540-75336-0_2","volume-title":"Trustworthy Global Computing","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., et al.: MOBIUS: Mobility, Ubiquity, Security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 10\u201329. Springer, Heidelberg (2007), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/978-3-540-75336-0_2"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-25271-6_4","volume-title":"Formal Methods for Components and Objects","author":"B. Beckert","year":"2011","unstructured":"Beckert, B., Bormer, T., Klebanov, V.: Improving the usability of specification languages and methods for annotation-based verification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 61\u201379. Springer, Heidelberg (2011)"},{"key":"4_CR6","series-title":"LNAI","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"4_CR7","unstructured":"Beckert, B., Klebanov, V.: Must program verification systems and calculi be verified? In: 3rd International Verification Workshop (VERIFY), Workshop at Federated Logic Conferences (FLoC), pp. 34\u201341 (2006)"},{"key":"4_CR8","unstructured":"B\u00f6hme, S.: Proof reconstruction for Z3 in Isabelle\/HOL. In: 7th International Workshop on Satisfiability Modulo Theories, SMT 2009 (2009)"},{"key":"4_CR9","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.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing\u00a07(1), 70\u201390 (1978)","journal-title":"SIAM Journal of Computing"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-28891-3_12","volume-title":"NASA Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Monate, B., Pacalet, A., Prevosto, V., Regehr, J., Yakobowski, B., Yang, X.: Testing static analyzers with randomly generated programs. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 120\u2013125. Springer, Heidelberg (2012), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/978-3-642-28891-3_12"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-37621-7_7","volume-title":"Software Security - Theories and Systems","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 134\u2013153. Springer, Heidelberg (2004)"},{"key":"4_CR13","unstructured":"Jones, D.: Who guards the guardians? (February 1997), \n                  \n                    http:\/\/www.knosof.co.uk\/whoguard.html"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1109\/TSE.2004.24","volume":"30","author":"D.R. Kuhn","year":"2004","unstructured":"Kuhn, D.R., Wallace, D.R., Gallo, A.M.: Software fault interactions and implications for software testing. IEEE Transactions on Software Engineering\u00a030(6), 418\u2013421 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR15","unstructured":"Lochbihler, A.: A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. Ph.D. thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik (July 2012), \n                  \n                    http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000028867"},{"key":"4_CR16","unstructured":"March\u00e9, C., Moy, Y.: The Jessie plugin for Deductive Verification in Frama-C\u2014Tutorial and Reference Manual (2013), \n                  \n                    http:\/\/krakatoa.lri.fr\/jessie.pdf"},{"key":"4_CR17","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"13","key":"4_CR18","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. Concurrency and Computation Practice and Experience\u00a013(13), 1173\u20131214 (2001)","journal-title":"Concurrency and Computation Practice and Experience"},{"key":"4_CR19","unstructured":"R Core Team: R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing, Vienna, Austria (2012), \n                  \n                    http:\/\/www.R-project.org"},{"key":"4_CR20","unstructured":"von Wright, J.: The formal verification of a proof checker, SRI internal report (1994)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 283\u2013294. ACM (2011)","DOI":"10.1145\/1993316.1993532"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38916-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T21:40:52Z","timestamp":1557783652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38916-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389153","9783642389160"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38916-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}