{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:13Z","timestamp":1725664993100},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643593"},{"type":"electronic","value":"9783540697565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-64359-1_744","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:41:03Z","timestamp":1330299663000},"page":"807-819","source":"Crossref","is-referenced-by-count":0,"title":["On the automatic validation of parameterized unity programs"],"prefix":"10.1007","author":[{"given":"J. -P.","family":"Bodeveix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"81_CR1","unstructured":"W. Ackermann. Solvable cases of the decision problem. NORTH-HOLLAND, 1968."},{"key":"81_CR2","unstructured":"F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992."},{"issue":"4","key":"81_CR3","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"J. Archibald","year":"1986","unstructured":"J. Archibald and J.-L. Baer. Cache coherence protocols: Evaluation using a multiprocessor simulation model. ACM Transactions on Computer Systems, 4(4):273\u2013298, nov 1986.","journal-title":"ACM Transactions on Computer Systems"},{"key":"81_CR4","doi-asserted-by":"crossref","unstructured":"J.-P. Bodeveix and M. Filali. On the refinement of symmetric' memory protocols. In Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 58\u201374. Springer-Verlag, sep 1995.","DOI":"10.1007\/3-540-60275-5_57"},{"key":"81_CR5","unstructured":"J.-P. Bodeveix and M. Filali. (quantifier elimination technics for program validation. Technical Report IRIT\/97-44-R, IRIT, nov 1997."},{"key":"81_CR6","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 10E20 states and beyond. In 5th Symposium on Logic in Computer Science, jun 1990."},{"key":"81_CR7","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design, A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"81_CR8","unstructured":"P. Doherty, W. Lukaszewicz, and A. Szalas. Computing circumpscription revisited: a reduction algorithm. Journal of automated reasonning, (x):1\u201342, 1995."},{"key":"81_CR9","unstructured":"Dov. Gabbay and Hans Jdrgen. Ohlbach. Quantifier elimination in second-order predicate logic. Technical Report 94-231, MPI, jul 1992."},{"key":"81_CR10","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1994."},{"key":"81_CR11","doi-asserted-by":"crossref","unstructured":"J.G. Henriksen, J.L. Jensen, M.S. Jorgensen, N. Klarlund, R. Paige, T. Rauhe, and A.B. Sandholm. Mona: Monadic second-order logic in practice. In Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 58\u201373, Aarhus, may 1995.","DOI":"10.1007\/3-540-60630-0_5"},{"key":"81_CR12","unstructured":"G.J. Holzmann. Design and validation of computer protocols. Prentice Hall, 1991."},{"issue":"3","key":"81_CR13","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, may 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"81_CR14","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 temporal prover. Technical Report STAN-CS-TR-94-151, Stanford University, jul 1994.","DOI":"10.21236\/ADA324036"},{"key":"81_CR15","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J.v. Leeuwen, editor, Handbook of Theoretical Computer Science, pages 133\u2013192. MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"81_CR16","unstructured":"J. van der Does. Lectures on quantifiers. In http:\/\/turing.wins.uva.nl\/-jvddoeslbookslQlectures.ps.Z, aug 1996."},{"key":"81_CR17","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In ACM, editor, ACM Symposium on Principles of Programming Languages, pages 184\u2013193, jan 1986. *** DIRECT SUPPORT *** A0008D07 00023","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Parallel and Distributed Processing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-64359-1_744.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:20:27Z","timestamp":1605648027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-64359-1_744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643593","9783540697565"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-64359-1_744","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}