{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:29:39Z","timestamp":1743006579390,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032394"},{"type":"electronic","value":"9783642032400"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03240-0_10","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T10:27:38Z","timestamp":1248690458000},"page":"85-102","source":"Crossref","is-referenced-by-count":2,"title":["Reentrant Readers-Writers: A Case Study Combining Model Checking with Theorem Proving"],"prefix":"10.1007","author":[{"given":"Bernard","family":"van Gastel","sequence":"first","affiliation":[]},{"given":"Leonard","family":"Lensink","sequence":"additional","affiliation":[]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71209-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Anand","year":"2007","unstructured":"Anand, S., Pasareanu, C.S., Visser, W.: Jpf-se: A symbolic execution extension to java pathfinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 134\u2013138. Springer, Heidelberg (2007)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-540-27813-9_42","volume-title":"Computer Aided Verification","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 484\u2013487. Springer, Heidelberg (2004)"},{"key":"10_CR3","unstructured":"Archer, M., Heitmeyer, C., Sims, S.: TAME: A PVS interface to simplify proofs for automata models. In: User Interfaces for Theorem Provers, Eindhoven, The Netherlands (1998)"},{"issue":"5","key":"10_CR4","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/1095430.1081767","volume":"30","author":"M.A. Barbosa","year":"2005","unstructured":"Barbosa, M.A.: A refinement calculus for software components and architectures. SIGSOFT Softw. Eng. Notes\u00a030(5), 377\u2013380 (2005)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10_CR5","series-title":"Texts in Theoretical Computer Science","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: POPL, pp. 117\u2013126 (1983)","DOI":"10.1145\/567067.567080"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: Proceedings of the 2000 International Conference on Software Engineering, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"10","key":"10_CR8","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1145\/362759.362813","volume":"14","author":"P.J. Courtois","year":"1971","unstructured":"Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with \u201creaders\u201d and \u201cwriters\u201d. Commun. ACM\u00a014(10), 667\u2013668 (1971)","journal-title":"Commun. ACM"},{"key":"10_CR9","unstructured":"de Groot, A.: Practical Automaton Proofs in PVS. PhD thesis, Radboud University Nijmegen (2008)"},{"key":"10_CR10","volume-title":"Java Concurrency in Practice","author":"B. Goetz","year":"2006","unstructured":"Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison Wesley Professional, Reading (2006)"},{"key":"10_CR11","unstructured":"Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: The formal specification language mCRL2. In: Proc. Methods for Modelling Software Systems, number 06351 in Dagstuhl Seminar Proceedings (2007)"},{"key":"10_CR12","first-page":"304","volume-title":"ICSE 2004: Proceedings of the 26th International Conference on Software Engineering","author":"V. Ha","year":"2004","unstructured":"Ha, V., Rangarajan, M., Cofer, D., Rues, H., Dutertre, B.: Feature-based decomposition of inductive proofs applied to real-time avionics software: An experience report. In: ICSE 2004: Proceedings of the 26th International Conference on Software Engineering, Washington, DC, USA, pp. 304\u2013313. IEEE Computer Society, Los Alamitos (2004)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in Theorem Proving and Model Checking for Protocol Verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 662\u2013681. Springer, Heidelberg (1996)"},{"issue":"5","key":"10_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00165-006-0013-4","volume":"19","author":"B. Jacobs","year":"2007","unstructured":"Jacobs, B., Smetsers, S., Wichers Schreur, R.: Code-carrying theories. Formal Asp. Comput.\u00a019(2), 191\u2013203 (2007)","journal-title":"Formal Asp. Comput."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-45251-6_23","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"S. Katz","year":"2001","unstructured":"Katz, S.: Faithful translations among models and specifications. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 419\u2013434. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-73368-3_6","volume-title":"Computer Aided Verification","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Kiniry, J.R., Poll, E.: A jml tutorial: Modular specification and verification of functional behavior for java. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, p. 37. Springer, Heidelberg (2007)"},{"key":"10_CR19","unstructured":"McMillan, K.L.: The SMV System. Carnegie Mellon University (1998-2001), \n                    \n                      http:\/\/www.cs.cmu.edu\/~modelcheck\/smv.html"},{"key":"10_CR20","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":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"10_CR22","unstructured":"Pantelic, V., Jin, X.-H., Lawford, M., Parnas, D.L.: Inspection of concurrent systems: Combining tables, theorem proving and model checking. In: Arabnia, H.R., Reza, H. (eds.) Software Engineering Research and Practice, pp. 629\u2013635. CSREA Press (2006)"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"issue":"3","key":"10_CR24","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/s10009-005-0218-5","volume":"8","author":"E.R. Robby","year":"2006","unstructured":"Robby, E.R., Dwyer, M.B., Hatcliff, J.: Checking jml specifications using an extensible software model checking framework. STTT\u00a08(3), 280\u2013299 (2006)","journal-title":"STTT"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44618-4_1","volume-title":"CONCUR 2000 - Concurrency Theory","author":"N. Shankar","year":"2000","unstructured":"Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 1\u201316. Springer, Heidelberg (2000)"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Sutter, H.: The free lunch is over: A fundamental turn toward concurrency in software. Dr. Dobb\u2019s Journal\u00a030(3) (March 2005)","DOI":"10.1145\/1095408.1095421"},{"key":"10_CR27","unstructured":"Tews, H., Weber, T., V\u00f6lp, M., Poll, E., van Eekelen, M., van Rossum, P.: Nova Micro\u2013Hypervisor Verification. Technical Report ICIS\u2013R08012, Radboud University Nijmegen, Robin deliverable D13 (May 2008)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-79707-4_14","volume-title":"Formal Methods for Industrial Critical Systems","author":"M. Eekelen van","year":"2008","unstructured":"van Eekelen, M., ten Hoedt, S., Schreurs, R., Usenko, Y.S.: Analysis of a session-layer protocol in mcrl2. verification of a real-life industrial implementation. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 182\u2013199. Springer, Heidelberg (2008)"},{"issue":"2","key":"10_CR29","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng.\u00a010(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03240-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:26:28Z","timestamp":1558268788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03240-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032394","9783642032400"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03240-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}