Orna Grumberg's Home Page

TECHNION - Israel Institute of Technology
Computer Science Department
Technion City - Haifa 32000 - Israel
Phones: Ofc: +972-4-829-4327 Sec: +972-4-8294314 Res: +972-4-8257568
Fax: +972-4-829-4353
Email: orna@cs.technion.ac.il
Additional information

Research Interest:

Conference Organization and Committees:

Together with Helmut Veith, I organized the workshop on 25 Years of Model Checking (25MC), held as part of CAV'06, in Seattle, on August 16, 2006.
The proceedings appears in LNCS 5000
.

Together with Michael Huth, I co-chaired the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), held in Braga, Portugal, March 26-30, 2007.

Special Courses:

Together with Dr. Limor Fix from Intel, Haifa, I taught during the first semester of 2000-2001 the course
Efficient Solutions for the Propositional SAT Problem and Their Application to Formal Verification

Together with Dr. Karen Yorav, Galileo Technology, Haifa, I taught during the second semester of 2002 a course on parallel and distributed model checking.

Presentations:

At the NATO Summer School, Marktoberdorf, 2001:
Model Checking, Abstractions and Reductions

At the CONCUR'02 workshop on Parallel and Distributed Model Checking (PDMC 2002):
Tutorial on Directions in Parallel and Distributed Model Checking

At the NATO Summer School, Marktoberdorf, 2007:
Automatic Refinement and Vacuity Detection in Symbolic Trajectory Evaluation (STE)

Students' Theses:

For my information, please mail to orna 'at' cs.technion.ac.il if you download a thesis.

Karen Yorav, Ph.D. Thesis, June 2000:
Exploiting Syntactic Structure for Automatic Verification

Sagi Katz, M.Sc. Thesis, December 2001:
Techniques for Increasing Coverage of Formal Verification

Doron Bustan, Ph.d. Thesis, July 2002:
Equivalence-Based Reductions and Checking for Preorders

Sharon Keidar-Barner, M.Sc. Thesis, December 2002:
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking

Sharon Shoham, M.Sc. Thesis, November 2003:
A Game-Based Framework for CTL Counterexamples and Abstraction-Refinement

Tamir Heyman, Ph.d. Thesis, December 2003:
Distributed Symbolic Model Checking

Avi Yadgar, M.Sc. Thesis, March 2004:
Memory Efficient ALL-Solutions SAT solver and its Application for Reachability Analysis

Alon Flaisher, M.Sc. Thesis, August 2004:
Enhanced Vacuity Detection in Linear Temporal Logic

Nili Ifergan, M.Sc. Thesis, July 2005:
Achieving High-Speedups in Distributed Reachability Analysis through Asynchronous Computation

Rachel Tzoref, M.Sc. Thesis, June 2006:
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation

Rotem Oshman, M.Sc. Thesis, July 2008:
Bounded Model-Checking for Branching-Time Logic

Sharon Shoham, Ph.d. Thesis, January 2009:
Abstraction-Refinement and Modularity in Mu-Calculus Model Checking

Publications: