{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:30:50Z","timestamp":1725492650929},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411963"},{"type":"electronic","value":"9783540409113"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40911-4_22","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T05:23:29Z","timestamp":1192771409000},"page":"380-397","source":"Crossref","is-referenced-by-count":5,"title":["Predicate Diagrams for the Verification of Reactive Systems"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Cansell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B book \u2014 Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"22_CR2","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Saidi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In 5th Langley Formal Methods Workshop, 2000. to appear."},{"key":"22_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computing abstractions of infinite state systems automatically and compositionally","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems automatically and compositionally. In Conference on Computer-Aided Verification (CAV\u201998), volume 1427 of Lecture Notes in Computer Science, pages 319\u2013331. Springer-Verlag, 1998."},{"key":"22_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Abstract animator for temporal specifications Application to TLA","author":"D. Cansell","year":"1999","unstructured":"D. Cansell and D. M\u00e9ry. Abstract animator for temporal specifications Application to TLA. In Gilberto File\u2019 and Agostino Cortesi, editors, SAS\u201999 Static Analysis Symposium, Venise, Italie, LNCS 1694, Heidelberg, September 1999. Springer Verlag."},{"key":"22_CR5","unstructured":"R. Cousot. Fondements des m\u00e9 thodes de preuve d\u2019invariance et de fatalit\u00e9 de programmes parall\u00e8 les. PhD thesis, INPL, novembre 1985. Doctorat-\u00e8s-Sciences."},{"key":"22_CR6","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstraction preserving \u2200ct\u0140, \u2203ct\u0140 and ct\u0140. In Ernst-R\u00fcdiger Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET\u201994), pages 561\u2013581. IFIP Transaction, 1994."},{"key":"22_CR7","series-title":"Lect Notes Comput Sci","first-page":"287","volume-title":"CAV\u201996","author":"L. Alfaro de","year":"1996","unstructured":"L. de Alfaro and Z. Manna. Temporal verification by diagram transformation. In R. Alur and T. A. Henzinger, editors, CAV\u201996, LNCS 1102, pages 287\u2013299. Springer-Verlag, jul. 1996."},{"key":"22_CR8","unstructured":"D. Detlefs, G. Nelson, and J. Saxe. Simplify: the ESC theorem prover. Technical report, Systems Research Center, Digital Equipment Corporation, Palo Alto, CA, November 1996."},{"key":"22_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Construction of abstract state graphs with PVS","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Conference on Computer-Aided Verification (CAV\u201997), volume 1254 of Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P. Granger","year":"1989","unstructured":"P. Granger. Static analysis of arithmetical congruences. IJCM, 30:165\u2013190, 1989.","journal-title":"IJCM"},{"key":"22_CR11","unstructured":"Hermann Hellwagner. Scalable readers\/writers synchronization on shared-memory machines. Technical report, Siemens AG, ZFE ST SN 2, 1993."},{"issue":"5","key":"22_CR12","first-page":"1512","volume":"16","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The SPIN model checker. IEEE Trans. on software engineering, 16(5):1512\u20131542, May 1997.","journal-title":"IEEE Trans. on software engineering"},{"key":"22_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/BFb0055757","volume-title":"Modularization and abstraction: The keys to practical formal verification","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to practical formal verification. In 23rd Intl. Symp. Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 54\u201371. Springer-Verlag, 1998."},{"key":"22_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-48168-0_11","volume-title":"CSL\u201999","author":"Y. Kesten","year":"1999","unstructured":"Y. Kesten and A. Pnueli. Verifying liveness by augmented abstraction. In A. Flum and M. Rodr\u00edguez-Artalejo, editors, CSL\u201999, LNCS 1683, pages 141\u2013156. Springer-Verlag, sep. 1999."},{"key":"22_CR15","unstructured":"F. Kr\u00f6ger. Temporal Logics of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1987. ISNB 3-540-17030-8."},{"issue":"8","key":"22_CR16","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"L. Lamport. A new solution of dijkstra\u2019s concurent programming problem. Communications of the ACM, 17(8):435\u2013455, May 1974.","journal-title":"Communications of the ACM"},{"issue":"3","key":"22_CR17","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"Transactions On Programming Languages and Systems"},{"issue":"9","key":"22_CR18","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1109\/32.464544","volume":"21","author":"L. Lamport","year":"1995","unstructured":"L. Lamport. TLA in pictures. IEEE Transactions on Software Engineering, 21(9):768\u2013775, September 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR19","unstructured":"L. Lamport. The operators of TLA+. Technical report-WEB TLA, Digital Equipment Corporation, 1996. http:\/\/www.research.digital.com\/SRC\/tla\/papers.html."},{"key":"22_CR20","unstructured":"L. Lamport. The module structure of tla+. Technical report-WEB TLA, Digital Equipment Corporation, 1998. http:\/\/www.research.digital.com\/SRC\/tla\/papers.html."},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bjorner, A. Browne, E. Chang, M. Colon, L. de Alfaro, H. Devarajan, H. Sipma, and T. Uribe. Step: the stanford theorem prover. Technical report, Department of Computer Science, Stanford University, June 1994.","DOI":"10.21236\/ADA324036"},{"key":"22_CR22","series-title":"Lect Notes Comput Sci","first-page":"334","volume-title":"TACAS\u2019 97","author":"Z. Manna","year":"1997","unstructured":"Z. Manna, A. Browne, H. B. Spima, and T. E. Uribe. Tools and algorithms for construction and analysis of systems. In Brinksma, editor, TACAS\u2019 97, LNCS 1217, pages 334\u2013350. Springer-Verlag, apr. 1997."},{"key":"22_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/3-540-49253-4_5","volume-title":"AMAST\u201998","author":"Z. Manna","year":"1998","unstructured":"Z. Manna, A. Browne, H. B. Spima, and T. E. Uribe. Visual abstractions for temporal verification. In A. Haeberer, editor, AMAST\u201998, LNCS 1548, pages 28\u201341. Springer-Verlag, dec. 1998."},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The temporal logics of reactive and concurrent systems-Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"22_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/3-540-63875-X_41","volume-title":"Advances in Computing Science\u2014ASIAN\u201997","author":"S. Merz","year":"1997","unstructured":"S. Merz. Rules for abstraction. In R. K. Shyamasundar and K. Ueda, editors, Advances in Computing Science\u2014ASIAN\u201997, volume 1345 of Lecture Notes in Computer Science, pages 32\u201345, Kathmandu, Nepal, Digital Equipment Corporation 1997. Springer-Verlag."},{"key":"22_CR26","unstructured":"S. Merz. On the verification of a self-stabilizing algorithm. Available at http:\/\/www.pst.informatik.uni-muenchen.de\/~merz\/papers\/dijkstra.ps.gz , 1998."},{"issue":"3","key":"22_CR27","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. Transactions On Programming Languages and Systems, 4(3):455\u2013495, July 1982.","journal-title":"Transactions On Programming Languages and Systems"},{"key":"22_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Abstract and model check while you prove","author":"H. Saidi","year":"1999","unstructured":"H. Saidi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, Conference on Computer-Aided Verification (CAV\u201999), volume 1633of Lecture Notes in Computer Science, pages 443\u2013454, Trento, Italy, 1999. Springer-Verlag."},{"key":"22_CR29","unstructured":"STERIA-Technologies de l\u2019Information,Aix-en-Provence (F).Atelier B, Manuel Utilisateur, 1998. Version 3.5."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40911-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:28:50Z","timestamp":1556904530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40911-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411963","9783540409113"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-40911-4_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}