{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:30:12Z","timestamp":1755217812279,"version":"3.43.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1023\/a:1012960513376","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T10:14:19Z","timestamp":1040638459000},"page":"69-89","source":"Crossref","is-referenced-by-count":0,"title":["Reduction and Quantifier Elimination Techniques for Program Validation"],"prefix":"10.1007","volume":"20","author":[{"given":"Jean-Paul","family":"Bodeveix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"386597_CR1","unstructured":"W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1968."},{"issue":"4","key":"386597_CR2","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"J. Archibald","year":"1986","unstructured":"J. Archibald and J.-L. Baer, \u201cCache coherence protocols: Evaluation using a multiprocessor simulation model,\u201d ACM Transactions on Computer Systems, Vol. 4, No. 4, pp. 273\u2013298, 1986.","journal-title":"ACM Transactions on Computer Systems"},{"key":"386597_CR3","unstructured":"J.-P. Bodeveix, D. Carri\u00e8re, and M. Filali, \u201cA refinement-based validation of a cache coherence protocol,\u201d in 10th International Conference on Parallel and Distributed Computing Systems, New Orleans, Louisiana, USA, October 1997, ISCA, pp. 332\u2013337."},{"key":"386597_CR4","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, \u201cSymbolic model checking: 10E20 states and beyond,\u201d in 5th Symposium on Logic in Computer Science, June 1990."},{"key":"386597_CR5","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, Reading, MA, 1988."},{"key":"386597_CR6","unstructured":"S. Crow, S. Owre, J. Rushby, N. Shankar, and S. Mandayam, \u201cA tutorial introduction to PVS,\u201d in Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, http:\/\/www.csl.sri.com\/pvs, April 1995."},{"key":"386597_CR7","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra, A Discipline of Programming, Prentice Hall, Englewood Cliffs NJ, 1976."},{"key":"386597_CR8","first-page":"1","volume":"10","author":"P. Doherty","year":"1995","unstructured":"P. Doherty, W. Lukaszewicz, and A. Szalas, \u201cComputing circumpscription revisited: A reduction algorithm,\u201d Journal of Automated Reasonning, Vol. 10, pp. 1\u201342, 1995.","journal-title":"Journal of Automated Reasonning"},{"key":"386597_CR9","unstructured":"D. Gabbay and H.J. Ohlbach, \u201cQuantifier elimination in second-order predicate logic,\u201d Technical Report 94-231, MPI, July 1992."},{"key":"386597_CR10","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1994","unstructured":"M.J.C. Gordon and T.F. Melham, Introduction to HOL, Cambridge University Press, Cambridge, UK, 1994."},{"key":"386597_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, \u201cMona: Monadic second-order logic in practice,\u201d in Workshop on Tools and Algorithms for the Construction and Analysis of Systems, May 1995, Aarhus, pp. 58\u201373.","DOI":"10.1007\/3-540-60630-0_5"},{"key":"386597_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, Englewood Cliffs, 1991."},{"issue":"9","key":"386597_CR13","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"L. Lamport, \u201cHow to make a multiprocessor that correctly executes multiprocess programs,\u201d IEEE Transactions on Computers, Vol. 28, No. 9, pp. 690\u2013691, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"386597_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, \u201cSTeP: The Stanford temporal prover,\u201d Technical Report STAN-CS-TR-94-151, Stanford University, July 1994.","DOI":"10.21236\/ADA324036"},{"key":"386597_CR15","unstructured":"P. Sainrat, A. Mzoughi, C. Rochange, and D. Litaize, \u201cThe design of the M3S project: A multiported shared memory multiprocessor,\u201d in Supercomputing'92, November 1992."},{"key":"386597_CR16","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"W. Thomas, \u201cAutomata on infinite objects,\u201d in Handbook of Theoretical Computer Science, J.v. Leeuwen (Ed.), MIT Press, Cambridge, MA, 1990, pp. 133\u2013192."},{"key":"386597_CR17","doi-asserted-by":"crossref","unstructured":"P. Wolper, \u201cExpressing interesting properties of programs in propositional temporal logic,\u201d in ACMSymposium on Principles of Programming Languages, January 1986, ACM (Ed.), pp. 184\u2013193.","DOI":"10.1145\/512644.512661"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012960513376.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1012960513376\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012960513376.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:13:32Z","timestamp":1754424812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1012960513376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["386597"],"URL":"https:\/\/doi.org\/10.1023\/a:1012960513376","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}