{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:56:46Z","timestamp":1779087406914,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642175107","type":"print"},{"value":"9783642175114","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17511-4_3","type":"book-chapter","created":{"date-parts":[[2010,12,7]],"date-time":"2010-12-07T06:24:40Z","timestamp":1291703080000},"page":"27-45","source":"Crossref","is-referenced-by-count":5,"title":["Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation"],"prefix":"10.1007","author":[{"given":"Gourinath","family":"Banda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John P.","family":"Gallagher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. In: Proceedings of the IEEE, pp. 971\u2013984 (2000)","DOI":"10.1109\/5.871304"},{"issue":"1-2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming\u00a072(1-2), 3\u201321 (2008)","journal-title":"Science of Computer Programming"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-00515-2_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"G. Banda","year":"2009","unstructured":"Banda, G., Gallagher, J.P.: Analysis of Linear Hybrid Systems in CLP. In: Hanus, M. (ed.) LOPSTR 2008. LNCS, vol.\u00a05438, pp. 55\u201370. Springer, Heidelberg (2009)"},{"key":"3_CR4","unstructured":"Banda, G., Gallagher, J.P.: Constraint-based abstraction of a model checker for infinite state systems. In: Wolf, A., Geske, U. (eds.) Proceedings of the 23rd Workshop on (Constraint) Logic Programming, University of Potsdam (online Technical Report series) (2009)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-62718-9_12","volume-title":"Logic Program Synthesis and Transformation","author":"F. Benoy","year":"1997","unstructured":"Benoy, F., King, A.: Inferring argument size relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 204\u2013223. Springer, Heidelberg (1997)"},{"issue":"1-2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/S0304-3975(96)00228-9","volume":"178","author":"A. Browne","year":"1997","unstructured":"Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci.\u00a0178(1-2), 237\u2013255 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR8","first-page":"303","volume-title":"ILPS","author":"C. Brzoska","year":"1995","unstructured":"Brzoska, C.: Temporal logic programming in dense time. In: ILPS, pp. 303\u2013317. MIT Press, Cambridge (1995)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: POPL, pp. 342\u2013354 (1992)","DOI":"10.1145\/143165.143235"},{"key":"3_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"3_CR12","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: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR13","first-page":"269","volume-title":"POPL 1979","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979, pp. 269\u2013282. ACM Press, New York (1979)"},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng.\u00a06(1), 69\u201395 (1999)","journal-title":"Autom. Softw. Eng."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: POPL 2000, pp. 12\u201325 (2000)","DOI":"10.1145\/325694.325699"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst.\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Du, X., Ramakrishnan, C.R., Smolka, S.A.: Real-time verification techniques for untimed systems. Electr. Notes Theor. Comput. Sci.\u00a039(3) (2000)","DOI":"10.1016\/S1571-0661(05)01222-3"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"3_CR20","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1090\/dimacs\/031\/06","volume-title":"Descriptive Complexity and Finite Models","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A.: Model checking and the mu-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a031, pp. 185\u2013214. American Mathematical Society, Providence (1996)"},{"key":"3_CR21","unstructured":"Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite-state systems by specializing constraint logic programs. In: Leuschel, M., Podelski, A., Ramakrishnan, C., Ultes-Nitsche, U. (eds.) Proceedings of the Second International Workshop on Verification and Computational Logic (VCL 2001), pp. 85\u201396. Tech. Report DSSE-TR-2001-3, University of Southampton (2001)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"3_CR23","unstructured":"Ganty, P.: The Fixpoint Checking Problem: An Abstraction Refinement Perspective. PhD thesis, Universit\u00e9 Libre de Bruxelles, D\u00e9partement d\u2019Informatique (2007)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 356\u2013373. Springer, Heidelberg (2001)"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: IEEE Real-Time Systems Symposium, pp. 230\u2013239 (1997)","DOI":"10.1109\/REAL.1997.641285"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis","author":"N. Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.E., Raymound, P.: Verification of linear hybrid systems by means of convex approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol.\u00a0864, pp. 223\u2013237. Springer, Heidelberg (1994)"},{"key":"3_CR28","unstructured":"Henriksen, K.S., Banda, G., Gallagher, J.P.: Experiments with a convex polyhedral analysis tool for logic programs. In: Workshop on Logic Programming Environments, Porto (2007)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013463. Springer, Heidelberg (1997)"},{"key":"3_CR30","volume-title":"Logic in Computer Science: Modelling and reasoning about systems","author":"M.R.A. Huth","year":"2000","unstructured":"Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2000)"},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1109\/REAL.2004.5","volume-title":"The 25th IEEE International Real-Time Systems Symposium","author":"J. Jaffar","year":"2004","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: A CLP proof method for timed automata. In: Anderson, J., Sztipanovits, J. (eds.) The 25th IEEE International Real-Time Systems Symposium, pp. 175\u2013186. IEEE Computer Society, Los Alamitos (2004)"},{"key":"3_CR32","unstructured":"Kelb, P.: Model checking and abstraction: A framework preserving both truth and failure information. Technical report, Carl yon Ossietzky Univ. of Oldenburg, Oldenburg, Germany (1994)"},{"key":"3_CR33","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/LICS.1988.5119","volume-title":"Proceedings, Third Annual Symposium on Logic in Computer Science","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings, Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, UK, July 5-8, pp. 203\u2013210. IEEE Computer Society, Los Alamitos (1988)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/10720327_5","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 63\u201382. Springer, Heidelberg (2000)"},{"issue":"1","key":"3_CR35","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06(1), 11\u201344 (1995)","journal-title":"Formal Methods in System Design"},{"key":"3_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)"},{"key":"3_CR37","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/3-540-44957-4_26","volume-title":"Computational Logic - CL 2000","author":"U. Nilsson","year":"2000","unstructured":"Nilsson, U., L\u00fcbcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 384\u2013398. Springer, Heidelberg (2000)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/3-540-45619-8_8","volume-title":"Logic Programming","author":"G. Pemmasani","year":"2002","unstructured":"Pemmasani, G., Ramakrishnan, C.R., Ramakrishnan, I.V.: Efficient real-time model checking using tabled logic programming and constraints. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol.\u00a02401, pp. 100\u2013114. Springer, Heidelberg (2002)"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/3-540-45013-0_8","volume-title":"Logic Based Program Synthesis and Transformation","author":"J.C. Peralta","year":"2003","unstructured":"Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664, pp. 90\u2013108. Springer, Heidelberg (2003)"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"3_CR41","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics\u00a05, 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"}],"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-642-17511-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T14:05:51Z","timestamp":1740751551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17511-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642175107","9783642175114"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17511-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}