{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:30:50Z","timestamp":1773192650187,"version":"3.50.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1995,1]]},"DOI":"10.1007\/bf01384316","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T03:30:13Z","timestamp":1112412613000},"page":"97-123","source":"Crossref","is-referenced-by-count":44,"title":["Using integer programming to verify general safety and liveness properties"],"prefix":"10.1007","volume":"6","author":[{"given":"James C.","family":"Corbett","sequence":"first","affiliation":[]},{"given":"George S.","family":"Avrunin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0377-2217(88)90012-4","volume":"36","author":"A. I. Ali","year":"1988","unstructured":"A. I. Ali, J. Kennington, and B. Shetty. The equal flow problem.European J. Oper. Res., 36:107?115, 1988.","journal-title":"European J. Oper. Res."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"G. S. Avrunin, U. A. Buy, and J. C. Corbett. Integer programming in the analysis of concurrent systems. In Larsen and Skou [16], pages 92?102.","DOI":"10.1007\/3-540-55179-4_10"},{"issue":"11","key":"CR3","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.1109\/32.106975","volume":"17","author":"G. S. Avrunin","year":"1991","unstructured":"G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden. Automated analysis of concurrent systems with the constrained expression toolset.IEEE Trans. Softw. Eng. 17(11):1204?1222, Nov. 1991.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"CR4","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"J. A. Bergstra","year":"1985","unstructured":"J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction.Theoretical Comput. Sci., 37(1):77?121, 1985.","journal-title":"Theoretical Comput. Sci."},{"issue":"8","key":"CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation.IEEE Transactions on Computers, C 35(8):677?691, 1986.","journal-title":"IEEE Transactions on Computers, C"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. InProceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428?439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"E. Clarke, D. Long, and K. McMillan. Compositional model checking. InProceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. InProceedings of the 19th ACM Symposium on Principles of Programming Languages, pages 343?354, Jan. 1992.","DOI":"10.1145\/143165.143235"},{"key":"CR9","unstructured":"E. M. Clarke and R. P. Kurshan, editors.Computer-Aided Verification '90, number 3 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Providence, RI, 1991. American Mathematical Society."},{"issue":"1","key":"CR10","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems.ACM Trans. Prog. Lang. Syst., 15(1):36?72, Jan. 1993.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"CR11","unstructured":"J. C. Corbett.Automated Formal Analysis Methods for Concurrent and Real-Time Software. PhD thesis, University of Massachusetts at Amherst, 1992."},{"issue":"4","key":"CR12","doi-asserted-by":"crossref","first-page":"841","DOI":"10.1145\/4221.4223","volume":"32","author":"H. Garcia-Molina","year":"1985","unstructured":"H. Garcia-Molina and D. Barbara. How to assign votes in a distributed system.J. ACM, 32(4):841?860, Oct. 1985.","journal-title":"J. ACM"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Larsen and Skou [16], pages 332?242.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"CR14","unstructured":"C. A. R. Hoare.Communicating Sequential Processes. Prentice-Hall International, 1985."},{"key":"CR15","unstructured":"R. Hojati, H. Touati, R. P. Kurshan, and R. K. Brayton. Efficient ?-regular language containment. In G. v. Bochmann and D. K. Probst, editors,Computer Aided Verification, 4th International Workshop Proceedings, volume 663 ofLecture Notes in Computer Science, pages 371?382, Montreal, Canada, 1992. Springer-Verlag."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and A. Skou, editors.Computer Aided Verification, 3rd International Workshop Proceedings, volume 575 ofLecture Notes in Computer Science, Aalborg, Denmark, July 1991. Springer-Verlag.","DOI":"10.1007\/3-540-55179-4"},{"key":"CR17","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner.Communication and Concurrency. Prentice Hall, London, 1989."},{"key":"CR18","unstructured":"D. K. Probst and H. F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. In Clarke and Kurshan [9], pages 15?24. Also LNCS 531, pp. 15?24."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor,Handbook of Theoretical Computer Science, volume B. MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"CR20","unstructured":"A. Valmari. Compositional state space generation. InEuropean Conference on Petri Nets, pages 43?62, 1990."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"A. Valmari. A stubborn attack on state explosion. In Clarke and Kurshan [9], pages 25?41.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"W. J. Yeh and M. Young. Compositional reachability analysis using process algebra. InProceedings of the Symposium on Testing, Analysis, and Verification (TAV4), pages 178?187, New York, Oct. 1991. ACM SIGSOFT, Association for Computing Machinery.","DOI":"10.1145\/120807.120812"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"H. Zuidweg. Verification by abstraction and bisimulation. In J. Sifakis, editor,Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, pages 105?166, June 1989. Appeared asLecture Notes in Computer Science 407.","DOI":"10.1007\/3-540-52148-8_10"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384316.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384316\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T03:28:58Z","timestamp":1735529338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["BF01384316"],"URL":"https:\/\/doi.org\/10.1007\/bf01384316","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}