Shmuel Katz's Home Page

Research Interests:

• Aspect-oriented software development, including verification methods for aspects, requirements engineering and traceability, design methods for aspects, and language support and analysis,
• Formal specification methods and connections among them, including issues of translations among specification notations and their effects on properties of models,
• Verification using convenient executions, including semi-automatic proofs built over a PVS proof environment, and model checking for scenario-based descriptions over SMV,
• Language constructs for distributed programming (superimposition, multiparty interactions, reconciliations),
• Self-stabilization and fault-tolerance.

• A list of most of my publications, including those about aspects, can be found in   publications.
• For copies of most of the papers, please send me an email request, however a few are online:
• "Specification and Verification of Event Detectors and Responses" by Cynthia Disenfeld and myself, in Modularity-AOSD 2013 (ACM Digital Library(
• "A Closer Look at Aspect Interference and Cooperation" by Cynthia Disenfeld and myself, in Modularity-AOSD 2012 (ACM Digital Library).
• "The Common Aspect Proof Environment" by myself and David Feitelson in the International Journal Software Tools Technology Transfer (STTT), vol. 14, pp. 41-52, 2012.
• "Making Aspects Natural: Events and Composition" by Christoph Bockish, Somayeh Malakuti, Mehmet Aksit, and myself, in Modularity-AOSD (ACM Digital Library), 2011.
• "Compositional Verification of Events and Observers" by Cynthia Disenfeld and myself, in FOAL 2011 (ACM Digital Library).
• "MAVEN: Modular Aspect Verification and Interference Analysis" by Max Goldman, Emilia Katz, and myself, in Formal Methods in System Design, vol. 37, 61-92, 2010.
• "User Queries for Specification Refinement Treating Shared Aspect Join Points" by Emilia Katz and myself, in SEFM 2010.
• "A Concern Architecture View for Aspect-Oriented Software Design" by Mika Katara and myself, in Software and Systems Modelling Journal (SoSyM), vol. 6, pp. 247-265, 2007.
• "Aspect Categories and Classes of Temporal Properties" , with very slight differences from the version that appears in TAOSD, volume 1, 2006.
• "A Mechanized proof Environment for the Convenient Computations proof Method" by Marcelo Glusman and myself, from the journal Formal Methods in System Design, vol. 23, pp. 115-142, 2003.
• "Superimpositions and Aspect-Oriented Programming" by Marcelo Sihman and myself, from the BCS Computer Journal, vol. 46, pp. 529-541, 2003.
• I am one of the project leaders of the Formal Verification project VeriTech to translate among specification and verification notations. A paper summarizing VeriTech and the idea of faithful translations among specification notations and properties is "VeriTech--A Framework for Translating Among Model Description Notations by Orna Grumberg and myself, in the International Journal on Software Tools for Technology Transfer (STTT), vol. 9, pp. 119-132, 2007, while an overview from the Integrated Formal Methods 2002 conference is available here .
• A copy of the slides used in my lectures at the Marktoberdorf summer school in 2002, on Convenient Computations and on Translating Among Models, is available here .
• I direct the Common Aspect Proof Environment (CAPE) project as part of the EU Network of Excellence AOSD-Europe. This project combines analysis and verification tools for aspects from Israel, Holland, France, England, and Germany into a common framework. It is available from the SSDL lab in our department.
• I was a co-Editor-in-Chief of the Springer Transactions on Aspect-Oriented Software Engineering (TAOSD), published as an LNCS journal subline, from 2009-2011, and serve on the editorial board. I have also been the head of the Systems and Software Development Lab (SSDL) in the Computer Science Department for several years, and the head of the departmental track in Software Engineering.