{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:28:49Z","timestamp":1778300929694,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600459","type":"print"},{"value":"9783540494133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_66","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:37:23Z","timestamp":1330277843000},"page":"409-422","source":"Crossref","is-referenced-by-count":27,"title":["Verification of real-time systems by successive over and under approximation"],"prefix":"10.1007","author":[{"given":"David L.","family":"Dill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Howard","family":"Wong-Toi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"32_CR1","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems (extended abstract). In Proc. of 3rd CONCUR, LNCS 630, Springer-Verlag, 1992."},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and D.L. Dill. Automata for modeling real-time systems. In Proc. of 17th ICALP, LNCS 443, Springer-Verlag, 1990.","DOI":"10.1007\/BFb0032042"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, A. Itai, R. Kurshan, and M. Yannakakis. Timing verification by successive approximation. In Proc. of 4th CAV, LNCS 663, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56496-9_12"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. A verification strategy for timing constrained systems. In Proc. of 4th CAV, LNCS 663, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56496-9_13"},{"key":"32_CR5","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. Iterative algorithms for formal verification of embedded real-time systems. In Proc. of ICCAD, 1994."},{"issue":"8","key":"32_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"32_CR7","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. of 5th LICS, 1990."},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of 4th POPL, 1977.","DOI":"10.1145\/512950.512973"},{"issue":"2\u20133","key":"32_CR9","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2\u20133):103\u2013179, July 1992.","journal-title":"Journal of Logic Programming"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, G. D\u00f6hmen, R. Herrmann, P. Kelb, and H. Pargmann. Model checking using adaptive state and data abstraction. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_75"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, International Workshop. LNCS 407, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"32_CR14","unstructured":"T.A. Henzinger and P.-H. Ho. Model checking strategies for hybrid systems. In Proc. of the International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, 1994."},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proc. of 7th LICS, 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"32_CR16","unstructured":"I. Kang and I. Lee. An efficient generation of the timed reachability graph for the analysis of real-time systems. Technical Report MS-CIS-94-36, University of Pennsylvania, 1994."},{"key":"32_CR17","unstructured":"K.L. McMillan and P.H. Ho. Automatic timing analysis of timed circuits. Unpublished manuscript. 1994."},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"V.G. Naik and A.P. Sistla. Modeling and verification of a real life protocol using symbolic model checking. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_54"},{"issue":"9","key":"32_CR19","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1109\/32.159837","volume":"SE-18","author":"X. Nicollin","year":"1992","unstructured":"X. Nicollin, J. Sifakis, and S. Yovine. Compiling real-time specifications into extended automata. IEEE Transactions on Software Engineering, SE-18(9):794\u2013804, 1992.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"J.S. Ostroff. Verification of safety critical systems using TTM\/RTTL. In Proc. of 1991 REX Workshop in \u201cReal-Time: Theory in Practice\u201d, LNCS 600, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0032008"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"T.G. Rokicki and C.J. Myers. Automatic verification of timed circuits. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_76"},{"key":"32_CR22","unstructured":"H.B. Weinberg and L.D. Zuck. Timed ethernet: Real-time formal specification of ethernet. In Proc. of 3rd CONCUR, LNCS 630, Springer-Verlag, 1992."},{"key":"32_CR23","volume-title":"PhD thesis","author":"H. Wong-Toi","year":"1994","unstructured":"H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Dept. of Computer Science, Stanford University, CA, December 1994."},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi and D.L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time System Development, chapter 7. World Scientific, 1995.","DOI":"10.1142\/9789812831583_0007"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_18"},{"issue":"12","key":"32_CR26","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1002\/scj.4690221204","volume":"22","author":"T. Yoneda","year":"1991","unstructured":"T. Yoneda, Y. Tohma, and Y. Kondo. Acceleration of timing verification method based on time petri nets. Systems and Computers in Japan, 22(12):37\u201352, 1991.","journal-title":"Systems and Computers in Japan"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_66.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:58Z","timestamp":1605648538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_66"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_66","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}