{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215981},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664253"},{"type":"electronic","value":"9783540483205"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48320-9_8","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T13:52:42Z","timestamp":1195134762000},"page":"82-97","source":"Crossref","is-referenced-by-count":27,"title":["Automating Modular Verification"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Luca","family":"de Alfaro","sequence":"additional","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Freddy Y. C.","family":"Mang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,19]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T. A. Henzinger. Reactive modules. In Proc. 11th IEEE Symp. Logic in Comp. Sci.., 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha: modularity in model checking. In Computer Aided Verification, LNCS 1427, pages 521\u2013525. Springer-Verlag, 1998."},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Mart\u00edn Abadi and Leslie Lamport. Conjoining specifications. ACM Trans. Prog. Lang. Sys.., 17(3):507\u2013534, 1995.","journal-title":"ACM Trans. Prog. Lang. Sys.."},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1145\/320613.320614","volume":"5","author":"C. Beeri","year":"1980","unstructured":"C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems, 5:241\u2013259, 1980.","journal-title":"ACM Transactions on Database Systems"},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BFb0032443","volume-title":"EDBT\u201992: 3rd International Conference on ExtendingDatabase Technology","author":"D. Barbara","year":"1992","unstructured":"D. Barbara and H. Garcia-Molina. The demarcation protocol: a technique for maintaining linear arithmetic constraints in distributed database systems. In EDBT\u201992: 3rd International Conference on ExtendingDatabase Technology, LNCS 580, pages 373\u2013388. SpringerVerlag, 1992."},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"1996","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In Computer Aided Verification, LNCS 1102, pages 428\u2013432. Springer-Verlag, 1996."},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"P. Cousot and R. Cousot. Refining model checking by abstract interpretation Automated Software Engineering Journal, 6(1):69\u201395, 1999.","journal-title":"Automated Software Engineering Journal"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic. In Proc. 10th ACM Symp. Princ. of Prog. Lang.., 1983.","DOI":"10.1145\/567067.567080"},{"key":"8_CR9","unstructured":"D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Technical University of Eindhoven, 1996."},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In Computer Aided Verification, LNCS. Springer-Verlag, 1997."},{"key":"8_CR11","unstructured":"G. J. Holzman. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"8_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/3-540-49519-3_27","volume-title":"Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD 1998)","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, S. Qadeer, S. K. Rajamani, and S. Tasiran. An assume-guarantee rule for checking simulation. In Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD 1998), LNCS 1522, pages 421\u2013432. SpringerVerlag, 1998."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-aided Verification of Coordinating Processes: The AutomataTheoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"8_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K. L. McMillan","year":"1997","unstructured":"K. L. McMillan. A compositional rule for hardware design refinement. In Computer Aided Verification, LNCS 1254, pages 24\u201335. Springer-Verlag, 1997."},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P. J. Ramadge","year":"1987","unstructured":"P. J. Ramadge and W. M. Wonham. Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization, 25:206\u2013230, 1987.","journal-title":"SIAM Journal of Control and Optimization"},{"key":"8_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"Proc. of 5th Conference on Foundations of Software Technology and Theoretical Computer Science","author":"E. W. Stark","year":"1985","unstructured":"E. W. Stark. A proof technique for rely\/guarantee properties. In Proc. of 5th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 206, pages 369\u2013391. Springer-Verlag, 1985."},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1968","unstructured":"J. W. Thatcher and J. B. Wright. Generalized finite-automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2:57\u201381, 1968.","journal-title":"Mathematical Systems Theory"}],"container-title":["Lecture Notes in Computer Science","CONCUR\u201999 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48320-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T18:56:50Z","timestamp":1684090610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48320-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664253","9783540483205"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48320-9_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}