{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:23:14Z","timestamp":1773840194964,"version":"3.50.1"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2008,5,2]],"date-time":"2008-05-02T00:00:00Z","timestamp":1209686400000},"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-0053-x","type":"journal-article","created":{"date-parts":[[2008,5,1]],"date-time":"2008-05-01T15:24:55Z","timestamp":1209655495000},"page":"235-266","source":"Crossref","is-referenced-by-count":30,"title":["Verification of evolving software via component substitutability analysis"],"prefix":"10.1007","volume":"32","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nishant","family":"Sinha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,5,2]]},"reference":[{"issue":"3","key":"53_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 17(3):507\u2013534","journal-title":"ACM Trans Program Lang Syst"},{"key":"53_CR2","unstructured":"ABB (2005) http:\/\/www.abb.com"},{"key":"53_CR3","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/1040305.1040314","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201905)","author":"R Alur","year":"2005","unstructured":"Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for java classes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201905), Long Beach, CA, January 12\u201314, 2005. Assoc Comput Mach, New York, pp 98\u2013109"},{"key":"53_CR4","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1109\/LICS.1996.561320","volume-title":"Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS\u201996)","author":"R Alur","year":"1996","unstructured":"Alur R, Henzinger T (1996) Reactive modules. In: Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS\u201996), New Brunswick, NJ, July 27\u201330, 1996. IEEE Comput Soc Press, Los Alamitos, pp 207\u2013218"},{"key":"53_CR5","doi-asserted-by":"crossref","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proc of 17th int conf on computer aided verification","DOI":"10.1007\/11513988_52"},{"issue":"2","key":"53_CR6","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(2):87\u2013106","journal-title":"Inf Comput"},{"key":"53_CR7","first-page":"203","volume-title":"Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI)","author":"T Ball","year":"2001","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani S (2001) Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI), Snowbird, UT, June 20\u201322, 2001. Assoc Comput Mach, New York, pp 203\u2013213"},{"key":"53_CR8","unstructured":"Ball T, Rajamani SK (2000) Boolean programs: a model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research, Redmond, WA, February ftp:\/\/ftp.research.microsoft.com\/pub\/tr\/tr-2000-14.pdf"},{"key":"53_CR9","unstructured":"Chaki S, Clarke E, Giannakopoulou D, P\u0103s\u0103reanu CS (2004) Abstraction and assume-guarantee reasoning for automated software verification. Technical Report 05.02, Research Institute for Advanced Computer Science (RIACS), Mountain View, CA"},{"key":"53_CR10","first-page":"55","volume-title":"Proceedings of the third workshop on specification and verification of component based systems (SAVCBS)","author":"S Chaki","year":"2004","unstructured":"Chaki S, Sharygina N, Sinha N (2004) Verification of evolving software. In: Proceedings of the third workshop on specification and verification of component based systems (SAVCBS), Newport Beach CA, October 31\u2013November\u00a01, 2004. Iowa State University, Ames, pp 55\u201361"},{"key":"53_CR11","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Groce A, Ouaknine J, Strichman O, Yorav K (2004) Efficient verification of sequential and concurrent C programs. Form Methods Syst Des 25(2\u20133)","DOI":"10.1023\/B:FORM.0000040026.56959.91"},{"key":"53_CR12","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Sharygina N, Sinha N (2005) Dynamic component substitutability analysis. In: Proc of conf on formal methods","DOI":"10.1007\/11526841_34"},{"key":"53_CR13","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proc of 17th int conf on computer aided verification","DOI":"10.1007\/11513988_51"},{"key":"53_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/11513988_18","volume-title":"Proceedings of the 17th international conference on computer aided verification (CAV\u201905)","author":"S Chaki","year":"2005","unstructured":"Chaki S, Ivers J, Sharygina N, Wallnau K (2005) The comfort reasoning framework. In: Proceedings of the 17th international conference on computer aided verification (CAV\u201905), Edinburgh Scotland, July 6\u201310, 2005. Lecture notes in computer science, vol 3576. Springer, New York, pp 164\u2013169"},{"key":"53_CR15","doi-asserted-by":"crossref","unstructured":"Chaki S, Strichman O (2007) Optimized L * for assume-guarantee reasoning. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201907)","DOI":"10.1007\/978-3-540-71209-1_22"},{"key":"53_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-45657-0_35","volume-title":"Proceedings of the 14th international conference on computer aided verification (CAV\u201902)","author":"A Chakrabarti","year":"2002","unstructured":"Chakrabarti A, de Alfaro L, Henzinger TA, Jurdzinski M, Mang FYC (2002) Interface compatibility checking for software modules. In: Proceedings of the 14th international conference on computer aided verification (CAV\u201902), Copenhagen, Denmark, July 27\u201331, 2002. Lecture notes in computer science, vol\u00a02404. Springer, New York, pp 428\u2013441"},{"key":"53_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proceedings of the 12th international conference on computer aided verification (CAV\u201900)","author":"E Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification (CAV\u201900), Chicago, IL, July 15\u201319, 2000. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 154\u2013169"},{"key":"53_CR18","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1145\/143165.143235","volume-title":"Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201992)","author":"E Clarke","year":"1992","unstructured":"Clarke E, Grumberg O, Long D (1992) Model checking and abstraction. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201992), Albuquerque, NM, January 19\u201322, 1992. Assoc Comput Mach, New York, pp 343\u2013354"},{"key":"53_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of workshop on logic of programs","author":"E Clarke","year":"1982","unstructured":"Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons for branching time temporal logic. In: Proceedings of workshop on logic of programs, Yorktown Heights, New York, May 4\u20136 1982. Lecture notes in computer science, vol 131. Springer, Berlin, pp 52\u201371"},{"key":"53_CR20","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1109\/LICS.1989.39190","volume-title":"Proceedings of the fourth annual IEEE symposium on logic in computer science (LICS\u201989)","author":"E Clarke","year":"1989","unstructured":"Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Proceedings of the fourth annual IEEE symposium on logic in computer science (LICS\u201989), Pacific Grove, CA, June 5\u20138, 1989. IEEE Comput Soc, Los Alamitos, pp 353\u2013362"},{"key":"53_CR21","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge"},{"key":"53_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Proceedings of the ninth international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201903)","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh JM, Giannakopoulou D, P\u0103s\u0103reanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the ninth international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201903), Warsaw Poland, April 7\u201311, 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 331\u2013346"},{"key":"53_CR23","doi-asserted-by":"crossref","unstructured":"Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Proc of the ACM\/SIGSOFT international symposium on software testing and analysis, pp 97\u2013108","DOI":"10.1145\/1146238.1146250"},{"key":"53_CR24","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Proceedings of the 10th international conference on computer aided verification (CAV\u201998)","author":"M Col\u00f3n","year":"1998","unstructured":"Col\u00f3n M, Uribe TE (1998) Generating finite-state abstractions of reactive systems using decision procedures. In: Proceedings of the 10th international conference on computer aided verification (CAV\u201998), Vancouver, Canada, June 28\u2013July\u00a02, 1998. Lecture notes in computer science, vol 1427. Springer, Berlin, pp 293\u2013304"},{"key":"53_CR25","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1109\/LICS.2001.932482","volume-title":"Proceedings of the 16th annual IEEE symposium on logic in computer science (LICS\u201901)","author":"S Das","year":"2001","unstructured":"Das S, Dill DL (2001) Successive approximation of abstract transition relations. In: Proceedings of the 16th annual IEEE symposium on logic in computer science (LICS\u201901), Boston, MA, June 16\u201319, 2001. IEEE Comput Soc, Los Alamitos, pp 51\u201360"},{"key":"53_CR26","first-page":"109","volume-title":"Proceedings of the ninth ACM SIGSOFT symposium on foundations of software engineering (FSE\u201901)","author":"L Alfaro de","year":"2001","unstructured":"de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the ninth ACM SIGSOFT symposium on foundations of software engineering (FSE\u201901), Vienna, Austria, September 10\u201314, 2001. Assoc Comput Mach, New York, pp 109\u2013120"},{"key":"53_CR27","series-title":"Lecture notes in computer science","volume-title":"Compositionality: the significant difference, international symposium, COMPOS\u201997","year":"1998","unstructured":"de Roever WP, Langmaack H, Pnueli A (eds) (1998) Compositionality: the significant difference, international symposium, COMPOS\u201997, Bad Malente, Germany, September 8\u201312, 1997. Lecture notes in computer science, vol\u00a01536. Springer, Berlin. (Revised lectures)"},{"key":"53_CR28","volume-title":"A discipline of programming","author":"E Dijkstra","year":"1976","unstructured":"Dijkstra E (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs"},{"key":"53_CR29","doi-asserted-by":"crossref","unstructured":"Gheorghiu M, Giannakopoulou D, P\u0103s\u0103reanu CS (2007) Refining interface alphabets for compositional verification. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201907)","DOI":"10.1007\/978-3-540-71209-1_23"},{"key":"53_CR30","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/ASE.2002.1114984","volume-title":"Proceedings of the 17th international conference on automated software engineering (ASE\u201902)","author":"D Giannakopoulou","year":"2002","unstructured":"Giannakopoulou D, P\u0103s\u0103reanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of the 17th international conference on automated software engineering (ASE\u201902), Edinburgh, Scotland, September 23\u201327, 2002. IEEE Comput Soc, Los Alamitos, pp 3\u201312"},{"key":"53_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proceedings of the ninth international conference on computer aided verification (CAV\u201997)","author":"S Graf","year":"1997","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: Proceedings of the ninth international conference on computer aided verification (CAV\u201997), Haifa, Israel, June 22\u201325, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 72\u201383"},{"key":"53_CR32","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201902)","author":"A Groce","year":"2002","unstructured":"Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201902), Grenoble, France, April 8\u201312, 2002. Lecture notes in computer science, vol 2280. Springer, New York, pp 357\u2013370"},{"key":"53_CR33","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 on computer aided verification (CAV\u201907)","DOI":"10.1007\/978-3-540-73368-3_45"},{"key":"53_CR34","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Chechik M (2006) Why waste a perfectly good abstraction? In: Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems, pp 212\u2013226","DOI":"10.1007\/11691372_14"},{"key":"53_CR35","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Wei O, Chechik M (2006) Yasm: A software model-checker for verification and refutation. In: Proc of computer-aided verification, pp 170\u2013174","DOI":"10.1007\/11817963_18"},{"key":"53_CR36","series-title":"SIGPLAN notices","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201902)","author":"TA Henzinger","year":"2002","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201902). SIGPLAN notices, vol 37(1). Assoc Comput Mach, New York, pp 58\u201370"},{"key":"53_CR37","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading"},{"key":"53_CR38","unstructured":"Ivers J, Sharygina N (2004) Overview of ComForT: a model checking reasoning framework. In: CMU\/SEI-2004-TN-018"},{"issue":"4","key":"53_CR39","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596\u2013619","journal-title":"ACM Trans Program Lang Syst"},{"key":"53_CR40","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"RP Kurshan","year":"1995","unstructured":"Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton"},{"issue":"6","key":"53_CR41","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov BH, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811\u20131841","journal-title":"ACM Trans Program Lang Syst"},{"key":"53_CR42","unstructured":"MAGIC: http:\/\/www.cs.cmu.edu\/~chaki\/magic"},{"key":"53_CR43","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/978-3-540-24851-4_20","volume-title":"Proceedings of the 18th European conference on object-oriented programming (ECOOP\u201904)","author":"S McCamant","year":"2004","unstructured":"McCamant S, Ernst MD (2004) Early identification of incompatibilities in multi-component upgrades. In: Proceedings of the 18th European conference on object-oriented programming (ECOOP\u201904), Oslo, Norway, June 14\u201318, 2004. Lecture notes in computer science, vol 3086. Springer, New York, pp\u00a0440\u2013464"},{"key":"53_CR44","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Proceedings of the ninth international conference on computer aided verification (CAV\u201997)","author":"K McMillan","year":"1997","unstructured":"McMillan K (1997) A compositional rule for hardware design refinement. In: Proceedings of the ninth international conference on computer aided verification (CAV\u201997), Haifa, Israel, June 22\u201327, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 24\u201335"},{"issue":"4","key":"53_CR45","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417\u2013426","journal-title":"IEEE Trans Softw Eng"},{"key":"53_CR46","doi-asserted-by":"crossref","unstructured":"Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: 4th International symposium on automated technology for verification and analysis (ATVA\u201906), pp 170\u2013185","DOI":"10.1007\/11901914_15"},{"key":"53_CR47","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and models of concurrent systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli A (1985) 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":"53_CR48","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299\u2013347","journal-title":"Inf Comput"},{"key":"53_CR49","volume-title":"The theory and practice of concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall International, New York"},{"key":"53_CR50","doi-asserted-by":"crossref","unstructured":"Shoham S, Grumberg O (2004) Monotonic abstraction-refinement for CTL. In: Proceedings of the 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201904), pp 546\u2013560","DOI":"10.1007\/978-3-540-24730-2_40"},{"key":"53_CR51","doi-asserted-by":"crossref","unstructured":"Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Proceedings of the 19th international conference on computer aided verification (CAV\u201907)","DOI":"10.1007\/978-3-540-73368-3_8"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0053-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0053-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0053-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,9]],"date-time":"2021-09-09T12:35:12Z","timestamp":1631190912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0053-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,2]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["53"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0053-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5,2]]}}}