Mugshot Amir Pnueli

Research interests

My main research interests are Semantics and Verification of Concurrent Programs, Temporal Logic, Logics of Programs, Specification and Non Procedural languages, Automatic Proof Methods for Correctness, Verification and Synthesis of Programs, Theory of Computation, Schemata Theory and its relations to Formal Languages Theory, Specification, Verification and Systematic development of Real-Time and Hybrid Systems. Refinement, using Temporal Logic. Compositional verification of reactive, real-time, and hybrid systems. Synthesis of such systems.


Some recent papers are available for downloading as technical reports, (a service maintained by the department). A full list of publications is also available. There is a list of invited talks, and a list of the books I am, or have been, involved in.

Additional information

Some additional information can be found in a short biography. The department can be reached at wisdom, and the institute at weizmann.


Spring 1999: Topics in Verification: Infinite-State Systems

Spring 2000: Verification of Reactive, Real-Time, and Hybrid Systems Part II: Real-Time and Hybrid Systems

Spring 2001: Verification of Reactive Systems

Holon Course Spring 2001: Parallel and Concurrent Systems

Spring 2002: Deductive Verification of Reactive Systems