Model Checking and Temporal Reasoning Group at UTCS

This is the homepage for Model Checking at Computer Sciences Department at The University of Texas at Austin.

General Information:

The Model Checking group, under the supervision of Professor E. Allen Emerson, studies the specification, verification and synthesis of concurrent, reactive systems.

Members:

Alumni:

Kedar Namjoshi (alumni)

Previous and Current Research Topics:

  • Model Checking
  • CTL (Computation Tree Logic)
  • Mu-Calculus
  • Complexity and expressiveness of temporal logics
  • Program synthesis from branching time temporal logic specifications
  • Automata on infinite objects and games
  • Classes:

  • CS353: Elements of the Theory of Computation
  • CS395T: Model Checking
  • Others:

  • The World Wide Web Virtual Library: Formal Methods
  • Publications Page


    Contact: trg@cs.utexas.edu