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 Chairing:

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.


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)

Introductory Lecture on Model Checking (3 hours) at National Taiwan University, 2009:
Introduction to Model Checking (3 hours)

Tutorials at ATVA 2009 (Macao):
2-Valued and 3-Valued Abstraction-Refinement Frameworks for Model Checking

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

Yael Meller, M.Sc. Thesis, January 2010:
Multi-Valued Abstraction and Compositional Model Checking

Avi Yadgar, Ph.d. Thesis, March 2010:
New Approaches to Model Checking and to 3-Valued Abstraction and Refinement

Yakir Vizel, Ph.d. Thesis, May 2014:
SAT-based Model Checking Using Interpolation and IC3

Yael Meller, Ph.d. Thesis, January 2016:
Model Checking Techniques for Behavioral UML Models

Karam Abd ElKader, M.Sc. Thesis, February 2016:
Automated Circular Assume-Guarantee Reasoning