Research

A1.

Deductive verification of hardware designs. This work started as a cooperation with Prof. W. Damm and continues as a research project of T. Arons and S. Ruah, maintaining collaboration with the team of W. Damm at Oldenburg.

A2.

Translation validation. Methods and tools to verify that a run of a compiler produces a correct translation of the source program. Research conducted by O. Shtrichman and Y. Rodeh with contributions by A. Etin. New trends in this area consider validation of optimizing compilers with emphasis on architecture-targeted optimization.

A3.

Optimizations of SAT algorithms for Bounded Model Checking.

A4.

Object Oriented specification and system development methods. Research conducted by D. Harel, and H. Kugler, in collaboration with W. Damm and O. Kupferman.

A5.

Aesthetic and Effective graph layouts, with application to the presentation of visual specifications. Research conducted by D. Harel and Y. Koren.

A6.

Methods and tools for verifying parameterized systems. Research conducted by T. Arons, D. Fisman, N. Piterman, A. Pnueli, S. Ruah, and E. Shahar.

A7.

model checking with full fairness, Abstraction, and Composition. Research conducted by Y. Kesten and A. Pnueli.

A8.

Hybrid and timed systems, Verification and Synthesis. Research conducted by A. Pnueli and Verimag (Grenoble) scientists O. Maler and J. Sifakis.

A9.

Compilation satisfying real-time requirements. Research conducted by A. Pnueli and Georgia-Tech scientist K. Palem.

A10.

Application of CS Formal Methods to the Modeling and Verification of Biological Systems. Research conducted by D. Harel, S. Efroni, N. Kam, and A. Pnueli in collaboration with I.R. Cohen of the Department of Immunology, WIS.

A11.

Expressibility issues in Temporal Logics and Automata. Research conducted by Nir Piterman in collaboration with Orna Kupferman and Moshe Vardi.

A12.

Derivation of requirement specification by Play-In scenarios. Research conducted by R. Marelly and D. Harel.

Additional details about these research activities can be found in research.

Dept. of Computer Science and Applied Math The Weizmann Institute of Science Rehovot 76100, Israel TelePhone: +972-8-934-3434 Telefax: +972-8-934-4122 To comment on this service, send feedback to the Nir Piterman