{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300584},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614746"},{"type":"electronic","value":"9783540685999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_92","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:41:44Z","timestamp":1330274504000},"page":"415-418","source":"Crossref","is-referenced-by-count":45,"title":["STeP: Deductive-algorithmic verification of reactive and real-time systems"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eddie","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Col\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arjun","family":"Kapur","sequence":"additional","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":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"40_CR1","unstructured":"Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., Kapur, A., Manna, Z., Sipma, H., and Uribe, T. STeP: The Stanford Temporal Prover, User's Manual. Tech. Rep. STAN-CS-TR-95-1562, Computer Science Department, Stanford University, Nov. 1995."},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Browne, A., and Manna, Z. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming (Sept. 1995), vol. 976 of LNCS, Springer-Verlag, pp. 589\u2013623.","DOI":"10.1007\/3-540-60299-2_37"},{"key":"40_CR3","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume":"1026","author":"A. Browne","year":"1995","unstructured":"Browne, A., Manna, Z., and Sipma, H. Generalized verification diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science (Dec. 1995), vol. 1026 of LNCS, pp. 484\u2013498.","journal-title":"15th Conference on the Foundations of Software Technology and Theoretical Computer Science"},{"key":"40_CR4","unstructured":"Browne, A., Manna, Z., and Sipma, H. Modular verification diagrams. Tech. rep., Computer Science Department, Stanford University, 1996."},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., and Lynch, N. The generalized railroad crossing: A case study in formal verification of real-time systems. In Proc. ICCC Real-Time Systems Symposium (1994), IEEE Press, pp. 120\u2013131.","DOI":"10.1109\/REAL.1994.342724"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"Manna, Z., Anuchitanukul, A., Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., de Alfaro, L., Devarajan, H., Sipma, H., and Uribe, T. STeP: The Stanford temporal prover. Tech. Rep. STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.","DOI":"10.21236\/ADA324036"},{"key":"40_CR7","doi-asserted-by":"crossref","unstructured":"Manna, Z., and Pnueli, A. Temporal verification diagrams. In Proc. Int. Symp. on Theoretical Aspects of Computer Software (1994), vol. 789 of LNCS, Springer-Verlag, pp. 726\u2013765.","DOI":"10.1007\/3-540-57887-0_123"},{"key":"40_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., and Pnueli, A.Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"40_CR9","unstructured":"Manna, Z., and Pnueli, A. Clocked transition systems. Tech. Rep. STAN-CS-TR-96-1566, Department of Computer Science, Stanford University, Apr. 1996."},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"Sipma, H., Uribe, T., and Manna, Z. Deductive model checking. In Proc. 8th Intl. Conference on Computer Aided Verification (July 1996), Springer-Verlag.","DOI":"10.1007\/3-540-61474-5_70"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_92.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:06:44Z","timestamp":1605629204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_92"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_92","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}