{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T14:40:08Z","timestamp":1740667208668,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642171710"},{"type":"electronic","value":"9783642171727"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17172-7_5","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:17:15Z","timestamp":1288703835000},"page":"81-101","source":"Crossref","is-referenced-by-count":1,"title":["The VATES-Diamond as a Verifier\u2019s Best Friend"],"prefix":"10.1007","author":[{"given":"Sabine","family":"Glesner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bj\u00f6rn","family":"Bartels","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"G\u00f6thel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moritz","family":"Kleine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"VATES project website, https:\/\/group.swt.tu-berlin.de\/vates"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"CASSIS 2004","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"5_CR3","volume-title":"10th International Conference on Qualtiy Software (QSIC 2010)","author":"B. Bartels","year":"2010","unstructured":"Bartels, B., Glesner, S.: Formal Modeling and Verification of Low-Level Software Programs. In: 10th International Conference on Qualtiy Software (QSIC 2010), IEEE Computer Society, Los Alamitos (2010)"},{"key":"5_CR4","unstructured":"Bartels, B., Glesner, S., G\u00f6thel, T.: Model Transformations to Mitigate the Semantic Gap in Embedded Systems Verification. In: International Colloquium on Graph and Model Transformation \u2013 on the occasion of the 65th birthday of Hartmut Ehrig (2010) (accepted for publication)"},{"issue":"2","key":"5_CR5","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1524\/itit.2007.49.2.118","volume":"49","author":"B. Becker","year":"2007","unstructured":"Becker, B., Damm, W., Fr\u00e4nzle, M., Olderog, E., Podelski, A., Wilhelm, R.: SFB\/TR 14 AVACS \u2013 Automatic Verification and Analysis of Complex Systems. It \u2013 Information Technology\u00a049(2), 118\u2013126 (2007)","journal-title":"It \u2013 Information Technology"},{"key":"5_CR6","series-title":"Lectures on Concurrency and Preti Nets","first-page":"87","volume-title":"Timed Automata: Semantics, Algorithms and Tools","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Lectures on Concurrency and Preti Nets, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLS 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"5_CR8","unstructured":"Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a Practical, Verified Kernel. In: HOTOS 2007 Proceedings of the 11th USENIX workshop on Hot topics in operating systems, Berkeley, CA, USA, pp. 1\u20136 (2007)"},{"key":"5_CR9","first-page":"423","volume-title":"FMOODS 1997 Proceedings of the IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ: a combination of object-Z and CSP. In: FMOODS 1997 Proceedings of the IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems, pp. 423\u2013438. Chapman & Hall, Ltd., London (1997)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-Checking CSP-OZ Specifications with FDR. In: IFM, pp. 315\u2013334 (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"5_CR11","unstructured":"Goldsmith, M., Roscoe, B., Armstrong, P.: Failures-Divergence Refinement - FDR2 User Manual (2005)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"G\u00f6thel, T., Glesner, S.: An Approach for Machine-Assisted Verification of Timed CSP Specifications. Innovations in Systems and Software Engineering - A NASA Journal 7 (2010) (to appear)","DOI":"10.1007\/s11334-010-0126-z"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"G\u00f6thel, T., Glesner, S.: Towards the Semi-Automatic Verification of Parameterized Real-Time Systems using Network Invariants. In: Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Method (2010) (accepted for publication)","DOI":"10.1109\/SEFM.2010.38"},{"key":"5_CR14","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, London (1985)"},{"key":"5_CR15","unstructured":"Hohmuth, M., Tews, H.: The VFiasco Approach for a Verified Operating System. In: Proc. 2nd ECOOP Workshop on Programming Languages and Operating Systems (2005)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Kassel, G., Smith, G.: Model Checking Object-Z Classes: Some Experiments with FDR. In: APSEC, pp. 445\u2013452 (2001)","DOI":"10.1109\/APSEC.2001.991513"},{"key":"5_CR17","unstructured":"Kleine, M., Bartels, B.: On Using CSP for the Construction of Concurrent Programs. In: International Conference on Software Engineering Theory and Practice (SETP 2010), Orlando, Florida, USA (2010)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-642-10452-7_18","volume-title":"Brazilian Symposium on Formal Methods (SBMF 2009)","author":"M. Kleine","year":"2009","unstructured":"Kleine, M., Helke, S.: Low Level Code Verification Based on CSP Models. In: Oliveira, M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 266\u2013281. Springer, Heidelberg (2009)"},{"key":"5_CR19","unstructured":"Kleine, M.: Using CSP for Software Verification. In: Mousavi, Sekerinski (eds.) Proceedings of Formal Methods 2009 Doctoral Symposium, Eindhoven University of Technology, pp. 8\u201313 (2009)"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. Inf. Comput.\u00a0117(1), 1\u201311 (1995)","journal-title":"Inf. Comput."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/978-3-540-88194-0_18","volume-title":"ICFEM 2008","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Fontaine, M.: Probing the Depths of CSP-M: A new FDR-compliant Validation Tool. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 278\u2013297. Springer, Heidelberg (2008)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45251-6_6","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"M. Leuschel","year":"2001","unstructured":"Leuschel, M., Massart, T., Currie, A.: How to make FDR Spin: LTL model checking of CSP using Refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 99. Springer, Heidelberg (2001)"},{"key":"5_CR24","unstructured":"Montenegro, S., Briess, K., Kayal, H.: Dependable Software (BOSS) for the BEESAT Pico Satellite. In: Data System. Aerospace - DASIA 2006, Berlin (2006)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"5_CR26","volume-title":"Concurrent and Real Time Systems: The CSP Approach","author":"S. Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. John Wiley & Sons, Inc., New York (1999)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-44919-1_13","volume-title":"Applications and Theory of Petri Nets 2003","author":"A.M. Sherif","year":"2003","unstructured":"Sherif, A.M., Sampaio, A., Cavalcante, S.: Specification and Validation of the SACI-1 On-Board Computer Using Timed-CSP-Z and Petri Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol.\u00a02679, pp. 161\u2013180. Springer, Heidelberg (2003)"},{"key":"5_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z specification language","author":"G. Smith","year":"2000","unstructured":"Smith, G.: The Object-Z specification language. Kluwer Academic Publishers, Norwell (2000)"}],"container-title":["Lecture Notes in Computer Science","Verification, Induction, Termination Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17172-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T13:29:06Z","timestamp":1740662946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17172-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171710","9783642171727"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17172-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}