CS home page
Shmuel Katz's Home Page
Department of Computer Science
Haifa 32000, Israel
- 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.
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.