乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T17:33:36Z","timestamp":1732037616008},"publisher-location":"Cham","reference-count":79,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_20","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"651-684","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Combining Model Checking and Deduction"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"20_CR1","volume-title":"Handbook of Model Checking","author":"P.A. Abdulla","year":"2018","unstructured":"Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"2","key":"20_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR3","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, Cambridge (1986)"},{"issue":"4","key":"20_CR4","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey\u2014Part\u00a01. Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"Trans. Program. Lang. Syst."},{"key":"20_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090","volume-title":"Computational Complexity: A\u00a0Modern Approach","author":"S. Arora","year":"2009","unstructured":"Arora, S., Barak, B.: Computational Complexity: A\u00a0Modern Approach. Cambridge University Press, Cambridge (2009)"},{"key":"20_CR6","first-page":"203","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0203\u2013313. ACM, New York (2001)"},{"key":"20_CR7","volume-title":"Handbook of Model Checking","author":"C.W. Barrett","year":"2018","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0049-237X(08)71097-8","volume-title":"Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics","author":"J. Barwise","year":"1978","unstructured":"Barwise, J.: First-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, vol.\u00a090, pp.\u00a05\u201346. North-Holland, Amsterdam (1978)"},{"key":"20_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). Coq home page: http:\/\/coq.inria.fr\/"},{"key":"20_CR10","volume-title":"Handbook of Model Checking","author":"A. Biere","year":"2018","unstructured":"Biere, A., Kroening, D.: SAT-based model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR11","volume-title":"Modal Logic","author":"P. Blackburn","year":"2002","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)"},{"key":"20_CR12","volume-title":"Handbook of Model Checking","author":"R. Bloem","year":"2018","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem. Perspectives in Mathematical Logic","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997)"},{"key":"20_CR14","volume-title":"Handbook of Model Checking","author":"P. Bouyer","year":"2018","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR15","volume-title":"Handbook of Model Checking","author":"J. Bradfield","year":"2018","unstructured":"Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a06538, pp.\u00a070\u201387. Springer, Heidelberg (2011)"},{"key":"20_CR17","series-title":"LNCS","first-page":"1","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"A.R. Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a07317, pp.\u00a01\u201314. Springer, Heidelberg (2012)"},{"key":"20_CR18","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"20_CR19","volume-title":"Handbook of Model Checking","author":"R.E. Bryant","year":"2018","unstructured":"Bryant, R.E.: Binary decision diagrams. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR20","first-page":"123","volume-title":"ACM Symposium on Theory of Computing (STOC)","author":"S.R. Buss","year":"1987","unstructured":"Buss, S.R.: The Boolean formula value problem is in ALOGTIME. In: ACM Symposium on Theory of Computing (STOC), pp.\u00a0123\u2013131. ACM, New York (1987)"},{"key":"20_CR21","volume-title":"Handbook of Model Checking","author":"S. Chaki","year":"2018","unstructured":"Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR22","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"20_CR23","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"20_CR24","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"20_CR25","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, New York (1986). Nuprl home page: http:\/\/www.nuprl.org"},{"issue":"1","key":"20_CR26","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"key":"20_CR27","first-page":"439","volume-title":"International Conference on Software Engineering","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp.\u00a0439\u2013448 (2000)"},{"key":"20_CR28","first-page":"238","volume-title":"ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages, pp.\u00a0238\u2013252. ACM, New York (1977)"},{"issue":"3","key":"20_CR29","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"key":"20_CR30","volume-title":"Handbook of Model Checking","author":"D. Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR31","volume-title":"Handbook of Model Checking","author":"L. Doyen","year":"2018","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR32","first-page":"997","volume-title":"Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pp.\u00a0997\u20131072. MIT Press\/Elsevier, Cambridge\/Amsterdam (1990)"},{"issue":"3","key":"20_CR33","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"20_CR34","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol.\u00a0XIX, pp.\u00a019\u201332. AMS, Providence (1967)"},{"key":"20_CR35","unstructured":"Ganzinger, H., Rue\u00df, H., Shankar, N.: Modularity and refinement in inference systems. Tech. Rep. CSL-SRI-04-02, SRI International, Computer Science Laboratory (2004). Revised, August 2004"},{"key":"20_CR36","volume-title":"Handbook of Model Checking","author":"D. Giannakopoulou","year":"2018","unstructured":"Giannakopoulou, D., Namjoshi, K.S., P\u0103s\u0103reanu, C.S.: Compositional reasoning. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR37","volume-title":"Handbook of Model Checking","author":"P. Godefroid","year":"2018","unstructured":"Godefroid, P., Sen, K.: Combining model checking and testing. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","key":"20_CR38","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993). HOL home page: http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/"},{"key":"20_CR39","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4","volume-title":"First Order Dynamic Logic","author":"D. Harel","year":"1979","unstructured":"Harel, D.: First Order Dynamic Logic. LNCS, vol.\u00a068. Springer, Heidelberg (1979)"},{"issue":"1","key":"20_CR40","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"issue":"10","key":"20_CR41","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"20_CR42","volume-title":"Handbook of Model Checking","author":"G. Holzmann","year":"2018","unstructured":"Holzmann, G.: Explicit-state model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0539-5","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1999","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)"},{"key":"20_CR44","volume-title":"Handbook of Model Checking","author":"R. Jhala","year":"2018","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"issue":"2","key":"20_CR45","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MAHC.2003.1203057","volume":"25","author":"C.B. Jones","year":"2003","unstructured":"Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann. Hist. Comput. 25(2), 26\u201349 (2003)","journal-title":"IEEE Ann. Hist. Comput."},{"key":"20_CR46","series-title":"Advances in Formal Methods","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods, vol.\u00a03. Kluwer Academic, Norwell (2000)"},{"key":"20_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer-Aided Verification, CAV","author":"S. Lahiri","year":"2006","unstructured":"Lahiri, S., Nieuwenhuis, R., Oliveras, A.: SMT techniques for predicate abstraction. In: Computer-Aided Verification, CAV. LNCS, vol.\u00a04144, pp.\u00a0424\u2013437. Springer, Heidelberg (2006)"},{"key":"20_CR48","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/oso\/9780198537465.003.0004","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2: Deduction Methodologies","author":"D. Leivant","year":"1994","unstructured":"Leivant, D.: Higher order logic. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2: Deduction Methodologies, pp.\u00a0229\u2013321. Clarendon, Oxford (1994)"},{"key":"20_CR49","first-page":"607","volume-title":"ACM Symposium on Principles of Programming Languages","author":"Y. Li","year":"2014","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: Jagannathan, S., Sewell, P. (eds.) ACM Symposium on Principles of Programming Languages, pp.\u00a0607\u2013618. ACM, New York (2014)"},{"key":"20_CR50","volume-title":"Handbook of Model Checking","author":"R. Majumdar","year":"2018","unstructured":"Majumdar, R., Raskin, J.F.: Symbolic model checking in non-Boolean domains. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR51","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems, Volume 1: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Volume 1: Specification. Springer, Heidelberg (1992)"},{"key":"20_CR52","volume-title":"Handbook of Model Checking","author":"J. Marques-Silva","year":"2018","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR53","volume-title":"Computer Programming and Formal Systems","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hershberg, D. (eds.) Computer Programming and Formal Systems. North-Holland, Amsterdam (1963)"},{"key":"20_CR54","volume-title":"Handbook of Model Checking","author":"K.L. McMillan","year":"2018","unstructured":"McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR55","unstructured":"Mints, G.E.: A short introduction to modal logic. No. 30 in CSLI lecture notes. Center for the Study of Language and Information (1992)"},{"issue":"2","key":"20_CR56","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"F.L. Morris","year":"1984","unstructured":"Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. IEEE Ann. Hist. Comput. 6(2), 139\u2013143 (1984)","journal-title":"IEEE Ann. Hist. Comput."},{"key":"20_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer-Aided Verification, CAV","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Computer-Aided Verification, CAV. LNCS, pp.\u00a0496\u2013500. Springer, Heidelberg (2004). SAL home page: http:\/\/sal.csl.sri.com\/"},{"issue":"2","key":"20_CR58","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. Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"Trans. Program. Lang. Syst."},{"key":"20_CR59","volume-title":"John von Neumann, Collected Works","author":"J. Neumann von","year":"1961","unstructured":"von Neumann, J.: John von Neumann, Collected Works, vol.\u00a0V. Pergamon, Oxford (1961)"},{"key":"20_CR60","volume-title":"Planning and Coding of Problems for an Electronic Computing Instrument","author":"J.v. Neumann","year":"1948","unstructured":"Neumann, J.v., Goldstine, H.H.: Planning and Coding of Problems for an Electronic Computing Instrument. Institute for Advanced Study, Princeton (1948)"},{"key":"20_CR61","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"2001","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2001)"},{"key":"20_CR62","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). Isabelle home page: http:\/\/isabelle.in.tum.de\/"},{"issue":"2","key":"20_CR63","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. Trans. Softw. Eng. 21(2), 107\u2013125 (1995). PVS home page: http:\/\/pvs.csl.sri.com","journal-title":"Trans. Softw. Eng."},{"issue":"2","key":"20_CR64","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. Park","year":"1976","unstructured":"Park, D.: Finiteness is mu-ineffable. Theor. Comput. Sci. 3(2), 173\u2013181 (1976)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"20_CR65","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"20_CR66","series-title":"LNCS","first-page":"58","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L. Pike","year":"2006","unstructured":"Pike, L., Brown, G.M.: Easy parameterized verification of biphase mark and 8N1 decoders. In: Hermanns, H., Palsberg, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03920, pp.\u00a058\u201372. Springer, Heidelberg (2006)"},{"key":"20_CR67","volume-title":"Handbook of Model Checking","author":"N. Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"20_CR68","first-page":"109","volume-title":"Annual Symposium on Foundations of Computer Science","author":"V.R. Pratt","year":"1976","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Annual Symposium on Foundations of Computer Science, pp.\u00a0109\u2013121 (1976)"},{"key":"20_CR69","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the 5th International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming. LNCS, vol.\u00a0137, pp.\u00a0337\u2013351. Springer, Heidelberg (1982)"},{"key":"20_CR70","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, CAV","author":"S. Rajan","year":"1995","unstructured":"Rajan, S., Shankar, N., Srivas, M.: An integration of model-checking with automated proof checking. In: Wolper, P. (ed.) Computer-Aided Verification, CAV. LNCS, vol.\u00a0939, pp.\u00a084\u201397. Springer, Heidelberg (1995)"},{"key":"20_CR71","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a02937, pp.\u00a0252\u2013266. Springer, Heidelberg (2004)"},{"key":"20_CR72","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Annual IEEE Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Annual IEEE Symposium on Logic in Computer Science, pp.\u00a055\u201374 (2002)"},{"key":"20_CR73","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1145\/1375581.1375602","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P.M. Rondon","year":"2008","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0159\u2013169. ACM, New York (2008). doi:10.1145\/1375581.1375602"},{"key":"20_CR74","unstructured":"Rushby, J.M., von Henke, F., Owre, S.: An introduction to formal specification and verification using EHDM. Tech. Rep. SRI-CSL-91-2, Computer Science Laboratory, SRI International (1991)"},{"key":"20_CR75","series-title":"LNCS","first-page":"72","volume-title":"Computer-Aided Verification, CAV","author":"H. Sa\u00efdi","year":"1997","unstructured":"Sa\u00efdi, H., Graf, S.: Construction of abstract state graphs with PVS. In: Computer-Aided Verification, CAV. LNCS, pp.\u00a072\u201383. Springer, Heidelberg (1997)"},{"key":"20_CR76","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer-Aided Verification, CAV","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Computer-Aided Verification, CAV. LNCS, pp.\u00a0443\u2013454. Springer, Heidelberg (1999)"},{"key":"20_CR77","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a03385, pp.\u00a025\u201341. Springer, Heidelberg (2005)"},{"issue":"4","key":"20_CR78","doi-asserted-by":"publisher","first-page":"20:1","DOI":"10.1145\/1592434.1592437","volume":"41","author":"N. Shankar","year":"2009","unstructured":"Shankar, N.: Automated deduction for verification. ACM Comput. Surv. 41(4), 20:1\u201320:56 (2009). doi:10.1145\/1592434.1592437","journal-title":"ACM Comput. Surv."},{"key":"20_CR79","first-page":"129","volume-title":"Collected Works of A.M. Turing: Mechanical Intelligence","author":"A.M. Turing","year":"1992","unstructured":"Turing, A.M.: Checking a large routine. In: Ince, D.C. (ed.) Collected Works of A.M. Turing: Mechanical Intelligence, pp.\u00a0129\u2013131. North-Holland, Amsterdam (1992). Originally presented at EDSAC Inaugural Conference on High Speed Automatic Calculating Machines, 24 June, 1949"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,6]],"date-time":"2024-07-06T21:24:28Z","timestamp":1720301068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_20","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}