{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:43Z","timestamp":1760586463719},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2008,5,17]],"date-time":"2008-05-17T00:00:00Z","timestamp":1210982400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2008,6]]},"DOI":"10.1007\/s10703-008-0055-8","type":"journal-article","created":{"date-parts":[[2008,5,16]],"date-time":"2008-05-16T16:22:07Z","timestamp":1210954927000},"page":"207-234","source":"Crossref","is-referenced-by-count":27,"title":["Automatic symbolic compositional verification by\u00a0learning assumptions"],"prefix":"10.1007","volume":"32","author":[{"given":"Wonhong","family":"Nam","sequence":"first","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,5,17]]},"reference":[{"key":"55_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans Program Lang Syst (TOPLAS) 17:507\u2013534","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"issue":"1","key":"55_CR2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger T (1999) Reactive modules. Form Methods Syst Des 15(1):7\u201348. Invited submission to FLoC\u201996 special issue. A preliminary version appears in Proceedings of the 11th LICS, 1996","journal-title":"Form Methods Syst Des"},{"key":"55_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasiran S (1998) MOCHA: Modularity in model checking. In: Proceedings of the 10th international conference on computer aided verification, pp 516\u2013520","DOI":"10.1007\/BFb0028774"},{"key":"55_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-48320-9_8","volume-title":"CONCUR\u201999: Concurrency theory, tenth international conference","author":"R Alur","year":"1999","unstructured":"Alur R, de Alfaro L, Henzinger T, Mang F (1999) Automating modular verification. In: CONCUR\u201999: Concurrency theory, tenth international conference. LNCS, vol\u00a01664. Springer, Berlin, pp\u00a082\u201397"},{"key":"55_CR5","doi-asserted-by":"crossref","unstructured":"Alur R, Cern\u00fd P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of the 32nd symposium on principles of programming languages, POPL 2005, pp 98\u2013109","DOI":"10.1145\/1040305.1040314"},{"key":"55_CR6","doi-asserted-by":"crossref","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of the 17th international conference of computer aided verification, CAV 2005, pp 548\u2013562","DOI":"10.1007\/11513988_52"},{"key":"55_CR7","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75:87\u2013106","journal-title":"Inf Comput"},{"key":"55_CR8","unstructured":"Barringer H, Pasareanu C, Giannakopoulou D (2003) Proof rules for automated compositional verification through learning. In: Proceedings of the 2nd international workshop on specification and verification of component based systems"},{"key":"55_CR9","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems, pp 193\u2013207","DOI":"10.21236\/ADA360973"},{"issue":"4","key":"55_CR10","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1137\/S0895480198340943","volume":"13","author":"A Birkendorf","year":"2000","unstructured":"Birkendorf A, B\u00f6ker A, Simon H-U (2000) Learning deterministic finite automata from smallest counterexamples. SIAM J Discrete Math 13(4):465\u2013491","journal-title":"SIAM J Discrete Math"},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Bryant R (1986) Graph-based algorithms for boolean-function manipulation. IEEE Trans Comput, C-35(8)","DOI":"10.1109\/TC.1986.1676819"},{"key":"55_CR12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th international conference on computer-aided verification (CAV 2002)","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV Version 2: An OpenSource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer-aided verification (CAV 2002). LNCS, vol\u00a02404. Springer, Berlin, pp\u00a0359\u2013364"},{"key":"55_CR13","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of international conference on computer aided verification (CAV\u201900), pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"55_CR14","series-title":"LNCS","first-page":"331","volume-title":"Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of software","author":"J Cobleigh","year":"2003","unstructured":"Cobleigh J, Giannakopoulou D, Pasareanu C (2003) Learning assumptions for compositional verification. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of software. LNCS, vol\u00a02619. Springer, Berlin, pp\u00a0331\u2013346"},{"key":"55_CR15","doi-asserted-by":"crossref","unstructured":"Cobleigh J, Avrunin G, Clarke L (2006) Breaking up is hard to do: An investigation of decomposition for assume-guarantee reasoning. In: Proceedings of the international symposium on software testing and analysis, pp 97\u2013108","DOI":"10.1145\/1146238.1146250"},{"key":"55_CR16","unstructured":"Fiduccia C, Mattheyses R (1982) A linear-time heuristic for improving network partitions. In: Proceedings of the 19th design automation conference, pp 241\u2013247"},{"key":"55_CR17","unstructured":"Giannakopoulou D, Pasareanu C (2005) Learning-based assume-guarantee verification. In: Proceeding of the 12th international spin workshop, pp 282\u2013287"},{"key":"55_CR18","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D, Pasareanu C, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of 17th IEEE international conference on automated software engineering (ASE 2002), pp 3\u201312","DOI":"10.1109\/ASE.2002.1114984"},{"issue":"3","key":"55_CR19","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Gr\u00fcmberg","year":"1994","unstructured":"Gr\u00fcmberg O, Long D (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"Gupta A, McMillan K, Fu Z (2007) Automated assumption generation for compositional verification. In: Proceedings of the 19th international conference of computer aided verification, CAV 2007, pp 420\u2013432","DOI":"10.1007\/978-3-540-73368-3_45"},{"key":"55_CR21","series-title":"LNCS","first-page":"521","volume-title":"CAV 98: Computer-aided verification","author":"T Henzinger","year":"1998","unstructured":"Henzinger T, Qadeer S, Rajamani S (1998) You assume, we guarantee: Methodology and case studies. In: CAV 98: Computer-aided verification. LNCS, vol\u00a01427. Springer, Berlin, pp\u00a0521\u2013525"},{"issue":"2","key":"55_CR22","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/0022-0000(91)90016-X","volume":"43","author":"O Ibarra","year":"1991","unstructured":"Ibarra O, Jiang T (1991) Learning regular languages from counterexamples. J Comput Syst Sci 43(2):299\u2013316","journal-title":"J Comput Syst Sci"},{"key":"55_CR23","unstructured":"Jones C (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University"},{"key":"55_CR24","unstructured":"Karypis G, Kumar V (1999) Multilevel k-way hypergraph partitioning. In: Proceedings of the 36th conference on design automation, pp 343\u2013348"},{"issue":"1","key":"55_CR25","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/92.748202","volume":"7","author":"G Karypis","year":"1999","unstructured":"Karypis G, Aggarwal R, Kumar V, Shekhar S (1999) Multilevel hypergraph partitioning: applications in VLSI domain. IEEE Trans Very Large Scale Integr (VLSI) Syst 7(1):69\u201379","journal-title":"IEEE Trans Very Large Scale Integr (VLSI) Syst"},{"key":"55_CR26","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An introduction to computational learning theory","author":"M Kearns","year":"1994","unstructured":"Kearns M, Vazirani U (1994) An introduction to computational learning theory. MIT Press, Cambridge"},{"issue":"2","key":"55_CR27","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1002\/j.1538-7305.1970.tb01770.x","volume":"49","author":"B Kernighan","year":"1970","unstructured":"Kernighan B, Lin S (1970) An efficient heuristic procedure for partitioning graphs. Bell Syst Tech J 49(2):291\u2013307","journal-title":"Bell Syst Tech J"},{"key":"55_CR28","volume-title":"Computer-aided Verification of Coordinating Processes: The automata-theoretic approach","author":"R Kurshan","year":"1994","unstructured":"Kurshan R (1994) Computer-aided Verification of Coordinating Processes: The automata-theoretic approach. Princeton University Press, Princeton"},{"key":"55_CR29","doi-asserted-by":"crossref","unstructured":"McMillan K (1997) A compositional rule for hardware design refinement. In: Proceedings of the 9th international conference on computer aided verification, pp 24\u201335","DOI":"10.1007\/3-540-63166-6_6"},{"key":"55_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Proceedings of the 14th international conference on computer aided verification","author":"K McMillan","year":"2002","unstructured":"McMillan K (2002) Applying SAT methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification. LNCS, vol\u00a02404. Springer, Berlin, pp\u00a0250\u2013264"},{"issue":"4","key":"55_CR31","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra J, Chandy K (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417\u2013426","journal-title":"IEEE Trans Softw Eng"},{"key":"55_CR32","doi-asserted-by":"crossref","unstructured":"Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA\u201906), pp 170\u2013185","DOI":"10.1007\/11901914_15"},{"key":"55_CR33","unstructured":"Nam W, Alur R (2007) Learning plans for safety and reachability goals with partial observability. Technical Report MS-CIS-07-16, University of Pennsylvania"},{"key":"55_CR34","doi-asserted-by":"crossref","unstructured":"Namjoshi K, Trefler R (2000) On the completeness of compositional reasoning. In: Proceedings of the 12th international conference of computer aided verification, CAV 2000, pp 139\u2013153","DOI":"10.1007\/10722167_14"},{"issue":"2","key":"55_CR35","first-page":"225","volume":"7","author":"D Peled","year":"2002","unstructured":"Peled D, Vardi M, Yannakakis M (2002) Black box checking. J Autom Lang Comb 7(2):225\u2013246","journal-title":"J Autom Lang Comb"},{"key":"55_CR36","first-page":"123","volume-title":"Logics and Models of Concurrent Systems","author":"A Pnueli","year":"1984","unstructured":"Pnueli A (1984) In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems. Springer, New York, pp 123\u2013144"},{"issue":"2","key":"55_CR37","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R Rivest","year":"1993","unstructured":"Rivest R, Schapire R (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299\u2013347","journal-title":"Inf Comput"},{"key":"55_CR38","doi-asserted-by":"crossref","unstructured":"Sharygina N, Chaki S, Clarke E, Sinha N (2005) Dynamic component substitutability analysis. In: Proceedings of the international symposium of formal methods Europe, pp 512\u2013528","DOI":"10.1007\/11526841_34"},{"key":"55_CR39","doi-asserted-by":"crossref","unstructured":"Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Proceedings of the 19th international conference of computer aided verification, CAV 2007, pp 39\u201354","DOI":"10.1007\/978-3-540-73368-3_8"},{"key":"55_CR40","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"FST & TCS 85: Foundations of software technology and theoretical computer science","author":"E Stark","year":"1985","unstructured":"Stark E (1985) A proof technique for rely-guarantee properties. In: FST & TCS 85: Foundations of software technology and theoretical computer science. LNCS, vol\u00a0206. Springer, Berlin, pp\u00a0369\u2013391"},{"key":"55_CR41","doi-asserted-by":"crossref","unstructured":"Vardhan A, Viswanathan M (2006) Lever: A tool for learning based verification. In: Proceedings of 18th international conference on computer aided verification (CAV 2006), pp 471\u2013474","DOI":"10.1007\/11817963_43"},{"key":"55_CR42","series-title":"LNCS","first-page":"494","volume-title":"Proceedings of 24th foundations of software technology and theoretical computer science","author":"A Vardhan","year":"2004","unstructured":"Vardhan A, Sen K, Viswanathan M, Agha G (2004) Actively learning to verify safety properties for FIFO automata. In: Proceedings of 24th foundations of software technology and theoretical computer science. LNCS, vol\u00a03328. Springer, Berlin, pp\u00a0494\u2013505"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0055-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0055-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0055-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T19:24:42Z","timestamp":1588706682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0055-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,17]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["55"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0055-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5,17]]}}}