{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:29Z","timestamp":1725516509400},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_17","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"153-160","source":"Crossref","is-referenced-by-count":2,"title":["Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification"],"prefix":"10.1007","author":[{"given":"Joseph R.","family":"Kiniry","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrice","family":"Chalin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cl\u00e9ment","family":"Hurlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Breunesse, C.-B.: On JML: Topics in Tool-assisted Verification of Java Programs. PhD thesis, Radboud University Nijmegen (2006)"},{"issue":"3","key":"17_CR2","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"17_CR3","unstructured":"Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide (2000)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (1999)","DOI":"10.1007\/3-540-48118-4_39"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","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\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"17_CR9","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification, 1st edn. (August 1996)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: JavaCard program verification. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics TPHOL 2001, vol.\u00a02151, pp. 1\u20133 (2001)","DOI":"10.1007\/3-540-44755-5_1"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-27815-3_5","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Counting votes with formal methods. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 21\u201322. Springer, Heidelberg (2004)"},{"key":"17_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":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"J.R. Kiniry","year":"2005","unstructured":"Kiniry, J.R., Cok, D.R.: ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"17_CR14","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual. Department of Computer Science, Iowa State University, 226 Atanasoff Hall, draft revision 1.94 edition (2004)"},{"key":"17_CR15","unstructured":"The MOBIUS project. http:\/\/mobius.inria.fr\/"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Ranise, S., Deharbe, D.: Light-weight theorem proving for debugging and verifying units of code. In: International Conference on Software Engineering and Formal Methods SEFM 2003, Canberra, Australia (September 2003)","DOI":"10.1109\/SEFM.2003.1236224"},{"issue":"2","key":"17_CR17","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.entcs.2005.12.050","volume":"157","author":"F. Rioux","year":"2006","unstructured":"Rioux, F., Chalin, P.: Improving the quality of web-based enterprise applications with extended static checking: A case study. Electronic Notes in Theoretical Computer Science\u00a0157(2), 119\u2013132 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR18","unstructured":"RTI: Health, Social, and Economics Research, Research Triangle Park, NC. The economic impacts of inadequate infrastructure for software testing. Technical Report Planning Report 02-3, NIST (May 2002)"},{"key":"17_CR19","unstructured":"SMT-LIB: The satisfiability modulo theories library. http:\/\/goedel.cs.uiowa.edu\/smtlib\/"},{"key":"17_CR20","unstructured":"The Systems Research Group GForge. http:\/\/sort.ucd.ie\/"}],"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_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:40Z","timestamp":1557718960000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}