Prof. Orna Grumberg

Prof. Orna Grumberg

Leumi Chair of Science

Contact information
Homepage:
http://www.cs.technion.ac.il/~orna/
Email:
orna[at]cs.technion.ac.il
Office:
620
Phone:
4327
Office Hours:
Monday, 16:00-17:00
Research interests
Computer-aided verification of software and hardware; Model checking; formal verification; Temporal logics; Modularity; Abstraction; Distributed model checking, SAT-based model checking, games, 3-valued logics.
Selected publications

GRUMBERG, O., and LONG, D.E., �Model checking and modular verification�, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, No. 3, pp. 843-871, 1994.

CLARKE, E.M., GRUMBERG, O., and LONG, D.E., �Model checking and abstraction�, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, No. 5, pp. 1512-1542, 1994.

KUPFERMAN, O., and GRUMBERG, O., �Branching time temporal logic and amorphous tree automata�, Information and Computation, Vol. 125, No. 1, pp. 62-69, 1996.

FIX, L., and GRUMBERG, O., �Verification of temporal properties�, Logic and Computation, Vol. 6, No, 3, pp. 343-362, 1996.

CLARKE, E.M., GRUMBERG, O., and HAMAGUCHI, H., �Another look at LTL model checking�, Formal Methods in System Design, Vol. 10, No. 1, 1997.

DAMS, D., GERTH, R., and GRUMBERG, O., �Abstract interpretation of reactive systems�, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 19, No. 2, 1997.

CLARKE, E.M., GRUMBERG, O., and JHA, S., "Verifying parameterized networks", ACM-TOPLAS, Vol. 19, No. 5, 1997.

LASTER, K., and GRUMBERG, O., "Modular model checking of software", International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), Lisbon, 1998.

KATZ, S., GEIST, D., GRUMBERG, O., "'Have I written enough properties?� - A method of comparison between specification and implementation'', CHARME'99, Bad Herrenalb, Germany, 1999.

CLARKE, E.M., GRUMBERG, O., JHA, S., LU, Y., and VEITH, H., �Computerexample-guided abstraction refinement�, International Conference on Computer Aided Verification (CAV�00), Chicago, 2000.

HEYMAN, T., GEIST, D., GRUMBERG, O., and SCHUSTER, A., �Achieving scalability in parallel reachability analysis of very large circuits�, International Conference on Computer Aided Verification (CAV�00), Chicago, 2000.

GRUMBERG, O., HEYMAN, T., and SCHUSTER, A., "Distributed model checking for mu-calculus", International Conference on Computer Aided Verification (CAV'01), July 2001.