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 papers from my work on aspect-oriented design and verification is here .
• A list of earlier publications can be found in   publications.
• For copies of most of the papers, please send me an email request, however a few are online, see below..
• A postscript copy of the paper "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, is available here .
• The article "Aspect Categories and Classes of Temporal Properties" is available in a preliminary version here, with very slight differences from the version that appears in TAOSD, volume 1, 2006.
• The article "Superimpositions and Aspect-Oriented Programming" by Marcelo Sihman and myself, from the BCS Computer Journal, vol. 46, pp. 529-541, 2003, is available here .
• I am one of the project leaders of the Formal Verification project VeriTech to translate among specification and verification notations. An early paper (in Postscript) explaining VeriTech and the idea of faithful translations among specification notations and properties can be found here , 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 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.