{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:45Z","timestamp":1725664185878},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:37:35Z","timestamp":1330277855000},"page":"70-83","source":"Crossref","is-referenced-by-count":7,"title":["CAVEAT: technique and tool for computer aided verification and transformation"],"prefix":"10.1007","author":[{"given":"E. Pascal","family":"Gribomont","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"Rossetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"K.R. Apt and D.C. Kozen, Limits for Automatic Program Verification, Inform. Process. Letters 22 (1986) 307\u2013309.","journal-title":"Inform. Process. Letters"},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/3-540-51285-3_42","volume":"366","author":"R.J. Back","year":"1989","unstructured":"R.J. Back, A Method for Refining Atomicity in Parallel Algorithms, PARLE'89, Lect. Notes in Comput. Sci. 366 (1989) 199\u2013216.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1145\/48022.48023","volume":"10","author":"R.J. Back","year":"1988","unstructured":"R.J. Back and R. Kurki-Suonio, Distributed co-operation with action systems, ACM Trans. Programming Languages Syst. 10 (1988) 513\u2013554.","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"7_CR4","unstructured":"S. Bensalem et al., Property Preserving Abstractions for the Verification of Concurrent Systems, to appear in Formal Methods in System Design (1994)."},{"key":"7_CR5","unstructured":"W. Bibel, Deduction \u2014 Automated Logic, Academic Press, 1993."},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. on Computers C-35 (1986) 677\u2013691.","journal-title":"IEEE Trans. on Computers"},{"key":"7_CR7","unstructured":"J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, Proc. 5th. Symp. on Logic in Computer Science (1990) 428\u2013439."},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson and A. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Trans. Programming Languages Syst. 8 (1986) 244\u2013263.","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"966","DOI":"10.1145\/359642.359655","volume":"21","author":"E.W. Dijkstra","year":"1978","unstructured":"E.W. Dijkstra and al., On-the-Fly Garbage Collection: An Exercise in Cooperation, Comm. ACM 21 (1978) 966\u2013975.","journal-title":"Comm. ACM"},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T. Elrad","year":"1982","unstructured":"T. Elrad and N. Francez, Decomposition of Distributed Programs into Communication-closed Layers, Sci. Comput. Programming 2 (1982) 155\u2013173.","journal-title":"Sci. Comput. Programming"},{"key":"7_CR11","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1109\/32.58787","volume":"16","author":"D.M. Goldschlag","year":"1990","unstructured":"D.M. Goldschlag, Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover, IEEE Trans. on Software Eng. 16 (1990) 1005\u20131023.","journal-title":"IEEE Trans. on Software Eng."},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-58179-0_55","volume":"818","author":"S. Graf","year":"1994","unstructured":"S. Graf, Verification of a distributed Cache memory by using abstractions, Lect. Notes in Comput. Sci. 818 (1994) 207\u2013219.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-15199-0_21","volume":"186","author":"E.P. Gribomont","year":"1985","unstructured":"E.P. Gribomont, Synthesis of parallel programs invariants, TAPSOFT'85, Lect. Notes in Comput. Sci. 186 (1985) 325\u2013338.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"7_CR14","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0167-6423(90)90020-E","volume":"14","author":"E.P. Gribomont","year":"1990","unstructured":"E.P. Gribomont, Stepwise refinement and concurrency: the finite-state case, Sci. Comput. Programming 14 (1990) 185\u2013228.","journal-title":"Sci. Comput. Programming"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"E.P. Gribomont, Design, verification and documentation of concurrent systems, in Proc. 4th. Refinement workshop, J.M. Morris and R.C. Shaw (Eds), pp. 360\u2013377, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3756-6_16"},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6423(93)90007-C","volume":"21","author":"E.P. Gribomont","year":"1993","unstructured":"E.P. Gribomont, Concurrency without toil: a systematic method for parallel program design\u201d. Sci. Comput. Programming 21 (1993) 1\u201356.","journal-title":"Sci. Comput. Programming"},{"key":"7_CR17","unstructured":"N. Halbwachs and F. Maraninchi, On the symbolic analysis of combinational loops in circuits and synchronous programs, REACT Report, 1994."},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/174662.174665","volume":"16","author":"B. Jonsson","year":"1994","unstructured":"B. Jonsson, Compositional Specification and Verification of Distributed System, ACM Trans. Programming Languages Syst. 16 (1994) 259\u2013303.","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume":"697","author":"R.P. Kurshan","year":"1993","unstructured":"R.P. Kurshan and L. Lamport, Verification of a Multiplier: 64 Bits and Beyond, CAV'93, Lect. Notes in Comput. Sci. 697 (1993) 166\u2013179.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and M. McMillan, A structural induction theorem for processes, Proc. 8th ACM Symp. on Principles of Distributed Computing, Edmonton (1989).","DOI":"10.1145\/72981.72998"},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0167-6423(83)90014-X","volume":"2","author":"L. Lamport","year":"1983","unstructured":"L. Lamport, An Assertional Correctness Proof of a Distributed Algorithm, Sci. Comput. Programming 2 (1983) 175\u2013206.","journal-title":"Sci. Comput. Programming"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"L. Lamport and F.B. Schneider, Pretending Atomicity, DEC SRC Rep. 44, May 1989.","DOI":"10.1007\/BF01619383"},{"key":"7_CR23","first-page":"183","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl and W. Bibel, SETHEO: A High-Performance Theorem Prover, Jl. of Automated Reasoning 8 (1992) 183\u2013212.","journal-title":"Jl. of Automated Reasoning"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle, Hierarchical Correctness Proofs for Distributed Algorithms, Proc. 6th ACM Symp. on Principles of Distributed Computing, New-York (1987) 137\u2013151.","DOI":"10.1145\/41840.41852"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Z. Manna et al., Step: the Stanford Temporal Prover (Draft), June 1994.","DOI":"10.21236\/ADA324036"},{"key":"7_CR26","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF00881842","volume":"12","author":"J.S. Moore","year":"1994","unstructured":"J.S. Moore, Introduction to the OBDD algorithm for the ATP Community, Jl. of Automated Reasoning 12 (1994) 33\u201345.","journal-title":"Jl. of Automated Reasoning"},{"key":"7_CR27","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G. Ricart","year":"1981","unstructured":"G. Ricart and A.K. Agrawala, An optimal algorithm for mutual exclusion, Comm. ACM 24 (1981) 9\u201317 (corrigendum: Comm. ACM 24 (1981) 578).","journal-title":"Comm. ACM"},{"key":"7_CR28","doi-asserted-by":"crossref","first-page":"716","DOI":"10.1007\/BF03259394","volume":"6","author":"F. Stomp","year":"1994","unstructured":"F. Stomp and W.P. de Roever, A principle for sequential phased reasoning about distributed systems, Formal Aspects of Computing 6 (1994) 716\u2013737.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR29","unstructured":"M.Y. Vardi, P. Wolper, An Automata-Theoretic Approach To Automatic Program Verification, Proc. Symp. on Logic in Comput. Sci., Cambridge (1986) 322\u2013331."},{"key":"7_CR30","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume":"407","author":"P. Wolper","year":"1990","unstructured":"P. Wolper and V. Lovinfosse, Verifying Properties of large Sets of Processes with Network Invariants, CAV'89, Lect. Notes in Comput. Sci. 407 (1990) 68\u201380.","journal-title":"Lect. Notes in Comput. Sci."},{"key":"7_CR31","unstructured":"L. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:22:33Z","timestamp":1640942553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}