{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:41:49Z","timestamp":1773654109525,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581796","type":"print"},{"value":"9783540484691","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:26:00Z","timestamp":1330269960000},"page":"55-67","source":"Crossref","is-referenced-by-count":68,"title":["Symbolic verification with periodic sets"],"prefix":"10.1007","author":[{"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Wolper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, May 1993.","journal-title":"Information and Computation"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428\u2013439, Philadelphia, June 1990.","DOI":"10.1109\/LICS.1990.113767"},{"issue":"3","key":"5_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"Randal E. Bryant. Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys, 24(3):293\u2013318, 1992.","journal-title":"ACM Computing Surveys"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM Symposium on Principles of Programming Langages, 1978.","DOI":"10.1145\/512760.512770"},{"key":"5_CR5","first-page":"23","volume-title":"volume 531 of Lecture Notes in Computer Science","author":"O. Coudert","year":"1990","unstructured":"O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagram. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 23\u201332, Rutgers, June 1990. Springer-Verlag."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 181\u2013191, Aalborg, July 1991.","DOI":"10.1007\/3-540-55179-4_18"},{"key":"5_CR8","first-page":"71","volume-title":"Lacture Notes in Computer Science","author":"S. Graf","year":"1993","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In Computer Aided Verification, Proc. 5th Int. Workshop, volume 697, pages 71\u201384, Elounda, Crete, June 1993. Lacture Notes in Computer Science, Springer-Verlag."},{"key":"5_CR9","first-page":"176","volume-title":"volume 531 of Lecture Notes in Computer Science","author":"P. Godefroid","year":"1990","unstructured":"P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 176\u2013185, Rutgers, June 1990. Springer-Verlag."},{"key":"5_CR10","volume-title":"Integer Programming","author":"H. Greenberg","year":"1971","unstructured":"H. Greenberg. Integer Programming. Academic Press, New York, 1971."},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149\u2013164, April 1993.","journal-title":"Formal Methods in System Design"},{"key":"5_CR12","volume-title":"Lecture Notes in Computer Science","author":"N. Halbwachs","year":"1993","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In Proc. 5th Workshop on Computer Aided Verification, volume 697, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag."},{"key":"5_CR13","volume-title":"Coverage preserving reduction strategies for reachability analysis","author":"G. J. Holzmann","year":"1992","unstructured":"G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland."},{"issue":"12","key":"5_CR14","doi-asserted-by":"crossref","first-page":"2413","DOI":"10.1002\/j.1538-7305.1985.tb00010.x","volume":"64","author":"G. J. Holzmann","year":"1985","unstructured":"G. J. Holzmann. Tracing protocols. AT&T Technical Journal, 64(12):2413\u20132434, 1985.","journal-title":"AT&T Technical Journal"},{"key":"5_CR15","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991."},{"key":"5_CR16","first-page":"189","volume-title":"Lecture Notes in Computer Science","author":"C. Jard","year":"1989","unstructured":"C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189\u2013196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag."},{"key":"5_CR17","first-page":"110","volume-title":"Lecture Notes in Computer Science","author":"A.S. Krishnakumar","year":"1993","unstructured":"A.S. Krishnakumar. Reachability and recurrence in extended finite state machines: Modular vector addition systems. In Proc. 5th Workshop on Computer Aided Verification, volume 697, pages 110\u2013122, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"F. Kabanza, J.-M. St\u00e9venne, and P. Wolper. Handling infinite temporal data. In Proc. of the 9th ACM Symposium on Principles of Database Systems, pages 392\u2013403, Nashville Tennessee, 1990.","DOI":"10.1145\/298514.298590"},{"key":"5_CR19","volume-title":"Research Report 1662","author":"H. LeVerge","year":"1992","unstructured":"H. LeVerge. A note on Chernikova's algorithm. Research Report 1662, INRIA, Rennes, April 1992."},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B. Lubachevsky","year":"1984","unstructured":"B. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. I. Acta Informatica, 21:125\u2013169, 1984.","journal-title":"Acta Informatica"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"5_CR22","volume-title":"Rapport de Recherche LIX\/RR\/90\/09","author":"N. Mercouroff","year":"1990","unstructured":"N. Mercouroff. Analyse s\u00e9mantique de communications entre processus de programmes parall\u00e8les. Rapport de Recherche LIX\/RR\/90\/09, Ecole Polytechnique, Palaiseau, France, September 1990."},{"key":"5_CR23","volume-title":"Linear and Combinatorial Programming","author":"K. Murty","year":"1976","unstructured":"K. Murty. Linear and Combinatorial Programming. Wiley, New York, 1976."},{"key":"5_CR24","volume-title":"Lecture Notes in Computer Science","author":"D. Peled","year":"1993","unstructured":"D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Conference on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag."},{"key":"5_CR25","unstructured":"A. Valmari. State space generation with induction. In Proc. Scandinavian Conference on Artificial Intelligence \u2014 89, pages 99\u2013115, Tampere, Finland, June 1989."},{"key":"5_CR26","first-page":"156","volume-title":"volume 531 of Lecture Notes in Computer Science","author":"A. Valmari","year":"1990","unstructured":"A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156\u2013165, Rutgers, June 1990. Springer-Verlag."},{"key":"5_CR27","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, June 1986."},{"key":"5_CR28","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C.H. West","year":"1978","unstructured":"C.H. West. Generalized technique for communication protocol validation. IBM J. of Res. and Devel., 22:393\u2013404, 1978.","journal-title":"IBM J. of Res. and Devel."},{"key":"5_CR29","first-page":"233","volume-title":"Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science","author":"P. Wolper","year":"1993","unstructured":"P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 233\u2013246, Hildesheim, August 1993. Springer-Verlag."},{"key":"5_CR30","first-page":"210","volume-title":"Lecture Notes in Computer Science","author":"M. Yannakakis","year":"1993","unstructured":"M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In Proc. 5th Workshop on Computer Aided Verification, volume 697 pages 210\u2013224, Elounda, Crete June 1993. Lecture Notes in Computer Science, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:22:22Z","timestamp":1742595742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}