{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:18:09Z","timestamp":1778249889281,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664598","type":"print"},{"value":"9783540482949","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48294-6_18","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:16:02Z","timestamp":1186157762000},"page":"284-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstract Animator for Temporal Specifications: Application to TLA"],"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"}]}],"member":"297","published-online":{"date-parts":[[1999,10,1]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B book\u2013Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"18_CR2","unstructured":"D. Cansell, J.-P. Gibson, B. Mermet, and D. M\u00e9ry. Sp\u00e9cification de services dans une logique temporelle compositionnelle. Rapport final du march\u00e9 n\u00b096 1B CNET-CNRS-CRIN, LORIA UMR 7503 Laboratoire Lorrain de Recherche en Informatique et Applications, f\u00e9vrier 1999."},{"key":"18_CR3","unstructured":"D. Cansell and D. M\u00e9ry. Interpr\u00e9tation de sp\u00e9cifications temporelles \u00e0 l\u2019aide d\u2019un outil de preuve. In AFADL: Approches formelles dans l\u2019assistance au d\u00e9veloppement de logiciels, sept, nov 1998."},{"key":"18_CR4","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"P. Cousot. Calculational System Design, chapter The Calculational Design of a Generic Abstract Interpreter. NATO ASI Series F. Amsterdam: IOS Press, 1999."},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Fourth Conference on Principles of Programming Languages POPL, pages 238\u2013252, Los Angeles, California, 1977. ACM Press.","DOI":"10.1145\/512950.512973"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Sixth Conference on Principles of Programming Languages POPL, pages 269\u2013282, San Antonio, Texas, 1979. ACM Press.","DOI":"10.1145\/567752.567778"},{"issue":"4","key":"18_CR7","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511\u2013547, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"J.-P. Gibson, B. Mermet, and D. M\u00e9ry. Feature interactions: A mixed semantic model approach. In Gerard O\u2019Regan and Sharon Flynn, editors, 1st Irish Workshop on Formal Methods, Dublin, Ireland, July 1997. Irish Formal Methods Special Interest Group (IFMSIG), Springer Verlag. http:\/\/ewic.springer.co.uk\/.","DOI":"10.14236\/ewic\/FM1997.3"},{"key":"18_CR9","unstructured":"J.-P. Gibson and D. M\u00e9ry. Always and Eventually in Object Requirements. In Rigorous Object Oriented Methods ROOM2 (Bradford), 1998."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"J.-P. Gibson and D. M\u00e9ry. COTSR Proceedings, chapter Fair Objects, page ?? Computer Science and Electronic Engineering. Horwood Publishing Ltd, October 1998.","DOI":"10.1533\/9781782420613.122"},{"key":"18_CR11","unstructured":"J.-P. Gibson and D. M\u00e9ry. Fair objects. In H. Zedan, editor, OT\u201998 1st UK Colloquium on Object Technology & System Re-engineering (COTSR), 6\u20198 April 1998."},{"key":"18_CR12","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":"18_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-53982-4_10","volume-title":"Proc TAPSOFT\u201991, Volume 1 (CAAP\u201991)","author":"P. Granger","year":"1991","unstructured":"P. Granger. Static analysis of linear congruence equalities among variables of a program. In S. Abramsky and T.S.E. Maibaum, editors, Proc TAPSOFT\u201991, Volume 1 (CAAP\u201991), Brighton, UK, LNCS 493, pages 169\u2013192. Springer-Verlag, 1991."},{"key":"18_CR14","unstructured":"P. Lacan, J.N. Monfort, Le Vinh Quy Ribal, A. Deutsch, and G. Gonthier. The software reliability verification process: The Ariane 5 example. In Proceedings DASIA 98\u2013DAta Systems IN Aerospace, Athens, Greece. ESA Publications, SP-422, May 25\u201328 1998."},{"key":"18_CR15","unstructured":"L. Lamport. How to write a long formula. Technical report, COMPAQ Palo Alto, http:\/\/www.research.digital.com\/SRC\/tla\/, december 1993."},{"issue":"3","key":"18_CR16","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"},{"key":"18_CR17","unstructured":"L. Lamport. The TLA\/TLA\n                           +\n                           WEB page. COMPAQ Palo Alto, http:\/\/www.research.digital.com\/SRC\/tla\/, 1999."},{"key":"18_CR18","unstructured":"L. Lamport and L. C. Paulson. Should your specification language be typed? Technical report SRC Research Report 147, SRC, 1998."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checkin. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"18_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification Proceedings","author":"D. M\u00e9ry","year":"1992","unstructured":"D. M\u00e9ry and A. Mokkedem. Crocos: An integrated environment for interactive verification of sdl specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings, Lecture Notes in Computer Science. Springer Verlag, 1992."},{"key":"18_CR21","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":"Stephan 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, dec 1997. Springer-Verlag."},{"key":"18_CR22","unstructured":"Steria M\u00e9diterrann\u00e9e. Atelier B, Version 3.2, Manuel de R\u00e9f\u00e9rence du Langage B. GEC Alsthom Transport and Steria M\u00e9diterrann\u00e9e and SNCF and INRETS and RATP, 1997."},{"key":"18_CR23","unstructured":"Union Internationale des T\u00e9l\u00e9communications. Introduction \u00e0 l\u2019ensemble de capacit\u00e9s 1 du r\u00e9seau intelligent. Technical Report UIT-T Q.1211, Union Internationale des T\u00e9l\u00e9communications, march 1993. R\u00e9seau Intelligent."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48294-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:02:48Z","timestamp":1778248968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-48294-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664598","9783540482949"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-48294-6_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"1 October 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}