{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:49Z","timestamp":1725511909269},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_24","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T18:56:34Z","timestamp":1183575394000},"page":"308-322","source":"Crossref","is-referenced-by-count":13,"title":["MAVEN: Modular Aspect Verification"],"prefix":"10.1007","author":[{"given":"Max","family":"Goldman","sequence":"first","affiliation":[]},{"given":"Shmuel","family":"Katz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"G. Kiczales","year":"2001","unstructured":"Kiczales, G., et al.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 327\u2013353. Springer, Heidelberg (2001)"},{"volume-title":"Aspect-Oriented Software Development","year":"2005","key":"24_CR2","unstructured":"Filman, R.E., et al. (eds.): Aspect-Oriented Software Development. Addison-Wesley, Boston (2005)"},{"issue":"5","key":"24_CR3","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1093\/comjnl\/46.5.529","volume":"46","author":"M. Sihman","year":"2003","unstructured":"Sihman, M., Katz, S.: Superimposition and aspect-oriented programming. BCS Computer Journal\u00a046(5), 529\u2013541 (2003)","journal-title":"BCS Computer Journal"},{"issue":"2-3","key":"24_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.tcs.2004.09.019","volume":"331","author":"E. Abraham","year":"2005","unstructured":"Abraham, E., et al.: An assertion-based proof system for multithreaded java. Theoretical Computer Science\u00a0331(2-3), 251\u2013290 (2005)","journal-title":"Theoretical Computer Science"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/11687061_4","volume-title":"Transactions on Aspect-Oriented Software Development I","author":"S. Katz","year":"2006","unstructured":"Katz, S.: Aspect categories and classes of temporal properties. In: Rashid, A., Aksit, M. (eds.) Transactions on Aspect-Oriented Software Development I. LNCS, vol.\u00a03880, pp. 106\u2013134. Springer, Heidelberg (2006)"},{"key":"24_CR6","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"24_CR7","unstructured":"Goldman, M.: Modular verification of aspects. MSc thesis, Technion \u2014 Israel Institute of Technology (2006), Available at http:\/\/www.cs.technion.ac.il\/Labs\/ssdl\/thesis\/finished\/2006\/max"},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/643603.643607","volume-title":"AOSD\u201903: Proc. 2nd Intl. Conf. on Aspect-oriented Software Development","author":"D. Sereni","year":"2003","unstructured":"Sereni, D., de Moor, O.: Static analysis of aspects. In: AOSD\u201903: Proc. 2nd Intl. Conf. on Aspect-oriented Software Development, pp. 30\u201339. ACM Press, New York (2003)"},{"key":"24_CR9","unstructured":"NuSMV: http:\/\/nusmv.irst.itc.it\/"},{"key":"24_CR10","unstructured":"Douence, R., S\u00fcdholt, M.: A model and a tool for Event-based Aspect-Oriented Programming (EAOP). TR 02\/11\/INFO, Ecole des Mines de Nantes (2002)"},{"key":"24_CR11","first-page":"137","volume-title":"Proc. SIGSOFT Conference on Foundations of Software Engineering, FSE\u201904","author":"S. Krishnamurthi","year":"2004","unstructured":"Krishnamurthi, S., Fisler, K., Greenberg, M.: Verifying aspect advice modularly. In: Proc. SIGSOFT Conference on Foundations of Software Engineering, FSE\u201904, pp. 137\u2013146. ACM, New York (2004)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","first-page":"389","volume-title":"Verification: Theory and Practice","author":"S. Katz","year":"2004","unstructured":"Katz, S., Sihman, M.: Aspect validation using model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 389\u2013411. Springer, Heidelberg (2004)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 - Concurrency Theory","author":"J. Hatcliff","year":"2001","unstructured":"Hatcliff, J., Dwyer, M.: Using the Bandera Tool Set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 39\u201358. Springer, Heidelberg (2001)"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4) (2000)","DOI":"10.1007\/s100090050043"},{"key":"24_CR15","unstructured":"Devereux, B.: Compositional reasoning about aspects using alternating-time logic. In: Proc. of Foundations of Aspect Languages Workshop, FOAL03 (2003)"},{"key":"24_CR16","unstructured":"Sipma, H.: A formal model for cross-cutting modular transition systems. In: Proc. of Foundations of Aspect Languages Workshop, FOAL03 (2003)"},{"issue":"3","key":"24_CR17","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR18","doi-asserted-by":"publisher","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., et al.: Parameterized interfaces for open system verification of product lines. In: Proc. 19th IEEE International Conference on Automated Software Engineering, ASE\u201904, Washington, DC, pp. 258\u2013267. IEEE Computer Society, Los Alamitos (2004)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Guelev, D.P., Ryan, M.D., Schobbens, P.Y.: Model-checking the preservation of temporal properties upon feature integration. In: Proc. 4th Intl. Workshop on Automated Verification of Critical Systems (AVoCS). Electronic Notes in Theoretical Computer Science, vol.\u00a0128(6), pp. 311\u2013324 (2004)","DOI":"10.1016\/j.entcs.2005.04.019"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:16:43Z","timestamp":1605745003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_24","relation":{},"subject":[]}}