FORMAL VERIFICATION GROUP WEBPAGE
 UNIVERSITY OF UTAH
SCHOOL OF COMPUTING

Contents

1  OVERVIEW

This is Prof. Ganesh Gopalakrishnan’s research group. We work on formally specifying and formally verifying concurrent systems. Our current work includes

2  NEW

Please visit our new tutorial site for ISP:

ISP Tutorial Page

3  PROJECTS

3.1  MPI Formal Verification

We are very excited to have developed the first (as far as we know) push-button dynamic formal verifier with completeness guarantees for MPI programs called ISP ISP is freely downloadable, runs with five different MPI libraries (MPICH2, OpenMPI, Microsoft MPI, MVAPICH, and IBM MPI) and finds deadlocks, MPI object leaks, and local assertion violations in MPI C programs (Fortran porting underway). Tutorial Webpage

3.2  Multi-core Communications API (MCAPI)

Message passing is going to make a resurgence in concurrent systems - already evidenced by the MCAPI API created by the Multicore Association (see the MCAPI website). We are building the first (as far as we know) dynamic verifier for MCAPI user applications. A paper accepted at FMCAD 2009 [.pdf]

3.3  Thread Verification

We have developed the first publicly available DPOR based dynamic verifier for Pthread/C programs called Inspect. We provide the full Inspect release plus benchmarks for your use. See under "Software" in the main buttons of the group page.

3.4  Parallel Model Checking

We have revived Eddy Murphi - a robust Murphi based distributed model checker. Eddy Murphi is now proven robust by releasing to Intel - it recently explored 10 billion states (400 billion transitions) on one of their large models on 37 nodes in slightly over a day. You can download Eddy Murphi from HERE.

4  CONCURRENCY EDUCATION

Concurrency Education website

4.1  BENCHMARKS

These are benchmarks beyond those provided with our papers. See Section 5 for additional benchmarks.

5  PUBLICATIONS

5.1  CONFERENCES

5.1.1  MPI Verification

  1. Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, “Reduced Execution Semantics of MPI: From theory to practice,” FM 2009, pgs 724–740, November 2009
    [.pdf] [.bib]
  2. Anh Vo, Sarvani Vakkalanka, Jason Williams, Ganesh Gopalakrishnan, Robert M. Kirby and Rajeev Thakur, “Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-Determinism,” EuroPVM/MPI, September 2009, pgs 271–281
    [.pdf] [.bib]
  3. Sriram Aananthakrishnan, Michael DeLisi, Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, “How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations, ” EuroPVM/MPI, September 2009, pgs 261-270
    [.pdf] [.bib]
  4. Sarvani Vakkalanka, Grzegorz Szubzda, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, “Satic-analysis Assisted Dynamic Verification to Efficiently Handle Waitany Non-determinism,” EuroPVM/MPI, September 2009, pgs 329–330
    [.pdf] [.bib]
  5. Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, “Formal Verification of Practical MPI Programs,” PPoPP 2009, Raleigh, North Carolina
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  6. Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, “Scheduling Considerations for Building Dynamic Verification Tools for MPI,” Parallel and Distributed Systems - Testing and Debugging (PADTAD-VI), Seattle, WA, July, 2008.
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  7. Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “Implementing Efficient Dynamic Formal Verification Methods for MPI Programs,” Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI), Dublin, Ireland, 2008, LNCS 5205, pp. 248-256.
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  8. Subodh Sharma, Sarvani Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “ A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs,” Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI), Dublin, Ireland, 2008, LNCS 5205, pp. 265-273.
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  9. Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby, “Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings,” Computer Aided Verification (CAV 2008), pp. 66-79, LNCS 5123. [.pdf] [.bib] [Benchmark Programs of This Paper]
  10. Sarvani Vakkalanka, Subodh V. Sharma, Ganesh Gopalakrishnan, and Robert M. Kirby, “ISP: A Tool for Model Checking MPI Programs,” Principles and Practices of Parallel Programming (PPoPP), Salt Lake City, February 2008, pp. 285-286.
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  11. Guodong Li, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, “Formal Specification of the MPI-2.0 Standard in TLA+,” Principles and Practices of Parallel Programming (PPoPP), Salt Lake City, February 2008, pp. 283-284.
    [.pdf] [.bib] [MPI 2.0 Formal Specification TAR and PDF files]
  12. Robert Palmer, Ganesh Gopalakrishnan, and Robert M. Kirby, “Semantics Driven Dynamic Partial-Order Reduction of MPI-based Parallel Programs,” Parallel and Distributed Systems - Testing and Debugging (PADTAD-V), London, England, July, year = 2007. Best Paper Award.
    [.pdf] [.bib] [.ppt]
  13. Salman Pervez, Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “Practical Model Checking Methods for Verifying Correctness of MPI Programs,” Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI), Paris, 344–353, LNCS 4757, France, September 30 - October 3, 2007.
    [.pdf] [.bib] [.ppt]
  14. Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, and Robert M. Kirby, “An Approach to Formalization and Analysis of Message Passing Libraries,” Formal Methods for Industry Critical Systems (FMICS), Berlin, S. Leue and P. Merino (editors), pp. 164-181, July 2008. (The European Association of Software Science and Technology (EASST) Best Paper Award.)
    [.pdf] [.bib] [.ppt] [Verification Environment in MS Visual Studio]
  15. Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “Formal Verification of Programs that use MPI One-sided Communication,” (One of three outstanding papers,) Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI), Bonn, Germany, 2006, LNCS 4192, 30-39.
    [.pdf] [.bib] [.ppt] [Byte-range Locking Protocol Models of This Paper in Promela]
  16. Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, and Robert M. Kirby, “Gauss: A Framework for Verifying Scientific Computing Software,” Workshop on Software Model Checking, Edinburgh, 2005 (a post CAV05 workshop). Paper included in the Electronic Notes on Theoretical Computer Science (ENTCS) No. 953.
    [.pdf] [.bib]
  17. Ganesh Gopalakrishnan and Robert M. Kirby, “Toward Reliable and Efficient Message Passing Software Through Formal Analysis,” An IPDPS 2006 workshop on Next-Generation Systems, 2006, Athens, Greece. Organizer: Frederica Darema (NSF).
    [.pdf]

5.1.2  MCAPI Verification (Multi-Core Communications API)

  1. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, “Dynamic Verification of Multicore Communication Applictions in MCAPI,” HLDVT 2009, November, San Francisco, CA
    [.pdf] [.bib]
  2. Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt, “MCC - A runtime verification tool for MCAPI user applications,” FMCAD 2009, November 2009
    [.pdf] [.bib]
  3. Subodh Sharma, Ganesh Gopalakrishnan, “Formal Verification of MCAPI Applications Using the Dynamic Verification tool MCC,” SRC Techcon, 2009, September, Austin, TX
    [.pdf] [.bib]

5.1.3  Thread Level Verification

  1. Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang, “Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis,” SPIN (279-295), June 2009, Grenoble, France
    [.pptx]
  2. Chao Wang, Yu Yang, Aarti Gupta, and Ganesh Gopalakrishnan, “Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions,” ATVA 2008, pp. 126-140, LNCS 5311.
    [.pdf] [.bib]
  3. Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby, “Efficient Stateful Dynamic Partial Order Reduction,” Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, August 2008, LNCS , pp. 288-305.
    [.pdf] [.bib] [Benchmark Programs of This Paper]
  4. Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby, “Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software,” Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, 58-75, LNCS 4595.
    [.pdf] [.bib] [.ppt]
  5. Robert Palmer, Ganesh Gopalakrishnan and Mike Kirby, “Formal Specification and Verification Using +CAL: An Experience Report,” Verify’06 workshop (Post FLoC 2006), Seattle, Aug 15, 2006.
    [.pdf] [.bib]
  6. Ritwik Bhattacharya, Steven M. German, and Ganesh Gopalakrishnan, “Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications,” Model Checking Software (13th International SPIN Workshop), Vienna, Austria, 2006, LNCS 3925, 252-270.
    [.pdf] [.bib] [Ritwik’s Partial-order Enabled Murphi (POeM)]
  7. Ritwik Bhattacharya, Steven M. German, and Ganesh Gopalakrishnan, “Symbolic Partial Order Reduction for Rule Based Transition Systems,” CHARME 2005, LNCS 2144, 332-335.
    [.pdf] [.bib]
  8. Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, “Specifying Java Thread Semantics using a Uniform Memory Model,” Joint ACM Java Grande - ISCOPE Conference, pp.192-201, ISBN:1-58113-599-8, 2002.
    [.pdf] [.bib] [Jason’s Directory]
  9. Robert Palmer and Ganesh Gopalakrishnan, “The Parallel PV Model-Checker,” International Workshop on Parallel and Distributed Model Checking (PDMC’02), Brno, Czech Republic, August, 2002.
  10. Jason Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, “Analyzing the CRF Java Memory Model with Murphi,” Workshop on Software Model-checking, Paris, France, July 2001. [Jason’s Directory]
  11. Jason Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, “Analyzing the CRF Java Memory Model with Murphi,” Asia Pacific Software Engineering Conference. Macau, 2001. [Jason’s Directory]
  12. Ratan Nalumasu and Ganesh Gopalakrishnan, “PV: an Explicit Enumeration Model-checker,” Formal Methods in Computer Aided Design, Second International Conference, FMCAD’98, Palo Alto, CA, USA, Nov 1998, Proceedings. Ganesh Gopalakrishnan and Phillip Windley (editors). Springer-Verlag LNCS 1522. pp. 523-528.
    [Ratan’s Directory] [Dissertation]
  13. Ratan Nalumasu and Ganesh Gopalakrishnan, “PV: A Model-checker for Verifying LTL-X Properties,” Lfm97: Fourth NASA LaRC Formal Methods Workshop, 10-12 September 1997, Hampton, Virginia.
    [Ratan’s Directory] [Dissertation]
  14. Ratan Nalumasu and Ganesh Gopalakrishnan, “A New Partial Order Reduction Algorithm for Concurrent System Verification,” Proceedings of the 1997 Computer Hardware Description Languages, Toledo, Spain, April 1997, pp. 305-314.
    [Ratan’s Directory] [Dissertation]
  15. Ratan Nalumasu and Ganesh Gopalakrishnan, “Explicit-enumeration based Verification made Memory-efficient,” Proceedings of the 1995 Computer Hardware Description Languages, Chiba, Japan, August, 1995, pp. 617-622.
  16. John Hurdle, Lüli Josephson, Erik Brunvand, and Ganesh Gopalakrishnan, “Asynchronous Models for Large Scale Neurocomputing Applications,” ‘NEURO NIMES ’92: Fifth International Conference on Neural Networks & their Applications,’ November 2-6, 1992, Nimes, France.
  17. Prabhat Jain and Ganesh Gopalakrishnan. “Efficient Symbolic Simulation Based Verification Using the Parametric form of Boolean Expressions,” International Conference on Computer Design (ICCD) 1992, pp. 598-602.

5.1.4  CUDA Verification

  1. Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan “A Symbolic Verifier for Cuda Programs,” PPoPP 2010, January, Bangalore, India (Accepted as a 2-page Poster Paper)
    [.pdf] [.bib]

5.1.5  Hardware Verification

  1. Xiaofang Chen, Steven M. German, and Ganesh Gopalakrishnan, “Transaction Based Modeling and Verification of Hardware Protocols,” Formal Methods in Computer Aided Design (FMCAD), 53-61, 2007, IEEE Computer Society.
    [.pdf] [.bib] [.ppt]
  2. Xiaofang Chen, Yu Yang, Michael DeLisi, Ganesh Gopalakrishnan, and Ching-Tsun Chou, “Hierarchical Cache Coherence Protocol Verification One Level at a Time Through Assume Guarantee,” IEEE Int’l High Level Design Validation and Test Workshop (HLDVT), 2007, 107-114.
    [.pdf] [.bib] [.ppt] [Hierarchical Protocol Benchmarks of This Paper in Murphi]
  3. Xiaofang Chen, Steven M. German, and Ganesh Gopalakrishnan, “Transaction Based Modeling and Verification of Hardware Protocols,” TECHCON, Semiconductor Research Corporation, Orlando, FL, 2007, Best Paper in Verification Session.
    [.pdf] [.bib] [.ppt]
  4. Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou, “Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee,” Formal Methods in Computer Aided Design (FMCAD), IEEE, San Jose, Nov 11-16, 81-88, 2006.
    [.pdf] [.bib] [techreport] [.ppt] [Hierarchical Protocol Benchmark Files of This Paper in Murphi]
  5. Sudhindra Pandav, Konrad Slind, and Ganesh Gopalakrishnan, “Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification,” CHARME 2005, LNCS 2144, 317-331.
    [.pdf] [.bib]
  6. Ali Sezgin and Ganesh Gopalakrishnan, “On the decidability of shared memory consistency verification,” Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2005, 199-208.
    [.pdf] [.bib]
  7. Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, “Memory-Model-Sensitive Data Race Analysis,” International Conference on Formal Engineering Methods (ICFEM), 2004, pages 30-45.
    [.pdf] [Jason’s Directory]
  8. Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind, “Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models,” International Parallel and Distributed Processing Symposium, 2004.
    [.pdf] [Jason’s Directory]
  9. Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj, “QB or not QB: An Efficient Execution Verification Tool for Memory Orderings,” Computer Aided Verification (CAV 2004), pp. 401-413, LNCS 3114.
    [.pdf] [.bib] [.ppt] [Itanium Spec of Intel] [Itanium HOL Spec Undelying MPEC] [Download MPEC] [O.Thorson’s UPC checker based on MPEC] [Hemanth’s Directory]
  10. Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind, “Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT,” Correct Hardware Design and Verification Methods, LNCS 2860, L’Aquila, Italy, 2003 pp. 81-95.
    [.pdf] [.ppt] [Jason’s Directory]
  11. Prosenjit Chatterjee, Hemanthkumar Sivaraj, and Ganesh Gopalakrishnan, “Shared memory consistency protocol verification against weak memory models: refinement via distributed model-checking.” 14th International Conference on Computer Aided Verification, Copenhagen, July 2002.
    [Prosenjit’s Directory] [.ppt] [Hemanth’s Directory]
  12. Ritwik Bhattacharya and Ganesh Gopalakrishnan, “Issues in Multiprocessor Memory Consistency Protocol Design and Verification.” Workshop on Designing Correct Circuits (DCC), Grenoble, France, August 2002.
  13. Annette Bunker, Sally A. McKee, and Ganesh Gopalakrishnan. “An Overview of Formal Hardware Specification Languages.” Grace Hopper Celebration of Women in Computing, October 2002.
    [Paper link]
  14. A. Weinzoepflen, M.D. Jones, D. Mery, D. Cansel and G. Gopalakrishnan, “Incremental Proof of the Producer/Consumer Property for the PCI Protocol,” ZB2002: Formal Specification and Development in Z and B, Grenoble, France, January 2002. Springer LNCS v.2272, pages 22-42.
  15. Annette Bunker and Ganesh Gopalakrishnan. “Using Live Sequence Charts for Hardware Protocol Specification and Compliance Verification,” in IEEE International High Level Design Validation and Test Workshop. IEEE Computer Society Press, November 2001, pages 95-100.
    [Paper link]
  16. Annette Bunker and Ganesh Gopalakrishnan, “An Approach to the Specification and Verification of System-on-Chip Compliance to Interfacing Standards,” International Conference on Integrated Design and Process Technology (IDPT), Pasadena, June 2002.
    [Paper link]
  17. Prosenjit Chatterjee and Ganesh Gopalakrishnan, “Towards a Formal Model of Shared Memory Consistency for Intel Itanium,” International Conference on Computer Design, Austin, TX, October 2001, 515-518.
    [Prosenjit’s Directory]
  18. Michael Jones and Ganesh Gopalakrishnan, “Verifying Transaction Ordering Properties in Unbounded Multi-Bus Networks through Algorithmic and Deductive Methods,” Formal Methods in Computer-Aided Design 2000 FMCAD’00), Austin, Texas.
    [Dissertation]
  19. Hans Jacobson, Chris Myers, and Ganesh Gopalakrishnan, “Achieving Fast and Exact Hazard-Free Logic Minimization of Extended Burst-Mode gC Finite State Machines,”, ICCAD, November, 2000.
    [Hans’s Directory]
  20. Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas, “Verifying Microarchitectures that Support Speculation and Exceptions,” Computer Aided Verification (CAV), Springer-Verlag LNCS 1855, 12th International Conference, Chicago, IL, July, 2000, pp. 521-537.
    [All PVS theory files and papers of Ravi Hosabettu] [Dissertation]
  21. Rajnish Ghughal and Ganesh Gopalakrishnan, “Verification methods for weaker shared memory consistency models,” Proceedings of the workshop FMPPTA (Formal Methods for Parallel Programming: Theory and Applications), Cancun, Mexico, May, 2000. Lecture Notes in Computer Science # 1800, José Rolim et al. (Eds.), pages 985-992.
    [Dissertation]
  22. Hans Jacobson, Erik Brunvand, Ganesh Gopalakrishnan, and Prabkahar Kudva, “High Level Asynchronous System Design Using the ACK Framework,” in Async’00, Proc. Sixth International Symposium on Advanced Research in Asynchronous Circuits and Systems, Eilat, Israel, April, 2000. IEEE Computer Society, ISBN 0-7695-0586-4, pages 93-103.
    [Hans’s Directory]
  23. Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas, “A Proof of Correctness of a Processor Implementing Tomasulo’s Algorithm Without a Reorder Buffer,” IFIP TC 10 WG 10.5 International Conference on Correct Hardware and Verification Methods (Charme’99), Bad Herrenalb (Germany), September 27-29, 1999. pp. 8-22, Springer LNCS.
    [All PVS theory files and papers of Ravi Hosabettu] [Dissertation]
  24. Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan, “Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach,” Computer Aided Verification, 11th International Conference, CAV’99, Trento, Italy, July 7-10, 1999. pp. 47-59.
    [All PVS theory files and papers of Ravi Hosabettu] [Dissertation]
  25. Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan, “Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem,” Formal Methods in Computer Aided Design, Second International Conference, FMCAD’98, Palo Alto, CA, USA, Nov 1998, Proceedings. Ganesh Gopalakrishnan and Phillip Windley (editors). Springer-Verlag LNCS 1522. pp. 237-254.
    [Mokkedem’s Files Including PVS]
  26. Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, “The ‘Test Model-checking’ Approach to the Verification of Formal Memory Models of Multiprocessors,” Computer Aided Verification, 10th International Conference, CAV’98, Vancouver, B.C., Canada, June/July 1998, Proceedings. Alan J. Hu and Moshe Y. Vardi (editors). Springer-Verlag LNCS 1427. pp. 464-476.
    [Ratan’s Directory] [Dissertation]
  27. Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan, “Decomposing the Proof of Correctness of Pipelined Microprocessors,” Computer Aided Verification, 10th International Conference, CAV’98, Vancouver, B.C., Canada, June/July 1998, Proceedings. Alan J. Hu and Moshe Y. Vardi (editors). Springer-Verlag LNCS 1427. pp. 122-134.
    [All PVS theory files and papers of Ravi Hosabettu] [Dissertation]
  28. Rajnish Ghughal, Abdel Mokkedem, Ratan Nalumasu, and Ganesh Gopalakrishnan, “Using ‘Test Model-Checking’ to Verify the Runway-PA800 Memory Model,” SPAA’98, Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, Puerto Vallarta, Mexico, June 28-July 2, 1998. pp. 231-239.
    [Ratan’s Directory] [Dissertation]
  29. Ratan Nalumasu and Ganesh Gopalakrishnan, “Deriving Efficient Cache Coherence Protocols Through Refinement,” Formal Methods for Parallel Programming: Theory and Applications (FMPPTA’98), April 1998.
    [Ratan’s Directory] [Dissertation]
  30. Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdel Mokkedem, and Ratan Nalumasu, “Formal Modeling and Validation Applied to a Commercial Coherent Bus: A Case Study,” Proceedings of CHARME (Correct Hardware design Methods), Montreal, October, 1997, pp. 48-64.
    [Ratan’s Directory] [Dissertation]
  31. Hans Jacobson and Ganesh Gopalakrishnan, “Asynchronous Microengines for Efficient High-level Control,” Advanced Research on VLSI (ARVLSI’97), Michigan, September 1997, pp. 201-218.
    [Hans’s Directory]
  32. Prabhakar Kudva, Ganesh Gopalakrishnan, and Hans Jacobson, “A Technique for Synthesizing Distributed Burst-mode Circuits,” ACM 33rd Design Automation Conference (DAC’96), Las Vegas, NV, June 3-8, 1996, pp. 67-70.
    [Hans’s Directory]
  33. Prabhakar Kudva, Hans Jacobson, Ganesh Gopalakrishnan, and Steven M. Nowick, “Synthesis of Hazard-free Customized CMOS Complex-gate Networks under Multiple-input Changes,” ACM 33rd Design Automation Conference (DAC’96), Las Vegas, NV, June 3-8, 1996, pp. 77-82.
    [Hans’s Directory]
  34. Prabhakar Kudva and Ganesh Gopalakrishnan, “Techniques for Synthesizing Efficient Burst-mode Circuits,” In TAU, workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Seattle, WA, Nov 10-11, 1995.
  35. Prabhakar Kudva, Ganesh Gopalakrishnan, and Venkatesh Akella, “An Asynchronous High Level Synthesis System Targeted at Interacting Burst-Mode Controllers,” Proceedings of the 1995 Computer Hardware Description Languages, Chiba, Japan, August, 1995, pp. 605-610.
  36. Jae-Tack Yoo, Ganesh Gopalakrishnan, Kent Smith, and John Mathews, “Counterflow-Clocked Pipelining Illustrated on the Design of High Speed HDTV Subband Vector Quantizer Chips,” Advanced Research on VLSI (ARVLSI’95), Chapel Hill, March 1995. (16 pages.)
  37. Prabhakar Kudva, Ganesh Gopalakrishnan, and Erik Brunvand, “Performance Analysis and Optimization of Asynchronous Circuits,” Intl. Conference on Computer Design (ICCD), 1994, pp. 221-224.
  38. Ganesh Gopalakrishnan, Prabhakar Kudva, Erik Brunvand, and Venkatesh Akella, “Peephole Optimization of Asynchronous Networks through Process Composition and Burst-mode Machine Generation,” Intl. Conference on Computer Design (ICCD), 1994, pp. 442-446.
  39. Ganesh Gopalakrishnan and Lüli Josephson, “Towards Amalgamating the Synchronous and Asynchronous Design Styles,” TAU ’93, Timing Aspects of VLSI, Malente, Germany. (13 pages.)
  40. Ganesh Gopalakrishnan and Venkatesh Akella, “A Transformational Approach to Asynchronous High-level Synthesis,” VLSI ’93, Grenoble, France, September 1993. IFIP/North-Holland publishers. pp. 201-210.
    [.pdf] [.bib]
  41. Venkatesh Akella and Ganesh Gopalakrishnan, “SHILPA: A High-level Synthesis System for Self-Timed Circuits,” accepted for publication in the International Conference on Computer Aided Design (ICCAD’92), Santa Clara, Nov. 1992. pp. 587-594.
  42. Armin Liebchen and Ganesh Gopalakrishnan. “Dynamic Reordering of High Latency Transactions in Time-Warp Simulation Using a Modified Micropipeline,” International Conference on Computer Design (ICCD) 1992, pp. 336-340.
  43. Prabhat Jain, Prabhakar Kudva, and Ganesh Gopalakrishnan, “Towards a Verification Technique for Large Synchronous Circuits,” The Fourth Computer-Aided Verification Workshop (CAV’92), Montreal, June 1992.
  44. Venkatesh Akella and Ganesh Gopalakrishnan. “Flow Analysis Techniques for the Synthesis of Efficient Asynchronous Circuits,” In TAU ’92: 1992 Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton, NJ, March 18–20, 1992.
  45. Venkatesh Akella and Ganesh Gopalakrishnan, “Hierarchical Action Refinement: A Methodology for Compiling Asynchronous Circuits from a Concurrent HDL,” Proceedings of the Tenth International Symposium on Computer Hardware Description Languages and their Applications, Marseille, France, April 1991.
  46. Ganesh Gopalakrishnan and Prabhat Jain and Venkatesh Akella and Luli Josephson and Wen-Yan Kuo, “Combining Verification and Simulation,” Advanced Research in VLSI (ARVLSI’91), Proceedings of the 1991 University of California Santa Cruz Conference, The MIT Press, 1991, Carlo Sequin (Ed.), pp. 323-339.
  47. Ganesh Gopalakrishnan and Prabhat Jain, “A Practical Approach to Synchronous Hardware Verification,” in VLSI Design ’91: The Fourth CSI/IEEE International Symposium on VLSI Design, January 5-8, 1991, New Delhi, India.
  48. Venkatesh Akella and Ganesh Gopalakrishnan, “High Level Test Generation via Process Composition,” Designing Correct Circuits, Oxford, 1990, Springer Verlag, Proceedings of the DCC Workshop, Oxford, September, 1990, Published in Springer series ‘Workshops in Computing,’ pp. 99-119
  49. Ganesh C. Gopalakrishnan, Narayana Mani, and Venkatesh Akella, “A Design Validation System for Synchronous Hardware based on a Process Model: A Case Study,” IMEC-IFIP Workshop on ‘Applied Formal Methods for Correct VLSI Design,’ Nov. 13–16, Leuven, Belgium, 1989. pp. 227-246.
  50. Ganesh C. Gopalakrishnan, Richard M. Fujimoto, Venkatesh Akella, N.S. Mani, and Kevin Smith, “Specification Driven Design of Custom VLSI Architectures in HOP,” G. Birtwistle and P.A. Subrahmanyam (editors), Current Trends in Hardware Verification and Automated Theorem Proving, Chapter 3, pp. 128–170, Springer-Verlag, 1989.
  51. Ganesh C. Gopalakrishnan, “Specification and Verification of Pipelined Hardware in HOP,” Ninth International Symposium on Computer Hardware Description Languages (CHDL’89), Washington, D.C., June, 1989, pp. 117–131.
  52. Ganesh C. Gopalakrishnan, Narayana Mani, and Venkatesh Akella, “Parallel Composition of Lock-step Synchronous Processes for Hardware Validation: Divide-and-conquer Composition,” in Springer Verlag Lecture Notes in Computer Science, No.407 (Automatic Verification Methods for Finite-State Systems, International Workshop, Grenoble, France, June 1989), J.Sifakis (Editor), pp. 374-382.
  53. Richard M. Fujimoto, Jya-Jang Tsai and Ganesh C. Gopalakrishnan, “Design and Performance Evaluation of the Roll Back Chip,” 1988 IEEE/ACM Computer Architecture Conference (ISCA’88), Honolulu, Hawaii, June 1988. pp. 401-408.
  54. Richard M. Fujimoto, Jya-Jang Tsai and Ganesh C. Gopalakrishnan, “The Roll Back Chip: Hardware Support for Distributed Simulation Using Time Warp,” the Society for Computer Simulation Multiconference, San Diego, CA, Feb 1988.
  55. Ganesh C. Gopalakrishnan, “Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets,” Internal Workshop on Petri Nets and Performance Models, Wisconsin, August 24-26 (1987).
  56. Ganesh C. Gopalakrishnan, M.K. Srivas, and D.R. Smith, “From Algebraic Specifications to Correct VLSI Circuits,” in book From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (Ed.), IFIP, North-Holland (1987) 197-225.
  57. Ganesh C. Gopalakrishnan, N.C.Lee, D.R.Smith and M.K.Srivas, “Deriving Module Interconnectivity From Behavioral Specifications and Coupling a VLSI Layout Editor for Error-free Routing,” 1986 Fall Joint Computer Conference, Dallas, Nov. 1986.
  58. Ganesh C. Gopalakrishnan, D.R.Smith, and M.K.Srivas, “An Algebraic Approach to the Specification and Realization of VLSI Designs,” 7th International Symposium on Computer Hardware Description Languages (CHDL’85), Tokyo, Japan, Aug. 1985, North-Holland (1985) 16-38.

5.2  RESEARCH PRESENTATIONS

MASTER LINK to all our presentations

5.2.1  MPI

  1. Gauss group’s poster at Supercomputing 2006
  2. Gauss group’s EuroPVM/MPI (2006) Outstanding Paper presentation (presented by Mike Kirby).
  3. Gauss group talk at the SIAM 2006 meeting (presented by Mike Kirby)
  4. cav04.ppt
  5. cav02.ppt

5.2.2  Hardware and Memory Models

  1. Constraints workshop (ETAPS 2004)
  2. DCC workshop (2004): Talk on Post-Si Verification
  3. Tutorial on Cache Coherence Protocol Verification at FMCAD 2004
    1. Ching Tsun Chou
    2. Steven German
    3. Ganesh Gopalakrishnan
  4. SRC presentations:
    1. 2006
    2. 2005
    3. 2004
  5. Presentation at the SRI Grand Challenge Workshop
  6. Presentation at Intel
  7. Intel FV tutorials

5.2.3  New Grad Presentation

  1. New Grad Presentation

5.2.4  Youth Education

  1. Science for 7th Graders (2006)
  2. Youth Education visitors (2006)

5.3  DISSERTATIONS

  1. Xiaofang Chen, PhD [.pdf] [.bib]
  2. Yu Yang, PhD [.pdf] [.bib]

5.4  BOOKS

  1. Ganesh Gopalakrishnan, “Computation Engineering: applied automata theory and logic” (505 pages). Springer, ISBN 0-387-24418-2, 2006.
  2. 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.
  3. 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.5  JOURNALS

5.5.1  Distributed Model Checking

  1. I. Melatti, R. Palmer, G. Sawaya, Y. Yang, R. M. Kirby, and G. Gopalakrishnan, “Parallel and distributed model checking in Eddy,” Journal International Journal on Software Tools for Technology Transfer (STTT), Springer Berlin / Heidelberg, ISSN 1433-2779 (Print), November 2008. (Special section on SPIN.)

5.5.2  MPI Verification

  1. Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “Formal Verification of Programs that use MPI One-sided Communication.” Under Submission.

5.5.3  Hardware Verification

  1. Ali Sezgin and Ganesh Gopalakrishnan, “On the definition of sequential consistency,” Inf. Process. Lett. 96(6): 193-196 (2005).
    A preliminary version [.pdf]
  2. Annette Bunker, Ganesh Gopalakrishnan, and Konrad Slind, “Live sequence charts applied to hardware requirements specification and verification,” STTT 7(4): 341-350 (2005).
    [Paper link]
  3. Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, “UMM: an operational memory model specification framework with integrated model checking capability,” Concurrency and Computation: Practice and Experience. Volume 17, Issue 5-6, Pages 465-487, February 2005.
    [.pdf] [.bib] [Jason’s Directory]
  4. Annette Bunker, Ganesh Gopalakrishnan, and Sally A. McKee, “Formal Hardware Specification Languages for Protocol Compliance Verification.” ACM Transactions on Design Automation of Electronic Systems, vol. 9, no. 1, January 2004.
    [.pdf] [Paper link]
  5. Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas, “Formal Verification of a Complex Pipelined Processor,” Formal Methods in System Design, Volume 23, Number 2, September 2003, pp. 171-213.
  6. Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas, “A Practical Methodology for Verifying Pipelined Microarchitectures,” IEEE Design & Test, Volume 20, Number 4, July-August 2003, pp. 4-15.
  7. Ratan Nalumasu and Ganesh Gopalakrishnan, “An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation,” Formal Methods in System Design (Kluwer), Vol. 20, No. 3, May 2002, pp. 231-247.
  8. Ratan Nalumasu and Ganesh Gopalakrishnan, “Deriving Efficient Cache Coherence Protocols Through Refinement,” Formal Methods in System Design (Kluwer), Vol. 20, No. 1, January 2002, Pages 107-125.
  9. Abdel Mokkedem, Ravi M. Hosabettu, Michael D. Jones and Ganesh C. Gopalakrishnan, “Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem,” in special issue ‘Formal Methods for CAD: Enabling technologies and system-level applications,’ Formal Methods in System Design, Ganesh Gopalakrishnan (Editor.), Volume 16, Issue 1, January, 2000, pp. 93-119.
  10. Hans M. Jacobson and Ganesh Gopalakrishnan, “Application-Specific Programmable Control for High-Performance Asynchronous Circuits,” Invited Paper, Proceedings of IEEE, Vol. 87, No. 2, Feb 1999, pp. 319–331.
  11. Jae-tack Yoo, Ganesh Gopalakrishnan, and Kent Smith, “Timing Constraints for High Speed Counterflow-Clocked Pipelining,” IEEE Transactions on Very Large Scale Integration (VLSI) Systems, Vol. 7, No. 2, June 1999, pp. 167-173.
    [.pdf]
  12. Prabhakar Kudva, Ganesh Gopalakrishnan, and Erik Brunvand, “Peephole Optimization of Asynchronous Macromodule Networks,” IEEE Transactions on Very Large Scale Integration (VLSI) Systems, Vol. 7, No. 1, March 1999, pp. 30-37.
    [.pdf]
  13. Jae-tack Yoo, Kent Smith, and Ganesh Gopalakrishnan, “A Fast Parallel Squarer Based on Divide-and-Conquer,” IEEE Journal of Solid-state Circuits, Vol. 32, No. 6, June 1997, pp. 909-912.
  14. Venkatesh Akella and Ganesh Gopalakrishnan, “CFSIM: A Concurrent Compiled Code Functional Simulator for hopCP,” International Journal of Computer Simulation, Vol. 4, No. 4, 1994, pp. 375-394.
  15. Ganesh Gopalakrishnan, “Micropipeline Wavefront Arbiters using Lockable C-elements,” IEEE Design & Test of Computers, Winter 1994, Vol.11, No.4, pp. 55-64.
  16. Venkatesh Akella and Ganesh Gopalakrishnan, “Specification and Validation Control Intensive ICs in hopCP,” IEEE Transactions on Software Engineering, Vol.20, No.6, June 1994, pp. 405-423.
  17. Ganesh Gopalakrishnan, Erik Brunvand, Nick Michell, and Steven M. Nowick, “A Correctness Criterion for Asynchronous Circuit Validation and Optimization,” IEEE Transactions on Computer Aided Design, Vol.13, No.11, November 1994, pp. 1309-1318.
    [.pdf]
  18. Ganesh Gopalakrishnan and Venkatesh Akella, “High Level Optimizations in Compiling Process Descriptions to Asynchronous Circuits,” Journal of VLSI Signal Processing (Kluwer), No. 7, 1994, pp. 33-45.
  19. Ganesh Gopalakrishnan and Richard Fujimoto, “Design and Verification of the Rollback Chip using HOP: An Illustration of Formal Methods Applied to Hardware Design,” ACM Transactions on Computer Systems (TOCS), Vol.11, No.2, May 1993, pp. 109-145.
  20. Ganesh Gopalakrishnan and Venkatesh Akella, “VLSI Asynchronous Systems: Specification and Synthesis,” Microprocessors & Microsystems, Vol.16, No.10, October 1992, pp. 517-527.
  21. Richard M. Fujimoto, Jya-jang Tsai, and Ganesh Gopalakrishnan, “Design and Evaluation of the Rollback Chip: Special Purpose Hardware for Time Warp,” IEEE Trans. on Computer, Vol.41, No.1, 1992, pp. 68-82.
  22. Ganesh C. Gopalakrishnan, Richard Fujimoto, Venkatesh Akella, and Narayana Mani, “HOP: A Process Model for Synchronous Hardware. Semantics, and Experiments in Process Composition,” Integration: The VLSI Journal (North-Holland), 8 (1989), pp. 209-247.

5.5.4  Model Checking and Functional Programming

  1. Prabhat Jain and Ganesh Gopalakrishnan, “Efficient Symbolic Simulation Based Verification Using the Parametric Form of Boolean Expressions,” IEEE Transactions on Computer Aided Design, Vol.13, No.8, August 1994, pp. 1005-1015.
  2. Ganesh C. Gopalakrishnan and Mandayam K. Srivas, “Implementing Functional Programs Using Mutable Abstract Data Types,” Information Processing Letters, Vol.26, No.6, Jan 1988.

5.6  SELECTED TECHNICAL REPORTS

(The full list of TRs is here)

  1. UUCS-07-008 Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert Kirby, “Runtime Model Checking of Multi-threaded C/C++ Programs.”
  2. UUCS-06-014, “A general compositional approach to verifying hierarchical cache coherence protocols,” Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou.
  3. UUCS-04-008, “Verification of MPI Programs Using Spin,” Steven Barrus, Ganesh Gopalakrishnan, Robert M. Kirby, Robert Palmer.
  4. UUCS-03-001, “Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking,” Hemanthkumar Sivaraj and Ganesh Gopalakrishnan.
  5. UUCS-03-028, “A Symbolic Partial Order Reduction Algorithm for Rule Based Transitions Systems,” Ritwik Bhattacharya, Steven German, and Ganesh Gopalakrishnan.

6  CONFERENCES/WORKSHOPS ORGANIZED

  1. General Chair, PADTAD 2009, Chicago, July 19-20, 2009.
  2. (EC)2 Exploiting Concurrency Efficiently and Correctly, Grenoble, France, June 26-27, 2009. A Pre-CAV 2009 Workshop.
  3. Lindstrom Retirement Workshop and FestSchrift. The ENTCS Special Issue is The ENTCS Special Issue is here, or look for Issue 193 of this.
  4. TV06: Seattle, WA, August 21-22, 2006. Multithreading in Hardware and Software: Formal Approaches to Design and Verification. Part of Floc 2006. You can get the articles thru this link. here, or look for Issue 174 of this.
  5. TPHOLs 2004 Co-organizer (with Annette Bunker - Konrad Slind is Chair) TPHOLs, Park City, Utah, September 2004.
  6. MPV 2000">Chair, Workshop on Specification and Verification of Shared Memory Systems (MPV). You can get the slides thru this link.
  7. WAVe 2000 Chair, Workshop on Advances in Verification (WAVe). You can get the articles thru this link.
  8. FMCAD 1998 Co-Chair, Formal Methods in CAD (FMCAD), 1998. You can get the articles thru this link.

7  SOFTWARE

7.1  MPI Formal Verification

7.1.1  ISP

Download ISP - our MPI/C program verification tool, and User Manual

The ISP (“In-situ Partial Order”) Verification tool employs our own dynamic partial order reduction algorithm called POE (see our CAV 2008 paper in Section 5.1 - item 9)

7.2  MCC Releated (Multi-core Communications API)

[Under Construction]

7.3  Thread Verification

7.3.1  Inspect

The Inspect Dynamic Verification tool for C/Thread Programs. Associated papers are : (click these 4,3,1).
[DOWNLOAD] [GETTING STARTED] [TUTORIAL SLIDES] [TUTORIAL EXAMPLES]

7.4  Model Checking Software

7.4.1  Murphi

The below link contains the descriptions and download links for the many versions of Murphi.

Murphi Software List

7.4.2  Other Model Checking Applications

  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  GRANTS

Supported in part by

9  AFFILIATED FACULTY

School of Computing:
Electrical and Computer Engineering:

10  PEOPLE (FACULTY, STUDENTS, AND ALUMNI)

FACULTY AND STUDENTS

ALUMNI

11  CONFERENCE DEADLINES

namestart datefirst submission deadlinedescription
IFM2/16/20099/12/2008Integrated Formal Methods
SOSP10/11/20093/2/2009Symposium on Operating Systems Principles
ICCAD11/2/20095/11/2009Computer-Aided Design
HPCA1/9/20107/24/2009High-Performance Computer Architecture
ASPLOS3/13/20108/3/2009Architectural Support for Programming Languages and OS
VMCAI1/17/20108/21/2009Verification, Model Checking and Abstract Interpretation
CAV7/16/20109/1/2009Computer Aided Verification
DATE3/8/20109/6/2009Design Automation and Test in Europe
ICSE5/2/20109/6/2009International Conference on Software Engineering
IPDPS4/19/20109/21/2009Parallel and Distributed Processing
TACAS3/20/201010/1/2009Tools and Algorithms for the Construction and Analysis of Systems
ESOP3/22/201010/1/2009European Symposium on Programming
NSDI4/28/201010/2/2009Networked System Design and Implementation
ISCA6/19/201011/9/2009Symposium on Computer Archetecture
PLDI6/5/201011/13/2009Programming Language Design and Implementation
SIGCSE3/10/20109/11/2009Symposium on Computer Science Education
DAC6/13/20101/22/2010Design Automation Conference
ICS6/1/20101/11/2010International Conference on Supercomputing
MEMOCODE7/26/20102/26/2010Formal Methods and Models for Codesign
ASE9/20/20103/8/2010Automated Software Engineering
VSTTE8/16/20103/29/2010Verified Software: Theories, Tools, and Experiments
SC11/13/20104/3/2010(approx)Super Computing
CONCUR8/31/20104/8/2010Concurrency Theory
FSE11/7/20103/5/2010Foundations of Software Engineering
SPIN9/27/20105/1/2010SPIN model checking
FMCAD10/20/20105/5/2010Formal Methods in Computer Aided Design
OSDI10/4/20105/7/2010Operating Systems Design and Implementation
POPL1/26/20117/14/2010Principles of Programming Languages
PPoPP2/12/20117/17/2010(approx)Principles and Practice of Parallel Programming
MEMS1/23/20119/1/2010(approx)Micro Electro Mechanical Systems
ICPP09/13/201002/24/2010International Conference on Parallel Processing
FSE11/07/201002/05/2010Foundations of Software Engineering
This document was translated from LATEX by HEVEA.