{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:37:03Z","timestamp":1725896223795},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_13","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"174-190","source":"Crossref","is-referenced-by-count":0,"title":["A Proof Framework for Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Leonard","family":"Lensink","sequence":"first","affiliation":[]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence (2000)"},{"key":"13_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/3-540-49059-0_19","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"T. Basten","year":"1999","unstructured":"Basten, T., Hooman, J.: Process Algebra in PVS. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 270\u2013284. Springer, Heidelberg (1999)"},{"key":"13_CR4","unstructured":"de Groot, A.: Practical Automaton Proofs in PVS. PhD thesis, Radboud University Nijmegen (2008)"},{"issue":"5","key":"13_CR5","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"},{"key":"13_CR6","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., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 419\u2013434. Springer, Heidelberg (2001)"},{"issue":"8","key":"13_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A New Solution of Dijkstra\u2019s Concurrent Programming Problem. Commun. ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"1-2","key":"13_CR8","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. Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","first-page":"747","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. 747\u2013752. Springer, Heidelberg (1992)"},{"key":"13_CR11","unstructured":"Pantelic, V., Jin, X.-H., Lawford, M., Parnas, D.L.: Inspection of concurrent systems: Combining tables, theorem proving and model checking. In: Software Engineering Research and Practice, pp. 629\u2013635 (2006)"},{"key":"13_CR12","unstructured":"Ripon, S., Miller, A.: Verification of symmetry detection using pvs. ECEASST\u00a035 (2010)"},{"key":"13_CR13","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":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-03240-0_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"B. Gastel van","year":"2009","unstructured":"van Gastel, B., Lensink, L., Smetsers, S., van Eekelen, M.: Reentrant Readers-Writers: A Case Study Combining Model Checking with Theorem Proving. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, pp. 85\u2013102. Springer, Heidelberg (2009)"},{"issue":"2","key":"13_CR15","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.scico.2010.03.004","volume":"76","author":"B. Gastel van","year":"2011","unstructured":"van Gastel, B., Lensink, L., Smetsers, S., van Eekelen, M.: Deadlock and Starvation Free Reentrant Readers-Writers. Sci. Comput. Program.\u00a076(2), 82\u201399 (2011)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T16:55:01Z","timestamp":1556902501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}