{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T03:29:59Z","timestamp":1761708599914},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,11,1]],"date-time":"2010-11-01T00:00:00Z","timestamp":1288569600000},"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":[[2010,11]]},"DOI":"10.1007\/s10703-010-0101-1","type":"journal-article","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:57:56Z","timestamp":1288706276000},"page":"61-92","source":"Crossref","is-referenced-by-count":16,"title":["MAVEN: modular aspect verification and interference analysis"],"prefix":"10.1007","volume":"37","author":[{"given":"Max","family":"Goldman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emilia","family":"Katz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shmuel","family":"Katz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,11,3]]},"reference":[{"issue":"2\u20133","key":"101_CR1","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/j.tcs.2004.09.019","volume":"331","author":"E Abraham","year":"2005","unstructured":"Abraham E, de Boer F, de Roever W, Steffen M (2005) An assertion-based proof system for multithreaded Java. Theor Comput Sci 331(2\u20133):251\u2013290","journal-title":"Theor Comput Sci"},{"key":"101_CR2","volume-title":"Proc of foundations of aspect languages workshop (FOAL05)","author":"D Balzarotti","year":"2005","unstructured":"Balzarotti D, D\u2019Ursi A, Cavallaro L, Monga M (2005) Slicing AspectJ woven code. In: Proc of foundations of aspect languages workshop (FOAL05)"},{"key":"101_CR3","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/383845.383857","volume":"44","author":"L Bergmans","year":"2001","unstructured":"Bergmans L, Aksit M (2001) Composing crosscutting concerns using composition filters. CACM 44:51\u201357","journal-title":"CACM"},{"key":"101_CR4","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1109\/ASE.2004.1342743","volume-title":"Proc 19th IEEE international conference on automated software engineering (ASE\u201904)","author":"C Blundell","year":"2004","unstructured":"Blundell C, Fisler K, Krishnamurthi S, Hentenryck PV (2004) Parameterized interfaces for open system verification of product lines. In: Proc 19th IEEE international conference on automated software engineering (ASE\u201904), pp 258\u2013267"},{"key":"101_CR5","unstructured":"Common aspect proof environment (CAPE) (2008). http:\/\/www.cs.technion.ac.il\/~ssdl\/research\/cape"},{"key":"101_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"CAV\u201999","author":"A Cimatti","year":"1999","unstructured":"Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: CAV\u201999. Lecture notes in computer science, vol\u00a01633. Springer, Berlin, pp 495\u2013499. http:\/\/nusmv.itc.it"},{"key":"101_CR7","volume-title":"Model checking","author":"EM Clarke Jr.","year":"1999","unstructured":"Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"101_CR8","volume-title":"Proc of foundations of aspect languages workshop (FOAL03)","author":"B Devereux","year":"2003","unstructured":"Devereux B (2003) Compositional reasoning about aspects using alternating-time logic. In: Proc of foundations of aspect languages workshop (FOAL03)"},{"key":"101_CR9","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1145\/976270.976288","volume-title":"Proc of 3th intl conf on aspect-oriented software development (AOSD\u201904)","author":"R Douence","year":"2004","unstructured":"Douence R, Fradet P, Sudholt M (2004) Composition, reuse, and interaction analysis of stateful aspects. In: Proc of 3th intl conf on aspect-oriented software development (AOSD\u201904). ACM, New York, pp 141\u2013150"},{"issue":"6","key":"101_CR10","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/j.entcs.2005.04.019","volume":"128","author":"DP Guelev","year":"2004","unstructured":"Guelev DP, Ryan MD, Schobbens PY (2004) Model-checking the preservation of temporal properties upon feature integration. In: Proc 4th intl workshop on automated verification of critical systems (AVoCS\u201904). Electron Notes Theor Comput Sci 128(6):311\u2013324","journal-title":"Electron Notes Theor Comput Sci"},{"key":"101_CR11","volume-title":"Aspect-oriented software development","year":"2005","unstructured":"Filman RE, Elrad T, Clarke S, Ak\u015fit M (eds) (2005) Aspect-oriented software development. Addison-Wesley, Boston"},{"key":"101_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-540-71209-1_24","volume-title":"Proc of TACAS 2007","author":"M Goldman","year":"2007","unstructured":"Goldman M, Katz S (2007) MAVEN: Modular aspect verification. In: Proc of TACAS 2007. Lecture notes in computer science, vol 4424. Springer, Berlin, pp 308\u2013322"},{"issue":"3","key":"101_CR13","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"101_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"Proc 12th int conf on concurrency theory, CONCUR\u201901","author":"J Hatcliff","year":"2001","unstructured":"Hatcliff J, Dwyer M (2001) Using the Bandera Tool Set to model-check properties of concurrent Java software. In: Larsen KG, Nielsen M (eds) Proc 12th int conf on concurrency theory, CONCUR\u201901. Lecture notes in computer science, vol 2154. Springer, Berlin, pp 39\u201358"},{"key":"101_CR15","doi-asserted-by":"crossref","unstructured":"Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Int J Softw Tools Technol Transf (STTT) 2(4)","DOI":"10.1007\/s100090050043"},{"key":"101_CR16","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1145\/1218563.1218574","volume-title":"AOSD \u201907","author":"W Havinga","year":"2007","unstructured":"Havinga W, Nagy I, Bergmans L, Aksit M (2007) A graph-based approach to modeling and detecting composition conflicts related to introductions. In: AOSD \u201907. ACM, New York, pp 85\u201395"},{"key":"101_CR17","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/1394496.1394500","volume-title":"FOAL \u201908","author":"E Katz","year":"2008","unstructured":"Katz E, Katz S (2008) Incremental analysis of interference among aspects. In: FOAL \u201908. ACM, New York, pp 29\u201338"},{"key":"101_CR18","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/11687061_4","volume":"1","author":"S Katz","year":"2006","unstructured":"Katz S (2006) Aspect categories and classes of temporal properties. Trans Aspect-Oriented Softw Dev 1:106\u2013134. LNCS 3880","journal-title":"Trans Aspect-Oriented Softw Dev"},{"key":"101_CR19","unstructured":"Katz S, Faitelson D The common aspect proof environment. Submitted for publication, 2009. See http:\/\/www.cs.technion.ac.il\/~ssdl\/research\/cape\/index.html"},{"key":"101_CR20","series-title":"Lecture notes in computer science","first-page":"389","volume-title":"Proc of international symposium on verification","author":"S Katz","year":"2003","unstructured":"Katz S, Sihman M (2003) Aspect validation using model checking. In: Proc of international symposium on verification. Lecture notes in computer science, vol\u00a02772. Springer, Berlin, pp 389\u2013411"},{"key":"101_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"Proc ECOOP 2001","author":"G Kiczales","year":"2001","unstructured":"Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold WG (2001) An overview of AspectJ. In: Proc ECOOP 2001. Lecture notes in computer science, vol\u00a02072. Springer, Berlin, pp 327\u2013353. http:\/\/aspectj.org"},{"key":"101_CR22","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-02059-9_6","volume":"5","author":"J Kienzle","year":"2009","unstructured":"Kienzle J, Duala-Ekoko E, G\u00e9lineau S (2009) AspectOptima: A\u00a0case study on aspect dependencies and interactions. Trans Aspect-Oriented Softw Dev 5:187\u2013234","journal-title":"Trans Aspect-Oriented Softw Dev"},{"key":"101_CR23","doi-asserted-by":"crossref","unstructured":"Krishnamurthi S, Fisler K (2007) Foundations of incremental aspect model-checking. ACM Trans Softw Eng Methodol (TOSEM) 16(2)","DOI":"10.1145\/1217295.1217296"},{"key":"101_CR24","volume-title":"The temporal logic of reactive and concurrent systems: specification","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin"},{"key":"101_CR25","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inform 6:319\u2013340","journal-title":"Acta Inform"},{"key":"101_CR26","volume-title":"Proc of international conference on foundations of software engineering (FSE04)","author":"M Rinard","year":"2004","unstructured":"Rinard M, Salcianu A, Bugrara S (2004) A classification system and analysis for aspect-oriented programs. In: Proc of international conference on foundations of software engineering (FSE04)"},{"key":"101_CR27","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/643603.643607","volume-title":"AOSD","author":"D Sereni","year":"2003","unstructured":"Sereni D, de Moor O (2003) Static analysis of aspects. In: AOSD, pp 30\u201339"},{"issue":"5","key":"101_CR28","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1093\/comjnl\/46.5.529","volume":"46","author":"M Sihman","year":"2003","unstructured":"Sihman M, Katz S (2003) Superimposition and aspect-oriented programming. BCS Comput\u00a0J 46(5):529\u2013541","journal-title":"BCS Comput\u00a0J"},{"key":"101_CR29","volume-title":"Proc of foundations of aspect languages workshop (FOAL03)","author":"HB Sipma","year":"2003","unstructured":"Sipma HB (2003) A formal model for cross-cutting modular transition systems. In: Proc of foundations of aspect languages workshop (FOAL03)"},{"key":"101_CR30","volume-title":"Proc of foundations of aspect languages workshop (FOAL03)","author":"M Storzer","year":"2003","unstructured":"Storzer M, Krinke J (2003) Interference analysis for AspectJ. In: Proc of foundations of aspect languages workshop (FOAL03)"},{"key":"101_CR31","first-page":"95","volume-title":"Proc workshop on methods, models, and tools for fault tolerance, MeMoT\u201907","author":"N Weston","year":"2007","unstructured":"Weston N, Taiani F, Rashid A (2007) Interaction analysis for fault-tolerance in aspect-oriented programming. In: Proc workshop on methods, models, and tools for fault tolerance, MeMoT\u201907, pp 95\u2013102"},{"key":"101_CR32","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1109\/WPC.2002.1021346","volume-title":"IEEE international workshop on programming comprehension","author":"J Zhao","year":"2002","unstructured":"Zhao J (2002) Slicing aspect-oriented software. In: IEEE international workshop on programming comprehension, pp 251\u2013260"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0101-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0101-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0101-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T01:12:43Z","timestamp":1559783563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0101-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,11]]}},"alternative-id":["101"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0101-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,11]]}}}