{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:17:08Z","timestamp":1725664628718},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540630104"},{"type":"electronic","value":"9783540690580"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63010-4_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:58:46Z","timestamp":1330279126000},"page":"64-78","source":"Crossref","is-referenced-by-count":6,"title":["The verus language: Representing time efficiently with BDDs"],"prefix":"10.1007","author":[{"given":"S\u00e9rgio","family":"Campos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"T. Bolognesi and F. Lucidi. A timed full LOTOS with time\/action tree semantics. In: Theories and Experiences for RealTime System Development. World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0008"},{"key":"5_CR2","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In 5 th Symposium on Logics in Computer Science, 1990."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"G. Berry and G. Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. In: Science of Computer Programming, vol. 19, 1992.","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"S.V. Campos. A quantitative approach to the formal verification of real-time systems. Ph.D. thesis, SCS, Carnegie Mellon University, 1996.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"S. V. Campos and O. Grumberg. Selective quantitative analysis and interval model checking: verifying different facets of a system. In: Computer Aided Verification, 1996.","DOI":"10.1007\/3-540-61474-5_74"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"S.V. Campos, E. M. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Real-Time Systems Symposium, 1994.","DOI":"10.1109\/REAL.1994.342709"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"S. V. Campos, E. M. Clarke, W. Marrero and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. In: ICCD, 1995.","DOI":"10.1109\/ICCD.1995.528793"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"S.V. Campos, E. M. Clarke, W. Marrero and M. Minea. Verus: a tool for quantitative analysis of finite-state real-time systems. In: Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.","DOI":"10.1145\/216636.216661"},{"key":"5_CR9","volume-title":"LNCS 131","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981. LNCS 131, Springer-Verlag, 1981."},{"key":"5_CR10","unstructured":"E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In 11 th CHDL, 1993."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"P. Clements, C. Heitmeyer, G. Labaw, and A. Rose. MT: a toolset for specifying and analyzing real-time systems. In IEEE Real-Time Systems Symposium, 1993.","DOI":"10.21236\/ADA465119"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"J. Davies and S. Schneider. Real-time CSP. In: Theories and Experiences for RealTime System Development. World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0002"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"A. N. Fredette and R. Cleaveland. RTSL: a language for real-time schedulability analysis. In IEEE Real-Time Systems Symposium, 1993.","DOI":"10.1109\/REAL.1993.393489"},{"key":"5_CR14","unstructured":"F. Jahanian and D. Stuart A method for verifying properties of modechart specifications. In: IEEE Real-Time Systems Symposium, 1988."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"C. Locke, D. Vogel, and T. Mesler. Building a predictable avionics platform in Ada: a case study. In IEEE Real-Time Systems Symposium, 1991.","DOI":"10.1109\/REAL.1991.160372"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic model checking \u2014 an approach to the state explosion problem. Ph.D. thesis, SCS, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"J. Ostroff. Visual tools for verifying real-time systems. In: Theories and Experiences for RealTime System Development. World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0003"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"J. Quemada, C. Miguel, D. Frutos and L. Llana. A timed LOTOS extension. In: Theories and Experiences for Realtime System Development. World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0009"}],"container-title":["Lecture Notes in Computer Science","Transformation-Based Reactive Systems Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63010-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,24]],"date-time":"2019-06-24T10:37:40Z","timestamp":1561372660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63010-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540630104","9783540690580"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-63010-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}