FORMAL VERIFICATION GROUP WEBPAGE
 University of Utah, School of Computing
Salt Lake City, Utah 84112, USA

1  OVERVIEW

This is a research page for publications and artifacts created under Prof. Ganesh Gopalakrishnan’s guidance. Collaborators include Profs. Zvonimir Rakamarić, Robert M. Kirby, Martin Berzins, Mary Hall, and Matthew Might.

2  NEW

An exciting new Post-doctoral Fellow position has been advertised.

3  PROJECTS (including software)

We distribute the following tools associated with our projects:

4  CONCURRENCY EDUCATION

The The Center for Parallel Computing at Utah (CPU) maintains useful links on this topic. We are contributing toward the IEEE/NSF Technical Committee on Parallel Processing (TCPP) Curriculum on Parallelism and Concurrency.

5  PUBLICATIONS

2012:
2011:
2010:
2009:
2008:
2007:
2006:
2005:
2004:
2003:
2002:
2001:
2000:
1999:
1998:
1997:
1996:
1995:
1994:
1993:
1992:
1991:
1990:
1989:
1988:
1987:
1986:
1985:

5.1  DISSERTATIONS and THESES

  1. Scalable Formal Dynamic Verification of MPI Programs through Distributed Causality Tracking, Anh Vo, PhD thesis, March 2011 [.pdf] [.pptx]
  2. Formal Verification of Programs and Their Transformations, Guodong Li, PhD thesis, August 2010 [.pdf]
  3. Efficient Dynamic Verification Algorithms for MPI Applications, Sarvani Vakkalanka, PhD thesis, April 2010 [.pdf], slides:[.pptx]
  4. Multicore System Design with XUM: the Extensible Utah Multicore Project, Ben Meakin, MS thesis, April 2010 [.pdf]
  5. Verification of Hierarchical Cache Coherence Protocols for Futuristic Processors, Xiaofang Chen, PhD thesis, July 2008 [.pdf] [.bib]
  6. Efficient Dynamic Verification of Concurrent Programs, Yu Yang, PhD thesis, March 2009 [.pdf] [.bib]
  7. Formal Analysis for MPI-Based High Performance Computing Software, Robert Palmer, PhD thesis, August 2007 [.pdf]
  8. Efficient Protocol Verification Using Rule-Based Systems, Ritwik Bhattacharya, PhD thesis, March 2006 [.pdf]
  9. Formal Specification and Verification of Memory Consistency Models of Shared Memory Multiprocessors, Prosenjit Chaterjee, MS Thesis, 2002 [.pdf]
  10. Formal Verification of Parameterized Protocols on Branching Networks, Mike Jones, PhD Thesis, 2001 [.pdf]
  11. Systematic Verification of Pipelined Processors, Ravi Hosabettu, PhD Thesis, 2000 [.pdf]
  12. Test Model Checking Approach to Verification of Formal Memory Models, Rajnish Ghughal, MS Thesis, 1999 [.pdf]
  13. Design and Verification Methods for Shared Memory Systems, Ratan Nalumasu, PhD Thesis, 1999 [.pdf]

5.2  BOOKS

  1. Ganesh Gopalakrishnan and Shaz Qadeer: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011 (LNCS 6806).
  2. Ganesh Gopalakrishnan, “Computation Engineering: applied automata theory and logic” (505 pages). Springer, ISBN 0-387-24418-2, 2006.
  3. Ganesh Gopalakrishnan and Phillip Windley, editors. Formal Methods in Computer-Aided Design. Proceedings of the 2nd International Conference, FMCAD ’98. Lecture Notes in Computer Science 1522, Springer-Verlag, 1998, 538 pages. ISSN 0302-9743.
  4. Slind, Konrad; Bunker, Annette; Gopalakrishnan, Ganesh C. (Eds.) Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Lecture Notes in Computer Science, Vol. 3223. ISBN: 3-540-23017-3o

5.3  JOURNALS

6  Director / Chairmanship

7  Other Software

  1. Yu Yang’s ZChaff to Ocaml Interface

    An interface to manipulate Zchaff from within Ocaml was written by Yu Yang. It’s here: Ocaml/SAT interface.

  2. Software related to Shared Memory Models

    We have been active in developing prototype software that helps explore shared memory consistency issues (also known as memory ordering issues, or formal memory models). A collection of tools appears here.

    1. MultiProcessor Execution Checker (MPEC)

      This is our SAT-based Intel Itanium execution validator tool, MPEC. Originally written by Prof. Ganesh Gopalakrishnan, the code was significantly extended by Yu Yang, PhD student in our group. The use of unsat cores for counterexample display was conceived by, and initially prototyped by Hemanthkumar Sivaraj. Yu Yang wrote the present version. A brief HOL specification (courtesy: Konrad Slind) that describes our Itanium memory model definition is here.

      This tool, sans the unsat core part, is the basis of our CAV 2004 paper. The unsat core part is expected to be part of a journal paper under construction.

    2. NemosFinder - Prolog-based MP execution checker

      A collection of Constraint Prolog routines were deveoped by our former student Yue “Jason” Yang, as part of his PhD, to express various memory models in a non-operational constraint based manner. These descriptions are “nicely organized” as a collection of clauses that constrain the pair-wise orderings among the memory instruction “tuples” (a design used also in MPEC). This is the basis for one of Yang’s papers.

    3. UMMChecker - Enumerative execution checker based on Murphi A collection of Murphi models were deveoped by our former student Yue “Jason” Yang, as part of his PhD, to express various memory models in an operational rule-based manner. These rules adhere to a general design paradigm called “Uniform Memory Model” by Dr. Yang. This is the basis for one of Yang’s papers.
  3. Model Checkers of the Promela/SPIN Genre

    We used to do many things in the area of Promela/SPIN-like systems. Most such efforts did not pan out as we could really not understand the internals of SPIN sufficiently.

    1. MP Checker based on Promela

      A Promela based checker of memory ordering rules, written by our former MS student Prosenjit Chatterjee. This forms the basis of our ICCD (2001) paper. It allows MP rules to be configured.

    2. PV: A SPIN-like Verifier The main reason for creating PV was to demonstrate our two-phase partial order reduction algorithm concretely. This was the basis of our FMSD 2002 paper.
    3. Eddy_SPIN: Distributed Verifier A distributed version of the SPIN model checker, developed at Utah with MPI. We refactored SPIN so as to have a next-state generator, given any state. We then grafted in the Eddy architecture (separate threads for communication and computation; see Eddy Murphi above. This tool cost us a lot of grief.
      • A race condition took very long to track down. This was because of the communication thread and computation thread accessing the hash-table directly. We avoided this race by having locally generated next states that are meant for the local node consumed via the consumption queue which receives msgs from other nodes (previously we had tried to directly insert these states into the local hash table). The tool finally worked, giving us exact state count matches. However it proved to be very slow, and due to the simplicity of our refactoring effort, had huge state vectors. We then implemented a disk-based buffer for the local queue of BFS states (did not help). This version is offered “as is” for anyone wanting to further our code path (kindly drop us a line if you do so).
      • We did not attempt liveness or PO reductions, although our PDMC 2001 experience tells us that we could incorporate our two-phase PO reduction algorithm. In fact, this algorithm is very well suited for distributed implementation, because it does not employ a stack proviso (which is a serialization point; we don’t know how to avoid that being the case).

8  AFFILIATED FACULTY

School of Computing:
Electrical and Computer Engineering:

9  STUDENTS AND ALUMNI

ALUMNI

10  SUPPORT

Supported in part by

Our research is primarily supported by NSF with additional support provided by SRC and the Department of Energy under the SUPER project.

This document was translated from LATEX by HEVEA.