{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:06:02Z","timestamp":1725483962276},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439301"},{"type":"electronic","value":"9783540456193"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45619-8_8","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:57:41Z","timestamp":1179572261000},"page":"100-114","source":"Crossref","is-referenced-by-count":8,"title":["Efficient Real-Time Model Checking Using Tabled Logic Programming and Constraints"],"prefix":"10.1007","author":[{"given":"Giridhar","family":"Pemmasani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"S. Basu, S. A. Smolka, and O. R. Ward. Model checking the Java Meta-Locking algorithm. In Proceedings of 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000), Edinburgh, Scotland, April 2000.","DOI":"10.1109\/ECBS.2000.839894"},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61474-5_73","volume-title":"Proceedings of the 8th International Conference on Computer-Aided Verification","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, W. O. D. Griffioen, K. J. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an audio protocol with bus collision using Uppaal. In Proceedings of the 8th International Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 244\u2013256, New Brunswick, New Jersey, USA, 1996. Springer-Verlag."},{"key":"8_CR4","unstructured":"T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1999."},{"key":"8_CR5","unstructured":"G. Delzanno and S. Etalle. Transforming a proof system into prolog for verifying security protocols. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001."},{"key":"8_CR6","unstructured":"G. Delzanno, S. Mukhopadhyay, and A. Podelski. Constraint-based model checking for timed systems with accurate widenings. Technical Report, Max-Planck-Institut f\u00fcr Informatik, 1999."},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99)","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 99), LNCS, volume 1579, pages 223\u2013239, Amsterdam, March 1999."},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u201989","author":"D. L. Dill","year":"1989","unstructured":"D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proceedings of CAV\u201989. LNCS 407, 1989."},{"key":"8_CR9","unstructured":"X. Du, C. R. Ramakrishnan, and S. A. Smolka. Tabled resolution + constraints: a recipe for model checking real-time systems. In Proceedings of the IEEE Real-Time Systems Symposium. IEEE Computer Society Press, 2000."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state processes using program transofmration. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001.","DOI":"10.1007\/3-540-45607-4_7"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"G. Gupta and E. Pontelli. A Constraint Based Approach for Specification and Verification of Real-Time Systems. In Proceedings of the IEEE Real-Time Systems Symposium, December 1997.","DOI":"10.1109\/REAL.1997.641285"},{"issue":"2","key":"8_CR12","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157\u2013185, August 1997.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"8_CR13","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P. H. Ho, and H. Wong-Toi. \u201cHyTech: A model checker for hybrid systems\u201d. International Journal on Software Tools for Technology Transfer, 1(2):110\u2013122, October 1997.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"5","key":"8_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Proc. of Fundamentals of Computation Theory","author":"K. G. Larsen","year":"1995","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Model checking for real-time systems. In Proc. of Fundamentals of Computation Theory, number 965 in LNCS, pages 62\u201388, August 1995."},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1:134\u2013152, 1997.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"M. Leuschel and S. Gruner. Abstract partial deduction using regular types and its application to model checking. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001.","DOI":"10.1007\/3-540-45607-4_6"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"U. Nilsson and J. Lubcke. Constraint logic programming for local and symbolic model-checking. In In Proc. of the Int\u2019l Conf. on Computational Logic (CL2000), volume 1861. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44957-4_26"},{"key":"8_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-63166-6_16","volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification (CAV\u2019 97)","author":"Y. S. Ramakrishna","year":"1997","unstructured":"Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV\u2019 97), volume 1254 of LNCS, pages 143\u2013154, Haifa, Israel, July 1997. Springer-Verlag."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V. N. Venkatakrishnan. XMC: A logic-programming-based verification toolset. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV\u2019 00), pages 576\u2013580. Springer-Verlag, 2000.","DOI":"10.1007\/10722167_48"},{"key":"8_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 13th International Conference on Computer-Aided Verification (CAV\u2019 01)","author":"A. Roychoudhury","year":"2001","unstructured":"A. Roychoudhury and I. V. Ramakrishnan. Automated inductive verification of parameterized protocols. In Proceedings of the 13th International Conference on Computer-Aided Verification (CAV\u2019 01), volume 2102 of LNCS. Springer-Verlag, 2001."},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 7th International Conference on Computer-Aided Verification","author":"O. Sokolsky","year":"1995","unstructured":"O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Verification, volume 939 of LNCS. American Mathematical Society, 1995."},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Constraint Programming (CP\u201996)","author":"L. Urbina","year":"1996","unstructured":"L. Urbina. Analysis of hybrid systems in CLP(R). In Constraint Programming (CP\u201996), volume LNCS 1102. Springer-Verlag, 1996."},{"key":"8_CR24","unstructured":"XSB. The XSB logic programming system. Available at www.cs.sunysb.edu\/~sbprolog ."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"S. Yovine. Model checking timed automata. In European Educational Forum: School on Embedded Systems, pages 114\u2013152, 1996.","DOI":"10.1007\/3-540-65193-4_20"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45619-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:20:49Z","timestamp":1556414449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45619-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439301","9783540456193"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45619-8_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}