{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:41:39Z","timestamp":1725748899790},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410093"},{"type":"electronic","value":"9783642410109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41010-9_11","type":"book-chapter","created":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T09:31:39Z","timestamp":1379323899000},"page":"154-168","source":"Crossref","is-referenced-by-count":1,"title":["Auditing User-Provided Axioms in Software Verification Conditions"],"prefix":"10.1007","author":[{"given":"Paul","family":"Jackson","sequence":"first","affiliation":[]},{"given":"Florian","family":"Schanda","sequence":"additional","affiliation":[]},{"given":"Angela","family":"Wallenburg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Alt-Ergo: an OCAML SMT solver for software verification, homepage at \n                  \n                    http:\/\/alt-ergo.lri.fr\/"},{"key":"11_CR2","unstructured":"CVC3: an automatic theorem prover for Satisfiability Modulo Theories (SMT), homepage at \n                  \n                    http:\/\/cvc4.cs.nyu.edu"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s11219-011-9168-1","volume":"21","author":"K.Y. Ahn","year":"2013","unstructured":"Ahn, K.Y., Denney, E.: A framework for testing first-order logic axioms in program verification. Software Quality Journal\u00a021, 159\u2013200 (2013)","journal-title":"Software Quality Journal"},{"key":"11_CR4","unstructured":"Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: 1st International Symposium Secure Software Engineering (ISSSE). IEEE (2006), \n                  \n                    http:\/\/www.adacore.com\/sparkpro\/tokeneer"},{"key":"11_CR5","unstructured":"Barnes, J., with Altran\u00a0Praxis: SPARK: the proven approach to high Integrity Software. Altran Praxis (2012)"},{"key":"11_CR6","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.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006), \n                  \n                    http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/\n                  \n                  \n                 for current information on Boogie"},{"key":"11_CR7","unstructured":"Beckert, B., Bormer, T., Klebanov, V.: On essential program annotations and completeness of verifying compilers. In: Filli\u00e2tre, J.C., Freitas, L. (eds.) Proceedings, Workshop on Verified Software: Theory, Tools, and Experiments, VSTTE (2009)"},{"key":"11_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., , Melquiond, G., Paskevich, A.: The why3 platform, version 0.80. Tech. rep., University Paris-Sud, CNRS, Inria (October 2012), \n                  \n                    http:\/\/why3.lri.fr"},{"key":"11_CR9","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Leino, K.R.M., Moskal, M. (eds.) Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364 ( August 2011), \n                  \n                    http:\/\/proval.lri.fr\/publications\/boogie11final.pdf"},{"key":"11_CR10","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press (1979), \n                  \n                    http:\/\/www.cs.utexas.edu\/users\/boyer\/acl.pdf"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: Quickcheck: A lightweight tool for random testing of haskell programs. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"},{"key":"11_CR12","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)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Crocker, D., Carlton, J.: Verification of c programs using automated reasoning. In: Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 7\u201314. IEEE Computer Society (2007)","DOI":"10.1109\/SEFM.2007.44"},{"key":"11_CR14","unstructured":"Dutertre, B., de\u00a0Moura, L.: The Yices SMT solver (August 2006), tool paper at \n                  \n                    http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"11_CR15","unstructured":"King, J.C.: A Program Verifier. Ph.D. thesis, Carnegie-Mellon University (1969)"},{"key":"11_CR16","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002), \n                  \n                    http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\n                  \n                  \n                 for current information"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41010-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T09:56:34Z","timestamp":1558086994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41010-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410093","9783642410109"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41010-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}