{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,14]],"date-time":"2024-09-14T01:13:37Z","timestamp":1726276417022},"publisher-location":"Berlin, Heidelberg","reference-count":71,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705437"},{"type":"electronic","value":"9783540705451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_4","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"11-18","source":"Crossref","is-referenced-by-count":6,"title":["Theorem Proving for Verification (Invited Tutorial)"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"2000","unstructured":"Aagaard, M., Harrison, J. (eds.): TPHOLs 2000. LNCS, vol.\u00a01869. Springer, Heidelberg (2000)"},{"key":"4_CR2","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2008","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol.\u00a04. IOS Press, Amsterdam (2008)"},{"key":"4_CR3","series-title":"ACM Monograph Series","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monograph Series. Academic Press, London (1979)"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/BF01844169","volume":"4","author":"B. Buchberger","year":"1970","unstructured":"Buchberger, B.: Ein algorithmisches Kriterium fur die L\u00f6sbarkeit eines algebraischen Gleichungssystems. Aequationes Mathematicae\u00a04, 374\u2013383 (1970); English translation, An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations. In: [6], pp. 535\u2013545","journal-title":"Aequationes Mathematicae"},{"key":"4_CR6","series-title":"London Mathematical Society Lecture Note Series","volume-title":"Gr\u00f6bner Bases and Applications","year":"1998","unstructured":"Buchberger, B., Winkler, F. (eds.): Gr\u00f6bner Bases and Applications. London Mathematical Society Lecture Note Series, vol.\u00a0251. Cambridge University Press, Cambridge (1998)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"4_CR8","first-page":"308","volume-title":"Information Processing 1974: Proceedings of IFIP Congress 1974","author":"R.M. Burstall","year":"1974","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974: Proceedings of IFIP Congress 1974, Stockholm, pp. 308\u2013312. North-Holland, Amsterdam (1974)"},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1109\/DAC.1979.1600119","volume-title":"Proceedings of the 16th ACM\/IEEE Design Automation Conference","author":"W.C. Carter","year":"1979","unstructured":"Carter, W.C., Joyner, W.H., Brand, D.: Symbolic simulation for correct machine design. In: Proceedings of the 16th ACM\/IEEE Design Automation Conference, pp. 280\u2013286. IEEE Computer Society Press, Los Alamitos (1979)"},{"key":"4_CR10","series-title":"Texts and monographs in symbolic computation","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and monographs in symbolic computation. Springer, Heidelberg (1998)"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00244942","volume":"4","author":"S.-C. Chou","year":"1988","unstructured":"Chou, S.-C.: An introduction to Wu\u2019s method for mechanical theorem proving in geometry. Journal of Automated Reasoning\u00a04, 237\u2013267 (1988)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A. Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number-theory. American Journal of Mathematics\u00a058, 345\u2013363 (1936)","journal-title":"American Journal of Mathematics"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd ACM Symposium on the Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"volume-title":"The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions","year":"1965","key":"4_CR16","unstructured":"Davis, M. (ed.): The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Raven Press, NY (1965)"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"4_CR19","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Symposium on Automatic Demonstration","author":"N.G. Bruijn de","year":"1970","unstructured":"de Bruijn, N.G.: The mathematical language AUTOMATH, its usage and some of its extensions. In: Laudet, M., Lacombe, D., Nolin, L., Sch\u00fctzenberger, M. (eds.) Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol.\u00a0125, pp. 29\u201361. Springer, Heidelberg (1970)"},{"key":"4_CR20","first-page":"589","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project AUTOMATH. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 589\u2013606. Academic Press, London (1980)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"4_CR23","unstructured":"Fontaine, P.: Techniques for verification of concurrent systems with invariants. PhD thesis, Institut Montefiore, Universit\u00e9 de Li\u00e8ge (2004)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P.C. Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory: Its justification and realization. IBM Journal of research and development\u00a04, 28\u201335 (1960)","journal-title":"IBM Journal of research and development"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme, I. Monatshefte f\u00fcr Mathematik und Physik\u00a038, 173\u2013198 (1931); English translation, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I. In: [67], pp. 592\u2013618 or [16], pp. 4\u201338","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1109\/DATE.2002.998262","volume-title":"Design, Automation and Test in Europe Conference and Exhibition (DATE 2002)","author":"E. Goldberg","year":"2002","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust Sat-solver. In: Kloos, C.D., Franca, J.D. (eds.) Design, Automation and Test in Europe Conference and Exhibition (DATE 2002), Paris, France, pp. 142\u2013149. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"4_CR27","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M.J.C. Gordon","year":"1989","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer, Heidelberg (1989)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J.R. Guard","year":"1969","unstructured":"Guard, J.R., Oglesby, F.C., Bennett, J.H., Settle, L.G.: Semi-automated mathematics. Journal of the ACM\u00a016, 49\u201362 (1969)","journal-title":"Journal of the ACM"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_14","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 217\u2013233. Springer, Heidelberg (2000)"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard and Harrison [1], pp. 234\u2013251","DOI":"10.1007\/3-540-44659-1_15"},{"key":"4_CR32","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A sceptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning\u00a021, 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","volume":"4","author":"J.N. Hooker","year":"1988","unstructured":"Hooker, J.N.: A quantitative approach to logical inference. Decision Support Systems\u00a04, 45\u201369 (1988)","journal-title":"Decision Support Systems"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"4_CR35","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-57826-9_135","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J.J. Joyce","year":"1994","unstructured":"Joyce, J.J., Seger, C.: The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In: Joyce, J.J., Seger, C. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 185\u2013198. Springer, Heidelberg (1994)"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In: Aagaard and Harrison [1], pp. 338\u2013355","DOI":"10.1007\/3-540-44659-1_21"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-44798-9_18","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Kaivola","year":"2001","unstructured":"Kaivola, R., Kohatsu, K.: Proof engineering in the large: Formal verification of the Pentium (R) 4 floating-point divider. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 196\u2013211. Springer, Heidelberg (2001)"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0032842","volume-title":"EUROSAM 84","author":"A. Kandri-Rody","year":"1984","unstructured":"Kandri-Rody, A., Kapur, D.: Algorithms for computing Gr\u00f6bner bases of polynomial ideals over various Euclidean rings. In: Fitch, J. (ed.) EUROSAM 1984 and ISSAC 1984. LNCS, vol.\u00a0174, pp. 195\u2013206. Springer, Heidelberg (1984)"},{"key":"4_CR40","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S. Krstic","year":"2007","unstructured":"Krstic, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 1\u201327. Springer, Heidelberg (2007)"},{"key":"4_CR41","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P.W. Markstein","year":"1990","unstructured":"Markstein, P.W.: Computation of elementary functions on the IBM RISC System\/6000 processor. IBM Journal of Research and Development\u00a034, 111\u2013119 (1990)","journal-title":"IBM Journal of Research and Development"},{"key":"4_CR42","first-page":"354","volume":"11","author":"Y.V. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.V.: Enumerable sets are Diophantine. Soviet Mathematics Doklady\u00a011, 354\u2013358 (1970)","journal-title":"Soviet Mathematics Doklady"},{"key":"4_CR43","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019, 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61398-6","volume-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"W. McCune","year":"1996","unstructured":"McCune, W., Padmanabhan, R.: Automated Deduction in Equational Logic and Cubic Curves. LNCS, vol.\u00a01095. Springer, Heidelberg (1996)"},{"key":"4_CR45","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5 K 86 floating-point division program. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR46","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/378239.379017","volume-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"4_CR47","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR48","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM\u00a053, 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"4_CR49","first-page":"1","volume":"1999","author":"J. O\u2019Leary","year":"1999","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal\u00a01999-Q1, 1\u201314 (1999), http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm","journal-title":"Intel Technology Journal"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201367 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031. Springer, Heidelberg (2001)"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","first-page":"195","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 195\u2013220. Springer, Heidelberg (1982)"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer Aided Verification","author":"S. Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.K.: An integration of model-checking with automated proof-checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 84\u201397. Springer, Heidelberg (1995)"},{"key":"4_CR54","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"4_CR55","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"4_CR56","unstructured":"Seger, C., Joyce, J.J. : A two-level formal verification methodology using HOL and COSMOS. Technical Report 91-10, Department of Computer Science, University of British Columbia, 2366 Main Mall, University of British Columbia, Vancouver, B.C, Canada V6T 1Z4 (1991)"},{"key":"4_CR57","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06, 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-70952-7_1","volume-title":"Formal Methods: Applications and Technology","author":"A. Slobodov\u00e1","year":"2007","unstructured":"Slobodov\u00e1, A.: Challenges for Formal Verification in Industrial Setting. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 1\u201322. Springer, Heidelberg (2007)"},{"key":"4_CR59","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/B978-0-08-040953-5.50011-8","volume-title":"Safety of Computer Control Systems, (SAFECOMP 1990)","author":"G. St\u00e5lmarck","year":"1990","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modeling and verifying systems and software in propositional logic. In: Daniels, B.K. (ed.) Safety of Computer Control Systems (SAFECOMP 1990), Gatwick, UK, pp. 31\u201336. Pergamon Press, Oxford (1990)"},{"key":"4_CR60","first-page":"261","volume":"1","author":"A. Tarski","year":"1936","unstructured":"Tarski, A.: Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica\u00a01, 261\u2013405 (1936); English translation, The Concept of Truth in Formalized Languages. In: [62], pp. 152\u2013278","journal-title":"Studia Philosophica"},{"key":"#cr-split#-4_CR61.1","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951);","DOI":"10.1525\/9780520348097"},{"key":"#cr-split#-4_CR61.2","unstructured":"Previous version published as a technical report by the RAND Corporation (1948); prepared for publication by McKinsey, J.C.C. Reprinted In: [10], pp. 24???84"},{"key":"4_CR62","unstructured":"Tarski, A. (ed.): Logic, Semantics and Metamathematics. Clarendon Press (1956)"},{"key":"4_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-74591-4_24","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Th\u00e9ry","year":"2007","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 319\u2013333. Springer, Heidelberg (2007)"},{"key":"4_CR64","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Trybulec, A.: The Mizar-QC\/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing)\u00a06, 136\u2013140 (1978)","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"4_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/3-540-15648-8_30","volume-title":"Logics of Programs","author":"A. Trybulec","year":"1985","unstructured":"Trybulec, A., Blair, H.A.: Computer aided reasoning. In: Parikh, R. (ed.) Logics of Programs, Brooklyn. LNCS, vol.\u00a0193, pp. 406\u2013412. Springer, Heidelberg (1985)"},{"issue":"2","key":"4_CR66","first-page":"230","volume":"42","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society\u00a042(2), 230\u2013265 (1936)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"4_CR67","unstructured":"van Heijenoort, J. (ed.): From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879\u20131931. Harvard University Press (1967)"},{"key":"4_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M. Vardi","year":"1996","unstructured":"Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"4_CR69","first-page":"157","volume":"21","author":"W. Wen-ts\u00fcn","year":"1978","unstructured":"Wen-ts\u00fcn, W.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica\u00a021, 157\u2013179 (1978)","journal-title":"Scientia Sinica"},{"key":"4_CR70","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World","author":"F. Wiedijk","year":"2006","unstructured":"Wiedijk, F.: The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T18:15:52Z","timestamp":1631643352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}