{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:40:01Z","timestamp":1737592801065,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_12","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"199-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Do You Trust Your Model Checker?"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Reif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Ruf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Vollmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and Their Applications. In IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pages 188\u2013191, Santa Clara, California, November 1993. ACM\/IEEE, IEEE Computer Society Press.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"12_CR2","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 IEEE Symposium on Logic in Computer Science (LICS), pages 1\u201333, Washington, D.C., June 1990. IEEE Computer Society Press."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"E. Clarke, K.L. McMillian, X. Zhao, M. Fujita, and J.C.-Y. Yang. Spectral Transforms for large Boolean Functions with Application to Technologie Mapping. In ACM\/IEEE Design Automation Conference (DAC), pages 54\u201360, Dallas, TX, June 1993.","DOI":"10.1145\/157485.164569"},{"key":"12_CR4","unstructured":"D. Long. Long-package sun release 4.1 overview of c-library functions, 1993."},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Correctness of Generic Modules","author":"W. Reif","year":"1992","unstructured":"W. Reif. Correctness of Generic Modules. In Nerode and Taitslin, editors, Symposium on Logical Foundations of Computer Science, LNCS 620, Berlin, 1992. Logic at Tver, Tver, Russia, Springer."},{"key":"12_CR6","unstructured":"W. Reif, G. Schellhorn, and K. Stenzel. Interactive Correctness Proofs for Software Modules Using KIV. In COMPASS\u201995 Tenth Annual Conference on Computer Assurance, Gaithersburg (MD), USA, 1995. IEEE pre"},{"key":"12_CR7","volume-title":"Automated Deduction-A Basis for Applications","author":"W. Reif","year":"1998","unstructured":"W. Reif, G. Schellhorn, K. Stenzel, and M. Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction-A Basis for Applications. Kluwer Academic Publishers, Dordrecht, 1998."},{"key":"12_CR8","unstructured":"J. Ruf. RAVEN: Real-time analyzing and veri_cation environment. Technical Report WSI 2000-3, University of T\u00fcbingen, Wilhelm-Schickard-Institute, January 2000."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Ruf and Thomas Kropf. Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In E. Cerny and D.K. Probst, editors, Conference on Correct Hardware Design and Veri_cationMethods (CHARME), pages 146\u2013166, Montreal, Canada, October 1997. IFIP WG 10.5, Chapman and Hall.","DOI":"10.1007\/978-0-387-35190-2_10"},{"key":"12_CR10","unstructured":"J\u00fcrgen Ruf and Thomas Kropf. Using MTBDDs for Composition and Model Checking of Real-Time Systems. In FMCAD 1998. Springer, November 1998."},{"key":"12_CR11","unstructured":"J\u00fcrgen Ruf and Thomas Kropf. Modeling and Checking Networks of CommunicatingReal-Time Systems. In Correct Hardware Design and VeriFication Methods (CHARME 99), pages 265\u2013279. IFIP WG 10.5, Springer, September 1999."},{"key":"12_CR12","volume-title":"Korrekte Modellpr\u00fcfung von Realzeitsystemen","author":"T. Vollmer","year":"2000","unstructured":"T. Vollmer. Korrekte Modellpr\u00fcfung von Realzeitsystemen. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Ulm, Germany, 2000. (in German)."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:00Z","timestamp":1737591780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}