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
-
Dynamic Verification Methods and tools for
Thread Programs (currently C/Pthreads)
- Dynamic Verification Methods and tools for
MPI (Message Passing Interface) programs (currently C/MPI)
- Verifying
Hierarchical Multicore Cache Coherence Protocols using Assume/Guarantee
methods supported by conventional tools (e.g., explicit state enumeration
using Murphi)
- Verifying hardware
implementations of cache coherence (and other)
protocols against higher level specifications
- Building verification tools for applications
written using the Multicore Communications API (MCAPI)
- Building an FPGA-based communication fabric realizing
MCAPI, and performance measurements
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
- 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] -
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]
- 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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)
-
Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer,
“Dynamic Verification of Multicore Communication Applictions in MCAPI,”
HLDVT 2009, November, San Francisco, CA
[.pdf]
[.bib] - Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt,
“MCC - A runtime verification tool for MCAPI user applications,”
FMCAD 2009, November 2009
[.pdf]
[.bib] - 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
- 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] - 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] - 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] - 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] - 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] - 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)] - 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] - 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] - 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.
- 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]
- 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]
- 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] - 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] - 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] - 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.
- 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.
-
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
-
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
- 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] - 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] - 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] - 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] - Sudhindra Pandav, Konrad Slind, and
Ganesh Gopalakrishnan,
“Counterexample Guided Invariant Discovery for
Parameterized Cache Coherence Verification,” CHARME 2005,
LNCS 2144, 317-331.
[.pdf]
[.bib] - 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] - 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] - 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] - 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] - 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] - 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] - Ritwik Bhattacharya and Ganesh Gopalakrishnan,
“Issues in Multiprocessor Memory Consistency Protocol Design and Verification.”
Workshop on Designing Correct Circuits (DCC), Grenoble, France, August 2002.
- 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] - 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.
- 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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.
- 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.
- 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.)
- Prabhakar Kudva, Ganesh Gopalakrishnan, and
Erik Brunvand,
“Performance Analysis and Optimization of Asynchronous
Circuits,”
Intl. Conference on Computer Design (ICCD), 1994,
pp. 221-224.
- 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.
- Ganesh Gopalakrishnan and Lüli Josephson,
“Towards Amalgamating the Synchronous and Asynchronous
Design Styles,” TAU ’93, Timing Aspects of VLSI,
Malente, Germany.
(13 pages.)
- 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] - 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.
-
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.
-
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.
-
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.
- 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.
- 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.
- 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.
- 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
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Ganesh C. Gopalakrishnan,
“Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets,”
Internal Workshop on Petri Nets and Performance
Models, Wisconsin, August 24-26 (1987).
- 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.
- 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.
- 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
- Gauss group’s poster at Supercomputing 2006
-
Gauss group’s EuroPVM/MPI (2006) Outstanding Paper presentation (presented by Mike Kirby).
- Gauss group talk at the SIAM 2006 meeting (presented by Mike Kirby)
- cav04.ppt
- cav02.ppt
5.2.2 Hardware and Memory Models
-
Constraints workshop (ETAPS 2004)
- DCC workshop (2004): Talk on Post-Si Verification
- Tutorial on Cache Coherence Protocol Verification at FMCAD 2004
-
Ching Tsun Chou
- Steven German
- Ganesh Gopalakrishnan
- SRC presentations:
-
2006
- 2005
- 2004
- Presentation at the SRI Grand Challenge Workshop
- Presentation at Intel
- Intel FV tutorials
5.2.3 New Grad Presentation
-
New Grad Presentation
5.2.4 Youth Education
-
Science for 7th Graders (2006)
- Youth Education visitors (2006)
5.3 DISSERTATIONS
- Xiaofang Chen, PhD
[.pdf]
[.bib]
- Yu Yang, PhD
[.pdf]
[.bib]
-
Ganesh Gopalakrishnan, “Computation Engineering: applied
automata theory and logic” (505 pages).
Springer, ISBN 0-387-24418-2, 2006.
- 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.
- 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
- 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
- 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
- Ali Sezgin and Ganesh Gopalakrishnan, “On the definition of
sequential consistency,” Inf. Process. Lett. 96(6): 193-196 (2005).
A preliminary version [.pdf] - 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] - 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] - 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] - 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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] - 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] - 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.
- 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.
- Ganesh Gopalakrishnan, “Micropipeline Wavefront Arbiters
using Lockable C-elements,”
IEEE Design & Test of Computers,
Winter 1994, Vol.11, No.4, pp. 55-64.
- 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.
- 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] - 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.
- 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.
- Ganesh Gopalakrishnan and Venkatesh Akella,
“VLSI Asynchronous Systems: Specification and Synthesis,”
Microprocessors & Microsystems, Vol.16, No.10, October 1992,
pp. 517-527.
- 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.
- 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
-
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.
- 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)
- UUCS-07-008
Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert Kirby,
“Runtime Model Checking of Multi-threaded C/C++ Programs.”
- UUCS-06-014,
“A general compositional approach to verifying hierarchical cache coherence protocols,”
Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou.
- UUCS-04-008, “Verification of MPI Programs Using Spin,”
Steven Barrus, Ganesh Gopalakrishnan, Robert M. Kirby, Robert Palmer.
- UUCS-03-001, “Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking,”
Hemanthkumar Sivaraj and Ganesh Gopalakrishnan.
- 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
- General Chair,
PADTAD 2009,
Chicago, July 19-20, 2009.
- (EC)2 Exploiting Concurrency Efficiently and Correctly,
Grenoble, France, June 26-27, 2009. A Pre-CAV 2009 Workshop.
- Lindstrom Retirement Workshop and
FestSchrift. The ENTCS Special Issue is
The ENTCS Special Issue is
here,
or look for
Issue 193 of this.
- 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.
- TPHOLs 2004
Co-organizer (with
Annette Bunker - Konrad Slind is Chair) TPHOLs, Park City, Utah,
September 2004.
- MPV 2000">Chair, Workshop on Specification and Verification of Shared Memory Systems (MPV).
You can get the slides thru this link.
- WAVe 2000
Chair, Workshop on Advances in Verification (WAVe).
You can get the articles thru this link.
- 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
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)
-
Runs under Linux, MAC OS/X, and Windows.
- Windows version has a Visual Studio plug-in that is also
downloadable.
- Tested with MPICH2, OpenMPI, and Microsoft MPI libraries. (If
interested
in other MPI libraries – try it, and if it does not work, let us know.)
- Push-button checking of thousands of lines of MPI/C code in seconds,
for deadlocks, assert violations, MPI object leaks, and
communication races.
7.2 MCC Releated (Multi-core Communications API)
[Under Construction]
7.3 Thread Verification
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
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
- 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.
- 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.
-
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.
- 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.
- 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.
- 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.
-
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.
- 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.
- 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
-
A grant from Microsoft Corporation
- NSF award CNS-0509379,
“CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis,”
September 2005-2009.
- NSF award CCF-0811429,
“CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design,”
June 2008-2011.
- SRC Task ID 1847.001,
“Formal Specification, Verification, and Test Generation for
Multi-core CPUs,”
August 2008.
9 AFFILIATED FACULTY
-
School of Computing:
-
- Electrical and Computer Engineering:
-
10 PEOPLE (FACULTY, STUDENTS, AND ALUMNI)
FACULTY AND STUDENTS
ALUMNI
-
Xiaofang Chen (Amazon)
- Dr. Igor Melatti (Post-doctoral visitor)
- Robert Palmer (past PhD, now with Microsoft’s HPC Group)
- Salman Pervez (past MS, now PhD student at Purdue
University)
- Sonjong Hwang (past BS/MS, with SAP Research, Korea)
- Steve Barrus (past BS/MS, now with Intel)
- Ritwik Bhattacharya (past PhD, now with
Intel Hillsboro)
- Sudhindra Pandav (past MS (Konrad was advisor), Intel Bangalore)
- Hemanthkumar Sivaraj (past MS, Intel Bangalore)
- Yue (Jason) Yang - (past PhD co-advised with Lindstrom, Microsoft)
- Ali Sezgin (past PhD - Asst Prof, Yeditepe Univ., now Staff Researcher under Serdar Tasiran,
Koc University)
- Annette Bunker (past PhD Co-Advised with Prof.
Konrad Slind - now at Intel, Hillsboro)
- Prosenjit Chatterjee (past MS,
now Manager, Formal Verification Group, Nvidia)
- Mike Jones (past PhD, now Assoc. Prof at BYU, Utah)
- Ravi Hosabettu (past PhD, now at Juniper Networks)
- Rajnish Ghughal (past MS, at Intel, Oregon)
- Ratan Nalumasu (past PhD, at Google)
- Prabhakar Kudva (past PhD, at IBM Watson)
- Venkatesh Akella (past PhD, now Full Professor at UC Davis)
- Prabhat Jain
(past MS, was at Bell Labs, then PhD student at MIT, now?)
- Narayana Mani (past MS, at ?)
11 CONFERENCE DEADLINES
| name | start date | first submission deadline | description |
| IFM | 2/16/2009 | 9/12/2008 | Integrated Formal Methods |
|
SOSP | 10/11/2009 | 3/2/2009 | Symposium on Operating Systems Principles |
|
ICCAD | 11/2/2009 | 5/11/2009 | Computer-Aided Design |
|
HPCA | 1/9/2010 | 7/24/2009 | High-Performance Computer Architecture |
|
ASPLOS | 3/13/2010 | 8/3/2009 | Architectural Support for Programming Languages and OS |
|
VMCAI | 1/17/2010 | 8/21/2009 | Verification, Model Checking and Abstract Interpretation |
|
CAV | 7/16/2010 | 9/1/2009 | Computer Aided Verification |
|
DATE | 3/8/2010 | 9/6/2009 | Design Automation and Test in Europe |
|
ICSE | 5/2/2010 | 9/6/2009 | International Conference on Software Engineering |
|
IPDPS | 4/19/2010 | 9/21/2009 | Parallel and Distributed Processing |
|
TACAS | 3/20/2010 | 10/1/2009 | Tools and Algorithms for the Construction and Analysis of Systems |
|
ESOP | 3/22/2010 | 10/1/2009 | European Symposium on Programming |
|
NSDI | 4/28/2010 | 10/2/2009 | Networked System Design and Implementation |
|
ISCA | 6/19/2010 | 11/9/2009 | Symposium on Computer Archetecture |
|
PLDI | 6/5/2010 | 11/13/2009 | Programming Language Design and Implementation |
|
SIGCSE | 3/10/2010 | 9/11/2009 | Symposium on Computer Science Education |
|
DAC | 6/13/2010 | 1/22/2010 | Design Automation Conference |
|
ICS | 6/1/2010 | 1/11/2010 | International Conference on Supercomputing |
|
MEMOCODE | 7/26/2010 | 2/26/2010 | Formal Methods and Models for Codesign |
|
ASE | 9/20/2010 | 3/8/2010 | Automated Software Engineering |
|
VSTTE | 8/16/2010 | 3/29/2010 | Verified Software: Theories, Tools, and Experiments |
|
SC | 11/13/2010 | 4/3/2010(approx) | Super Computing |
|
CONCUR | 8/31/2010 | 4/8/2010 | Concurrency Theory |
|
FSE | 11/7/2010 | 3/5/2010 | Foundations of Software Engineering |
|
SPIN | 9/27/2010 | 5/1/2010 | SPIN model checking |
|
FMCAD | 10/20/2010 | 5/5/2010 | Formal Methods in Computer Aided Design |
|
OSDI | 10/4/2010 | 5/7/2010 | Operating Systems Design and Implementation |
|
POPL | 1/26/2011 | 7/14/2010 | Principles of Programming Languages |
|
PPoPP | 2/12/2011 | 7/17/2010(approx) | Principles and Practice of Parallel Programming |
|
MEMS | 1/23/2011 | 9/1/2010(approx) | Micro Electro Mechanical Systems |
|
ICPP | 09/13/2010 | 02/24/2010 | International Conference on Parallel Processing |
|
FSE | 11/07/2010 | 02/05/2010 | Foundations of Software Engineering |
This document was translated from LATEX by
HEVEA.