Model checking publications

• E.M. Clarke, O. Grumberg, H. Hirashi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Formal Methods in System Design, Volume 6/2, 1995. A preliminary version appeared in CHDL, 93.
• E.M. Clarke, R. Enders, T. Filkorn, and S. Jha, Exploiting Symmetry in Temporal Logic Model Checking, Formal Methods in System Design, Volume 9/2, 1996. A preliminary version appeared in CAV, 95.
• A. Browne, E.M. Clarke, S. Jha, D.E. Long, and W. Marrero, An Improved Algorithm for Evaluation of Fix-point Expressions, Theoretical Computer Science, Volume 178, 1997. A preliminary version appeared in CAV, 94.
• E.M. Clarke and S. Jha, Symmetry and Induction in Model Checking, Computer Science Today (Recent Trends and Developments), Special LNCS 1000-th volume, September 1995, Editor J. Van Leeuwen.
• E.M. Clarke, O. Grumberg, and S. Jha, Verifying Parameterized Networks, ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 19/5, 1997. A preliminary version appeared in CONCUR, 95.
• E.A. Emerson, S. Jha, and D. Peled, Combining Partial Order and Symmetry Reductions, Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 1997.
• S. Jha, M. Minea, Y. Lu, and E.M. Clarke, Equivalence Checking using Abstract BDDS, Proceedings of International Conference on Computer Design (ICCD), October 1997.
• E.M. Clarke, E.A. Emerson, S. Jha, and A.P. Sistla, Symmetry Reductions in Model Checking, Computer Aided Verification (CAV), 1998.
• E.M. Clarke, S. Jha, Y. Lu, and D. Wang, Abstract BDDs: a general methodology for using abstraction in Model Checking, 10-th IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), September 1999.
• S. Berezin, E. Clarke, S. Jha, and W. Marrero, Model checking algorithms for the mu-calculus, {\em to appear} in Proof, Language, and Interaction, Edited by G. Plotkin, MIT Press, 2000.
• E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstract Refinement, Computer Aided Verification (CAV), July 200.
• E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Progress on the State Explosion Problem in Model Checking, Dagstuhl 10-th Anniversary: Informatics 1-10 Years Back and 10 Years Ahead, LNCS volume 2000, Springer verlag, editor Riehnhard Wilhelm, 2001.
• P. Chauhan, E.M. Clarke, S. Jha, J.H. Kukula, H. Veith, and D. Wang, Using Combinatorial Optimization Methods for Quantification Scheduling, Correct Hardware Design and Verification Methods (CHARME), Sept 2001.
• P. Chauhan, E.M. Clarke, S. Jha, J.H. Kukula, H. Veith, and D. Wang, Non-linear Quantification Scheduling in Image Computation, ICCAD, 2001.
• E.M. Clarke, S. Jha, Y. Lu, H. Veith, Tree-like Counterexamples in Model Checking, Logic in Computer Science (LICS 2002), July 2002.
• T. Reps, S. Schwoon, and S. Jha, Weighted pushdown systems and their application to interprocedural dataflow analysis, 10th International Static Analysis Symposium (SAS) (June 11-13, 2003, San Diego, CA).
  To download the paper please click here.