{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:42:24Z","timestamp":1704454944641},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,12,5]],"date-time":"2007-12-05T00:00:00Z","timestamp":1196812800000},"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-007-0042-5","type":"journal-article","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T16:11:49Z","timestamp":1196957509000},"page":"267-284","source":"Crossref","is-referenced-by-count":10,"title":["Three optimizations for Assume\u2013Guarantee reasoning with L*"],"prefix":"10.1007","volume":"32","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,12,5]]},"reference":[{"key":"42_CR1","first-page":"346","volume-title":"Proceedings of the 5th international symposium on the theory and applications of satisfiability testing (SAT \u201902)","author":"F Aloul","year":"2002","unstructured":"Aloul F, Ramani A, Markov I, Sakallah K (2002) PBS: A backtrack search pseudo-boolean solver and optimizer. In: Proceedings of the 5th international symposium on the theory and applications of satisfiability testing (SAT \u201902), Cincinnati, OH, May 6\u20139, 2002. University of Cincinnati, Cincinnati, pp\u00a0346\u2013353. http:\/\/gauss.ececs.uc.edu\/Conferences\/SAT2002\/sat2002list.html"},{"key":"42_CR2","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/1040305.1040314","volume-title":"Popl05","author":"R Alur","year":"2005","unstructured":"Alur R, Cerny P, Gupta G, Madhusudan P, Nam W, Srivastava A (2005) Synthesis of interface specifications for Java classes. In: Palsberg J, Abadi M (eds) Popl05, Long Beach, CA, January 12\u201314, 2005. Association for Computing Machinery, New York, pp\u00a098\u2013109"},{"key":"42_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Proceedings of the 17th international conference on computer aided verification (CAV \u201905)","author":"R Alur","year":"2005","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV \u201905), Edinburgh, Scotland, July 6\u201310, 2005. Lecture notes in computer science, vol\u00a03576. Springer, New York, pp\u00a0548\u2013562"},{"issue":"2","key":"42_CR4","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":"42_CR5","unstructured":"Ball T, Rajamani SK (2002) Generating abstract explanations of spurious counterexamples in C programs. Technical report MSR-TR-2002-09, Microsoft Research, Redmond, Washington, USA, January 2002"},{"key":"42_CR6","first-page":"14","volume-title":"Proceedings of the 2nd workshop on specification and verification of component based systems (SAVCBS \u201903)","author":"H Barringer","year":"2003","unstructured":"Barringer H, Giannakopoulou D, P\u0103s\u0103reanu CS (2003) Proof rules for automated compositional verification. In: Proceedings of the 2nd workshop on specification and verification of component based systems (SAVCBS \u201903), Helsinki, Finland, September 1\u20132, 2003. Iowa State University, Ames, pp\u00a014\u201321"},{"key":"42_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Proceedings of the 17th international conference on computer aided verification (CAV \u201905)","author":"S Chaki","year":"2005","unstructured":"Chaki S, Clarke EM, Sinha N, Thati P (2005) Automated Assume\u2013Guarantee reasoning for simulation conformance. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV \u201905), Edinburgh, Scotland, July 2005. Lecture notes in computer science, vol 3576. Springer, Berlin, pp\u00a0534\u2013547"},{"key":"42_CR8","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: Etessami\u00a0K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV \u201905), Edinburgh, Scotland, July 6\u201310, 2005. Lecture notes in computer science, vol\u00a03576. Springer, New York, pp\u00a0164\u2013169"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"Chaki S, Sinha N (2006) Assume\u2013Guarantee reasoning for deadlock. In: Proc. of FMCAD, 2006","DOI":"10.1109\/FMCAD.2006.8"},{"key":"42_CR10","series-title":"Lecture notes in computer science","first-page":"276","volume-title":"Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201907)","author":"S Chaki","year":"2006","unstructured":"Chaki S, Strichman O (2006) Optimized L* for Assume\u2013Guarantee reasoning. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201907), Braga, Portugal, March 24\u2013April 1, 2007. Lecture notes in computer science, vol\u00a04424. Springer, New York, pp\u00a0276\u2013291"},{"issue":"5","key":"42_CR11","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J\u00a0Assoc Comput Mach 50(5):752\u2013794","journal-title":"J\u00a0Assoc Comput Mach"},{"key":"42_CR12","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 9th 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: Garavel H, Hatcliff J (eds) Proceedings of the 9th 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\u00a02619. Springer, New York, pp\u00a0331\u2013346"},{"key":"42_CR13","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/302405.302467","volume-title":"Proceedings of the 21st international conference on software engineering (ICSE \u201999)","author":"MD Ernst","year":"1999","unstructured":"Ernst MD, Cockrell J, Griswold WG, Notkin D (1999) Dynamically discovering likely program invariants to support program evolution. In: Proceedings of the 21st international conference on software engineering (ICSE \u201999), Los Angeles, CA, May 1999. IEEE Computer Society, Los Alamitos, pp\u00a0213\u2013224"},{"key":"42_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-540-71209-1_23","volume-title":"Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201907)","author":"M Gheorghiu","year":"2007","unstructured":"Gheorghiu M, Giannakopoulou D, P\u0103s\u0103reanu CS (2007) Refining interface alphabets for compositional verification. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS \u201907), Braga, Portugal, March 24\u2013April 1, 2007. Lecture notes in computer science, vol\u00a04424. Springer, New York, pp\u00a0292\u2013307"},{"key":"42_CR15","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 Computer Society, Los Alamitos, pp\u00a03\u201312"},{"key":"42_CR16","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: Katoen J-P, Stevens P (eds) 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\u00a0357\u2013370"},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Habermehl P, Vojnar T (2005) Regular model checking using inference of regular languages. In: Proceedings of the 6th international workshop on verification of infinite-state systems (INFINITY \u201904). Electronic notes in theoretical computer science, vol\u00a0138(3), pp\u00a021\u201336","DOI":"10.1016\/j.entcs.2005.01.044"},{"issue":"3","key":"42_CR18","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1016\/S0022-0000(74)80044-9","volume":"9","author":"D Johnson","year":"1974","unstructured":"Johnson D (1974) Approximation algorithms for combinatorial problems. J\u00a0Comput Syst Sci 9(3):256\u2013278","journal-title":"J\u00a0Comput Syst Sci"},{"key":"42_CR19","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: Mason REA (ed) Proceedings of the 9th IFIP world congress. Information Processing, vol\u00a083, Paris, France, September 1983, pp\u00a0321\u2013332"},{"key":"42_CR20","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"RP Kurshan","year":"1994","unstructured":"Kurshan RP (1994) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton"},{"issue":"4","key":"42_CR21","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 Soft Eng 7(4):417\u2013426","journal-title":"IEEE Trans Soft Eng"},{"key":"42_CR22","series-title":"IFIP conference proceedings","first-page":"225","volume-title":"Proceedings of the joint international conference on formal description techniques for distributed systems and communication protocols (FORTE \u201999)","author":"D Peled","year":"1999","unstructured":"Peled D, Vardi MY, Yannakakis M (1999) Black box checking. In: Wu J, Chanson ST, Gao Q (eds) Proceedings of the joint international conference on formal description techniques for distributed systems and communication protocols (FORTE \u201999), Beijing, China, October 1999. IFIP conference proceedings, vol 156. Kluwer Academic, Dordrecht, pp\u00a0225\u2013240"},{"key":"42_CR23","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume":"13","author":"A Pnueli","year":"1985","unstructured":"Pnueli A (1985) In transition from global to modular temporal reasoning about programs. Logics Models Concurr Syst 13:123\u2013144","journal-title":"Logics Models Concurr Syst"},{"issue":"2","key":"42_CR24","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"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0042-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-007-0042-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0042-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T04:48:59Z","timestamp":1684126139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-007-0042-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,5]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["42"],"URL":"https:\/\/doi.org\/10.1007\/s10703-007-0042-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12,5]]}}}