My research deals with system design, modeling, and analysis. My research began with model checking and hardware verification at CMU. I also spent summers at Intel and Cadence investigating how to use formal methods to verify real world microprocessor designs. I am also interested in real-time systems, and how a model checker can be used to analyze the performance of these systems in addition to verifying correctness.

Currently, I am investigating how to model and verify computer security protocols including authentication protocols and electronic commerce protocols. With the growth such entities as "the Internet" and "the World Wide Web", both in the number of users and the number of organizations offering services, computer security and information survivability are quickly becoming extremely important and challenging areas. I hope to continue to make contributions in these fields.

I am also involved with the  Foundations of Programming Languages Group  here at DePaul.

Below is a list of my publications:
 
 

Publications

Modal Mu-Calculus

  • S. Berezin, E. Clarke, S. Jha, W. Marrero. Model Checking Algorithms for the mu-Calculus. Technical Report TR-CMU-CS-96-180, Carnegie Mellon University, September 1996. To appear in a book. ( Postscript)

  • D.E. Long, A. Browne, E.M. Clarke, S. Jha, W.R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Theoretical Computer Science, Volume 178, 1997. A preliminary version appeared in Proceedings of Computer-Aided Verification, 1994. ( Postscript)

    •

    Quantitative Real-Time Analysis

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems. In Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995. ( Postscript)

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Timing analysis of industrial real-time systems. In Workshop on Industrial Strength Formal Specification Techniques, 1995. ( Postscript)

  • S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994. ( Postscript)

    • Analyzing Security Protocols

  • E. Clarke, S. Jha, and W. Marrero. Partial order reductions for security protocol verification. Tools and Algorithms for the Construction and Analysis of Systems, 2000. ( Postscript)

  • E.M. Clarke and W. Marrero. Using formal methods for analyzing security. Information Survivability Workshop, 1998. ( HTML)

  • E.M. Clarke, and S. Jha, W. Marrero. A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols. Workshop on Formal Methods and Security Protocols, 1998. (Postscript)

  • E.M. Clarke, and S. Jha, W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998.(Postscript)

  • W. Marrero, E.M. Clarke, and S. Jha. Model checking for security protocols. In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. A Preliminary version appeared as Technical Report TR-CMU-CS-97-139, Carnegie Mellon University, May 1997. (Postscript)