פרופ' ארנה גרימברג

פרופ' ארנה גרימברג

Leumi Chair of Science

יצירת קשר
דף בית:
http://www.cs.technion.ac.il/~orna/
דואר אלקטרוני:
orna[at]cs.technion.ac.il
משרד:
620
טלפון:
4327
שעות קבלה:
Tuesday, 16:00-17:00
תחומי עניין במחקר
אימות בעזרת מחשב של חומרה ותוכנה; מודולריות ואבסטרקציה; לוגיקה טמפורלית; בדיקת מודל מקבילית, שקילויות ויחסי סדר בין מבנים, אימות מונחה-SAT, משחקים.
פרסומים נבחרים

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.