{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:35:52Z","timestamp":1725550552415},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304920"},{"type":"electronic","value":"9783540322405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11589976_2","type":"book-chapter","created":{"date-parts":[[2005,10,26]],"date-time":"2005-10-26T13:38:16Z","timestamp":1130333896000},"page":"5-19","source":"Crossref","is-referenced-by-count":2,"title":["Generating Path Conditions for Timed Systems"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]},{"given":"Hongyang","family":"Qu","sequence":"additional","affiliation":[]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Budhiraja, N., Marzullo, K., Schneider, F.B.: Derivation of sequential, real-time process-control programs. Foundations of Real-Time Computing: Formal Specifications and Methods, 39\u201354 (1991)","DOI":"10.1007\/978-1-4615-4016-8_2"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"issue":"6","key":"2_CR5","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/367766.368168","volume":"5","author":"R.W. Floyd","year":"1962","unstructured":"Floyd, R.W.: Algorithm 97: Shortest Path. Communications of the ACM\u00a05(6), 345 (1962)","journal-title":"Communications of the ACM"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","first-page":"548","volume-title":"Verification: Theory and Practice","author":"E. Gunter","year":"2004","unstructured":"Gunter, E., Peled, D.: Unit Checking: Symbolic Model Checking for a Unit of Code. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 548\u2013567. Springer, Heidelberg (2004)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1006\/inco.1994.1060","volume":"112","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal proof methodologies for timed transition systems. Information and Computation\u00a0112, 273\u2013337 (1994)","journal-title":"Information and Computation"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111, 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/0020-0190(92)90116-D","volume":"43","author":"D.J. Scholefield","year":"1992","unstructured":"Scholefield, D.J., Zedan, H.S.M.: Weakest Precondition Semantics for Time and Concurrency. Information Processing Letters\u00a043, 301\u2013308 (1992)","journal-title":"Information Processing Letters"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/321105.321107","volume":"9","author":"S. Warshall","year":"1962","unstructured":"Warshall, S.: A theorem on boolean matrices. Journal of the ACM\u00a09(1), 11\u201312 (1962)","journal-title":"Journal of the ACM"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-65193-4_20","volume-title":"Lectures on Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol.\u00a01494, pp. 114\u2013152. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11589976_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T14:05:37Z","timestamp":1586527537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11589976_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304920","9783540322405"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11589976_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}