{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:27:11Z","timestamp":1752982031038},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"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-89439-1_24","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"333-342","source":"Crossref","is-referenced-by-count":15,"title":["Valigator: A Verification Tool with Bound and Invariant Generation"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[]},{"given":"Thibaud","family":"Hottelier","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"24_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY Tool. Software and System Modeling\u00a04(1), 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"24_CR2","volume-title":"High Integrity Software - The Spark Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software - The Spark Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"doi-asserted-by":"crossref","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: Proc. of FMC (2005)","key":"24_CR3","DOI":"10.1007\/11804192_17"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","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.) CASSIS 2004. LNCS, vol.\u00a03362. Springer, Heidelberg (2005)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2008), http:\/\/www.SMT-LIB.org","key":"24_CR6"},{"issue":"1","key":"24_CR7","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00008-8","volume":"35","author":"J. Brauburger","year":"1999","unstructured":"Brauburger, J., Giesl, J.: Approximating the Domains of Functional and Imperative Programs. Sci. Comput. Programming\u00a035(1), 113\u2013136 (1999)","journal-title":"Sci. Comput. Programming"},{"issue":"3-4","key":"24_CR8","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B.: An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal. J. of Symbolic Computation\u00a041(3-4), 475\u2013511 (2006)","journal-title":"J. of Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier Elimination for the Elementary Theory of RealClosed Fields by Cylindrical Algebraic Decomposition. LNCS, vol.\u00a033, pp. 134\u2013183 (1975)","key":"24_CR9","DOI":"10.1007\/3-540-07407-4_17"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL, pp. 238\u2013252 (1977)","key":"24_CR10","DOI":"10.1145\/512950.512973"},{"key":"24_CR11","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":"3","key":"24_CR12","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. of the ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. of the ACM"},{"key":"24_CR13","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"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: Proc. of PLDI, pp. 234\u2013245 (2002)","key":"24_CR14","DOI":"10.1145\/512529.512558"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590. Springer, Heidelberg (2007)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning Algebraically About P-Solvable Loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 249\u2013264. Springer, Heidelberg (2008)"},{"unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Technical Report 98-06u, Iowa State University (2003)","key":"24_CR17"},{"unstructured":"M\u00fcller, P., Meyer, J., Poetzsch-Heffter, A.: Programming and Interface Specification Language of Jive\u2014 specification and Design Rationale. Technical Report 223, University of Hagen (1997)","key":"24_CR18"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"unstructured":"Odersky, M.: The Scala Language Specification (2008), http:\/\/www.scala-lang.org","key":"24_CR20"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Shankar, N., Rushby, J.: VS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607. Springer, Heidelberg (1992)"},{"unstructured":"Seidl, H., Petter, M.: Inferring Polynomial Invariants with Polyinvar. In: Proc. of NSAD (2005)","key":"24_CR22"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP Compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"unstructured":"Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media (2003)","key":"24_CR24"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,21]],"date-time":"2023-05-21T03:01:42Z","timestamp":1684638102000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}