{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:05:52Z","timestamp":1761620752985},"reference-count":51,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4549,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1016\/s0304-3975(00)00088-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T14:45:40Z","timestamp":1027608340000},"page":"27-60","source":"Crossref","is-referenced-by-count":19,"title":["Deductive verification of real-time systems using STeP"],"prefix":"10.1016","volume":"253","author":[{"given":"Nikolaj S.","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00088-8_BIB1","series-title":"Proc. REX Workshop \u201cReal-Time","first-page":"1","article-title":"An old-fashioned recipe for real time","volume":"vol. 600","author":"Abadi","year":"1992"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB3","unstructured":"R. Alur, T.A. Henzinger (Eds.), in: Proc. 8th Internat. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, July 1996."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB4","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, Modularity for timed and hybrid systems, Proc. 8th Internat. Conf. on Concurrency Theory, Lecture Notes in Computer Science, vol. 1243, Springer, Berlin, 1997, pp. 74\u201388.","DOI":"10.1007\/3-540-63141-0_6"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB5","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, E.D. Sontag (Eds.), in: Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science, vol. 1066, Springer, Berlin, 1996.","DOI":"10.1007\/BFb0020948"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB6","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BF00360339","article-title":"Specification and verification of reactive system behaviour: the railroad crossing example","volume":"10","author":"Armstrong","year":"1996","journal-title":"Real-Time Systems"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB7","series-title":"Hybrid Systems III","first-page":"232","article-title":"Uppaal-a tool suite for automatic verification of real-time systems","volume":"vol. 1066","author":"Bengtsson","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB8","series-title":"Proc. 8th Internat. Conf. on Computer Aided Verification","first-page":"323","article-title":"Powerful techniques for the automatic generation of invariants","volume":"vol. 1102","author":"Bensalem","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB9","unstructured":"N.S. Bj\u00f8orner, Integrating decision procedures for temporal verification, Ph.D. thesis, Computer Science Department, Stanford University, November 1998."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB10","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, A. Browne, E.S. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, T.E. Uribe, STeP: the stanford temporal prover, User's Manual, Tech. Rep. STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.","DOI":"10.1007\/3-540-59293-8_237"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB11","series-title":"Proc. 8th Internat. Conf. on Computer Aided Verification","first-page":"415","article-title":"STeP","volume":"vol. 1102","author":"Bj\u00f8rner","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB12","unstructured":"N.S. Bj\u00f8rner, A. Browne, Z. Manna, Automatic generation of invariants and intermediate assertions, Theoret. Comput. Sci. 173(1) (1997) 49\u201387. Preliminary version appeared in 1st Internat. Conf. on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, vol. 976, Springer, Berlin, 1995, pp. 589\u2013623."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB13","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, M.E. Stickel, T.E. Uribe, A practical integration of first-order reasoning and decision procedures, Proc. 14th Internat. Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 1249, Springer, Berlin, July 1997, pp. 101\u2013115.","DOI":"10.1007\/3-540-63104-6_13"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB14","doi-asserted-by":"crossref","unstructured":"A. Browne, Z. Manna, H.B. Sipma, Generalized temporal verification diagrams, In 15th Conf. on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 1026, Springer, Berlin, 1995, pp. 484\u2013498.","DOI":"10.1007\/3-540-60692-0_69"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB15","series-title":"Theories and Experiences for Real-Time System Development, AMAST","article-title":"Real-time symbolic model checking for discrete time models","author":"Campos","year":"1995"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB16","unstructured":"E.S. Chang, Compositional verification of reactive and real-time systems, Ph.D. thesis, Computer Science Department, Stanford University, Stanford, California, 1993, Tech. Report STAN-CS-TR-94-1522."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB17","doi-asserted-by":"crossref","unstructured":"E.S. Chang, Z. Manna, A. Pnueli, Compositional verification of real-time systems, Proc. 9th IEEE Symp. Logic in Comp. Sci., IEEE Computer Society Press, Silverspring, MD, 1994, pp. 458\u2013465.","DOI":"10.1109\/LICS.1994.316045"},{"issue":"5","key":"10.1016\/S0304-3975(00)00088-8_BIB18","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of durations","volume":"40","author":"Chaochen","year":"1992","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB19","series-title":"Proc. 10th Internat. Conf. on Computer Aided Verification","first-page":"293","article-title":"Generating finite-state abstractions of reactive systems using decision procedures","volume":"vol. 1427","author":"Col\u00f3n","year":"1998"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB20","series-title":"Hybrid Systems III","first-page":"208","article-title":"The tool KRONOS","volume":"vol. 1066","author":"Daws","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB21","doi-asserted-by":"crossref","unstructured":"C. Daws, S. Yovine, Verification of multirate timed automata with KRONOS: two examples, Tech. Rep. Spectre-95-06, VERIMAG, April 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB22","unstructured":"J.W. de Bakker, C. Huizing, W.P. de Roever, G. Rosenberg (Eds.), in: Proc. REX Workshop \u201cReal-Time: Theory in Practice\u201d, Lecture Notes in Computer Science, vol. 600, Springer, Berlin, 1992."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB23","series-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"Dill","year":"1989"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB24","first-page":"995","article-title":"Temporal and modal logic","volume":"vol. B","author":"Emerson","year":"1990"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB25","unstructured":"S.J. Garland, J.V. Guttag, A guide to LP, the Larch Prover, Tech. Rep. 82, Digital Equipment Corportation, SRC, December 1991."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB26","series-title":"Proc. 21st Internat. Colloq. Aut. Lang. Prog.","article-title":"Liveness in timed and untimed systems","volume":"vol. 820","author":"Gawlick","year":"1994"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB27","series-title":"Introduction to HOL","author":"Gordon","year":"1993"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB28","unstructured":"C. Heitmeyer, R.D. Jeffords, B. Labaw, A benchmark for comparing different approaches for specifying and verifying real-time systems, Proc. 10th Internat. Workshop on Real-Time Operating Systems and Software, 1993."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB29","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, N. Lynch, The generalized railroad crossing: a case study in formal verification of real-time systems, Proc. IEEE Real-Time Systems Symp., IEEE Press, New York, December 1994, pp. 120\u2013131.","DOI":"10.1109\/REAL.1994.342724"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB30","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, P. Ho, HYTECH: the Cornell hybrid technology tool, in: Hybrid Systems II, Lecture Notes in Computer Science, vol. 999, Springer, Berlin, 1995, pp. 265\u2013293.","DOI":"10.1007\/3-540-60472-3_14"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB31","series-title":"Proc. 3rd Internat. Symp. on Formal Techniques in Real Time and fault Tolerant Systems","first-page":"351","article-title":"Verification methods for the divergent runs of clock systems","volume":"vol. 863","author":"Henzinger","year":"1994"},{"issue":"2","key":"10.1016\/S0304-3975(00)00088-8_BIB32","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1006\/inco.1994.1060","article-title":"Temporal proof methodologies for timed transition systems","volume":"112","author":"Henzinger","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB33","series-title":"Hybrid Systems III","first-page":"13","article-title":"Verifying clocked transition systems","volume":"vol. 1066","author":"Kesten","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB34","unstructured":"Y. Kesten, Z. Manna, A. Pnueli, Verification of clocked and hybrid systems, in: G. Rozenberg, F.W. Vaandrager (Eds.), Lectures on Embedded Systems, Lecture Notes in Computer Science, vol. 1494, Tutorial, Springer, Heidelberg, 1998, pp. 4\u201373."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB35","unstructured":"L. Lamport, Proving possibility properties, Tech. Rep. 137, Digital Equipment Corporation, Systems Research Center, July 1995."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB36","series-title":"Proc. REX Workshop \u201cReal-Time: Theory in Practice\u201d","first-page":"397","article-title":"Forward and backward simulations for timing-based systems","volume":"vol. 600","author":"Lynch","year":"1992"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB37","series-title":"Proc. REX Workshop \u201cReal-Time: Theory in Practice\u201d","first-page":"447","article-title":"From timed to hybrid systems","volume":"vol. 600","author":"Maler","year":"1992"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB38","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1991"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB39","series-title":"Proc. Internat. Symp. on Theoretical Aspects of Computer Software","first-page":"726","article-title":"Temporal verification diagrams","volume":"vol. 789","author":"Manna","year":"1994"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB40","series-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna","year":"1995"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB41","unstructured":"Z. Manna, A. Pnueli, Clocked transition systems, Tech. Rep. STAN-CS-TR-96-1566, Computer Science Department, Stanford University, April 1996."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB42","series-title":"Temporal Logic of Real-Time Systems","author":"Ostroff","year":"1990"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB43","doi-asserted-by":"crossref","DOI":"10.1109\/87.572129","article-title":"A visual toolset for the design of real-time discrete event systems","author":"Ostroff","year":"1997","journal-title":"IEEE Trans. Control Systems Technol."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB44","series-title":"Proc. 8th Internat. Conf. on Computer Aided Verification","first-page":"411","article-title":"PVS","volume":"vol. 1102","author":"Owre","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB45","doi-asserted-by":"crossref","unstructured":"D.A. Peled, V. Pratt, G.J. Holzmann (Eds.), Workshop on Partial Order Methods in Verification (Princeton: 1996), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, July 1997.","DOI":"10.1090\/dimacs\/029"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB46","series-title":"Proc. 5th Internat. Conf. on Computer Aided Verification","first-page":"280","article-title":"Verification of real-time systems using PVS","volume":"vol. 697","author":"Shankar","year":"1993"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB47","unstructured":"H.B. Sipma, Diagram-based verification of discrete, real-time and hybrid systems, Ph.D. thesis, Computer Science Department, Stanford University, December 1998."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB48","unstructured":"J.U. Skakkeb\u00e6k, A verification assistant for a real-time logic, Ph.D. thesis, Technical University of Denmark, 1994."},{"key":"10.1016\/S0304-3975(00)00088-8_BIB49","doi-asserted-by":"crossref","unstructured":"J.X. Su, D.L. Dill, C.W. Barrett, Automatic generation of invariants for processor verification, 1st Internat. Conf. on Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol. 1166, Springer, Berlin, November 1996, pp. 377\u2013388.","DOI":"10.1007\/BFb0031822"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB50","first-page":"564","article-title":"The generalized railroad crossing: Its symbolic analysis in CLP(R)","volume":"vol. 1118","author":"Urbina","year":"1996"},{"key":"10.1016\/S0304-3975(00)00088-8_BIB51","unstructured":"T.E. Uribe, Abstraction-based deductive-algorithmic verification of reactive systems, Ph.D. thesis, Computer Science Department, Stanford University, December 1998."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000888?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000888?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:55:48Z","timestamp":1556412948000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500000888"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["S0304397500000888"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00088-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}