{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:53Z","timestamp":1725516533582},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_53","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"491-495","source":"Crossref","is-referenced-by-count":2,"title":["The Importance of Non-theorems and Counterexamples in Program Verification"],"prefix":"10.1007","author":[{"given":"Graham","family":"Steel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"W. Ahrendt","year":"2002","unstructured":"Ahrendt, W.: Deductive search for errors in free data type specifications using model generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"},{"key":"53_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"53_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"53_CR4","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Proceedings of the, European Symposium on Research in Computer Security, pp. 253\u2013270, 2003. Extended version available as Technical Report 404, ETH Zurich (2003)","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"53_CR5","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), pp. 230\u2013239 (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"issue":"5","key":"53_CR6","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the Association for Computing Machinery\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"1-2","key":"53_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation\u00a0159(1-2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"key":"53_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"47","volume-title":"Automated Reasoning","author":"L.A. Dennis","year":"2004","unstructured":"Dennis, L.A.: The use of proof planning critics to diagnose errors in the base cases of recursive programs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 47\u201358. Springer, Heidelberg (2004)"},{"issue":"2","key":"53_CR9","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"53_CR10","unstructured":"McCune, W.: A Davis Putnam program and its application to finite first order model search. Technical report, Argonne National Laboratory (1994)"},{"key":"53_CR11","doi-asserted-by":"crossref","unstructured":"Monroy, R.: Predicate synthesis for correcting faulty conjectures: The proof planning paradigm. In: Automated Software Engineering, pp. 247\u2013269 (2003)","DOI":"10.1023\/A:1024448931103"},{"key":"53_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"53_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. Paulson","year":"1998","unstructured":"Paulson, L.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"53_CR14","unstructured":"Pike, L., Miner, P., Torres, W.: Model checking failed conjectures in theorem proving: a case study. Technical Report NASA\/TM\u20132004\u2013213278, NASA Langley Research Center (November 2004), http:\/\/www.cs.indiana.edu\/~lepike\/pub_pages\/unproven.html"},{"key":"53_CR15","volume-title":"Numerical Recipes in C: The Art of Scientific Computing","author":"W. Press","year":"1992","unstructured":"Press, W., Teukolsky, S., Vetterling, W., Flannery, B.: Numerical Recipes in C: The Art of Scientific Computing. Cambridge University Press, Cambridge (1992)"},{"key":"53_CR16","series-title":"Springer Lecture Notes in Artificial Intelligence","first-page":"340","volume-title":"11th Conference on Automated Deduction","author":"M. Protzen","year":"1992","unstructured":"Protzen, M.: Disproving conjectures. In: Kapur, D. (ed.) 11th Conference on Automated Deduction, Saratoga Springs, NY, USA, June 1992. Springer Lecture Notes in Artificial Intelligence, vol.\u00a0(607), pp. 340\u2013354. Springer, Heidelberg (1992)"},{"key":"53_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_52","volume-title":"Automated Reasoning","author":"W. Reif","year":"2001","unstructured":"Reif, W., Schellhorn, G., Thums, A.: Flaw detection in formal specifications. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, Springer, Heidelberg (2001)"},{"key":"53_CR18","doi-asserted-by":"crossref","unstructured":"Slaney, J.: FINDER: Finite Domain Enumerator. In: Australian National University (1995), ftp:\/\/arp.anu.edu.au\/pub\/papers\/slaney\/finder\/finder.ps.gz","DOI":"10.1007\/3-540-58156-1_63"},{"issue":"1","key":"53_CR19","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.entcs.2004.05.023","volume":"125","author":"G. Steel","year":"2004","unstructured":"Steel, G., Bundy, A.: Attacking group multicast key management protocols using CORAL. Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0125(1), 125\u2013144 (2004) (Also available as Informatics Research Report EDI-INF-RR-0241. Presented at the ARSPA workshop 2004)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"53_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-25984-8_8","volume-title":"Automated Reasoning","author":"G. Steel","year":"2004","unstructured":"Steel, G., Bundy, A., Maidl, M.: Attacking a protocol for group key agreement by refuting incorrect inductive conjectures. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 137\u2013151. Springer, Heidelberg (2004)"},{"key":"53_CR21","series-title":"Lecture Notes in Artificial Intelligence","first-page":"27","volume-title":"Automated Reasoning","author":"T. Weber","year":"2004","unstructured":"Weber, T.: Bounded model generation for Isabelle\/HOL. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 27\u201336. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:44:31Z","timestamp":1557719071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}