Publications
- Vinu Joseph, Saurav Muralidharan, Animesh Garg, Michael Garland, and Ganesh Gopalakrishnan (2019). A Programmable Approach to Model Compression. (pp. 13). arxiv.
Published, 11/06/2019.
https://arxiv.org/pdf/1911.02497.pdf - Ganesh L. Gopalakrishnan (2019). Automata and Computability: A Programmer's Perspective. (pp. 328). CRC Press. Published, 02/06/2019.
- Tyler Sorenson, Alastair F. Donaldson, Mark Batty, Ganesh Gopalakrishnan, and Zvonimir Rakamaric, ``Portable Inter-Workgroup Barrier Synchronisation for GPUs,'' Object-Oriented Programming, Systems, Languages \& Applications (SPLASH), November, 2016. Published, 11/01/2016.
- Vishal Chandra Sharma, Ganesh Gopalakrishnan, and Sriram Krishnamoorthy, ``PRESAGE: Protecting Structured Address Generation against Soft Errors,'' The 23rd annual IEEE International Conference on High Performance Computing, Data, and Analytics (HiPC), December, 2016. Published, 11/01/2016.
- Sriram Aananthakrishnan, Greg Bronevetsky, Mark S. Baranowski, and Ganesh Gopalakrishnan, ``ParFuse: Parallel and Compositional analysis of Message Passing Programs,'' The 29th International Workshop on Languages and Compilers for Parallel Computing (LCPC), September, 2016.
Published, 11/01/2016.
http://www.cs.utah.edu/fv - Mohammed Al-Mahfoudh, Ganesh Gopalakrishnan, and Ryan Stutsman, ``Toward Rigorous Design of Domain-Specific Distributed Systems,'' Workshop on Formal Methods in Software Engineering (FormaliSE) May, 2016. Published, 11/01/2016.
- Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Dong H. Ahn, Gregory L Lee, Ignacio Laguna, Martin Schulz, Joachim Protze, and Matthias Mueller, ``ARCHER: Effectively Spotting Data Races in Large OpenMP Applications,'' IPDPS, May, 2016.
Published, 06/01/2016.
http://www.cs.utah.edu/fv - Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman, ``Toward Bringing Distributed Systems Design upon Rigorous Footing,'' Workshop on Formal Methods and Integration (FMi). 2016.
Published, 05/01/2016.
http://www.cs.utah.edu/fv - Vishal Chandra Sharma, Ganesh Gopalakrishnan, Sriram Krishnamoorthy, ``Towards Resiliency Evaluation of Vector Programs,'' 21st IEEE Workshop on Dependable Parallel, Distributed and Network-Centric Systems (DPDNS) 2016.
Published, 05/01/2016.
http://www.cs.utah.edu/fv - Charles Jacobsen, Alexey Solovyev, Ganesh Gopalakrishnan, ``A Parametrized Floating-Point Formalization in HOL Light,'' Electronic Notes in Theoretical Computer Science, Volume 317, 18 November 2015, Pages 101–107, (selected from the papers presented at the Seventh and Eighth International Workshops on Numerical Software Verification, NSV). doi:10.1016/j.entcs.2015.10.010.
Published, 11/01/2015.
http://www.cs.utah.edu/fv - Wei-Fan Chiang, Ganesh Gopalakrishnan, and Zvonimir Rakamaric, ``Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs,'' Workshop on Numerical Software Verification, 2015, Seattle, WA.
Published, 10/01/2015.
http://www.cs.utah.edu/fv - Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric and Ganesh Gopalakrishnan, ``Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions,'' pp. 532-550, Nikolaj Bj{\o}rner and Frank S. de Boer (ed.), FM 2015, LNCS 9109.
Published, 08/01/2015.
http://www.cs.utah.edu/fv - Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen and John Wickerson, ``GPU concurrency: Weak behaviours and programming assumptions,'' ASPLOS 2015, Istanbul, Turkey.
Published, 03/01/2015.
http://www.cs.utah.edu/fv - Joachim Protze, Simone Atzeni, Dong H. Ahn, Martin Schulz, Ganesh Gopalakrishnan, Matthias S. Muller, Ignacio Laguna, Zvonimir Rakamaric, Greg L. Lee., “Towards Provid- ing Low-Overhead Data Race Detection for Large OpenMP Applications,” LLVM Compiler Infrastructure in HPC Workshop (LLVM-HPC 2014), New Orleans, LA, USA. Published, 11/17/2014.
- Peng Li, Guodong Li, and Ganesh Gopalakrishnan, “Practical Symbolic Checking of GPU Programs,” Supercomputing (SC 2014). Published, 11/17/2014.
- Diego Caminha B de Oliveira, Alan Humphrey, Qingyu Meng, Zvonimir Rakamaric, Martin Berzins and Ganesh Gopalakrishnan, “Systematic Debugging of Concurrent Systems Using Coalesced Stack Trace Graphs,” LCPC 2014. Published, 09/01/2014.
- Vishal Chandra Sharma, Zvonimir Rakamari ́c and Ganesh Gopalakrishnan, “FUSED: A Low- cost Online Soft-Error Detector,” 10th Workshop on Silicon Errors in Logic - System Effects (SELSE) 2014. Published, 02/04/2014.
- Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamar ́c and Alexey Solovyev, “Ef- ficient Search for Inputs Causing High Floating-point Errors,” Principles and Practices of Parallel Programming (PPoPP), February, 2014. Published, 02/03/2014.
- Vishal Chandra Sharma, Arvind Haran, Zvonimir Rakamari, and Ganesh Gopalakrishnan, “Towards Formal Approaches to System Resilience,” 19th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC) 2013. Published, 11/2013.
- Tyler Sorensen, Ganesh Gopalakrishnan, and Vinod Grover, “Towards Shared Memory Con- sistency Models for GPUs,” Proceedings of the 27th international ACM conference on Inter- national conference on supercomputing, 2013. Published, 07/2013.
- Sriram Ananthakrishnan, Greg Bronevetsky, and Ganesh Gopalakrishnan, “Hybrid Approach for Data-flow Analysis of MPI Programs,” Proceedings of the 27th international ACM con- ference on International conference on supercomputing, 2013. Published, 07/2013.
- Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamari, and Guodong Li, “Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding,” Nasa For- mal Methods 2013. Published, 06/2013.
- Diego Caminha, Ganesh Gopalakrishnan, Zvonimir Rakamari ́c, Martin Berzins, Alan Humphrey, and Qingyu Meng, “Practical Formal Correctness Checking of Million-Core Problem Solving Environments for HPC,” 7th International Workshop on Software Engineering for Computa- tional Science and Engineering, 2013. Published, 05/2013.
- Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamari ́c, Dong Ahn, and Gregory Lee, “Determinism and Reproducibility in Large-Scale HPC Systems,” 4th Workshop on Determinism and Correctness in Parallel Programming, 2013. Published, 02/2013.
- Peng Li, Guodong Li, and Ganesh Gopalakrishnan, “Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs,” Supercomputing 2012, Salt Lake City, UT, November 2012. Published, 11/01/2012.
- Subodh Sharma, Ganesh Gopalakrishnan, and Greg Bronevetsky, “A Sound Reduction of Persistent- sets for Deadlock Detection in MPI Applications,” SMBF 2012 - The Brazilian Symposium on Formal Methods, Natal, September 2012. Published, 09/01/2012.
- Guodong Li and Ganesh Gopalakrishnan, “Parameterized Verification of GPU Kernels,” PLC Work- shop 2012 (An IPDPS 2012 Workshop). Published, 07/01/2012.
- Ganesh Gopalakrishnan, “Formal Methods for Surviving the Jungle of Heterogeneous Parallelism,” EduPar (An IPDPS 2012 Workshop). Published, 07/01/2012.
- Ganesh Gopalakrishnan and Tyler Sorensen, “Integrating Formal Methods for Parallelism and Concurrency into Existing CS Curricula,” EduPar Poster (An IPDPS 2012 Workshop). Published, 07/01/2012.
- Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan, “GKLEE: Concolic Verification and Test Generation for GPUs,” Principles and Practices of Parallel Programming (PPoPP), February, 2012. Published, 02/01/2012.
- Ganesh Gopalakrishnan, Robert M. Kirby, Stephen Siegel, Rajeev Thakur, William Gropp, Ewing Lusk, Bronis R. de Supinski, Martin Schulz, and Greg Bronevetsky, “Formal Analysis of MPI-Based Parallel Programs: Present and Future,” Communications of ACM, December 2011.
Published, 12/01/2011.
http://cacm.acm.org/magazines/2011/12 - Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Bronis R. de Supinski, Martin Schulz, and Greg Bronevetsky, “Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update,” Parallel Architectures and Compilation Techniques (PACT), Galveston, TX, October 2011.
Published, 10/01/2011.
http://www.cs.utah.edu/fv - Caitlin Sadowski, Thomas Ball, Judith Bishop, Sebastian Burckhardt, Ganesh Gopalakrish- nan, Joseph Mayo, Madanlal Musuvathi, Shaz Qadeer, and Stephen Toub, “Practical Parallel and Concurrent Programming,” ACM SIGCSE, Waikiki, May 2011.
Published, 05/01/2011.
http://www.cs.utah.edu/fv - Stephen F. Siegel and Ganesh Gopalakrishnan, “Formal Analysis of Message Passing,” Invited Tutorial Paper, pages 2-18, Verification, Model Checking and Abstract Interpretation 2011, Austin, TX.
Published, 01/01/2011.
http://www.cs.utah.edu/fv - Ganesh L. Gopalakrishnan and Robert M. Kirby, Top Ten Ways to make Formal Methods for HPC Practical, 2010 FSE/SDP Workshop on the Future of Software Engineering Research, Santa Fe, NM, November, ACM, http://www.cs.utah.edu/formal verification/pdf/sdp2010-workshop.pdf, 2010.
Published, 11/01/2010.
http://www.cs.utah.edu/fv - Anh Vo, Sriram Aananthakrishnan, Ganesh Gopalakrishnan, Bronis R. de Supinski, Martin Schulz, and Greg Bronevetsky, “A Scalable and Distributed Dynamic Formal Verifier for MPI Programs,” Supercomputing 2010, New Orleans, LA. http://www.computer.org/portal/web/csdl/doi/10.1109/SC.2010.7.
Published, 11/01/2010.
http://www.cs.utah.edu/fv - Guodong Li and Ganesh Gopalakrishnan, Scalable SMT-based verification of GPU kernel functions, Foundations of Software Engineering, 2010, http://www.cs.utah.edu/fv/PUG, 187- 196.
Published, 11/01/2010.
http://www.cs.utah.edu/fv - Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan and Robert M. Kirby, “Distributed dynamic partial order reduction,” Journal on Software Tools for Technology Transfer, Volume 12, Issue 2 (2010), Page 113-122.
Published, 09/01/2010.
http://www.cs.utah.edu/fv - Alan Humphrey, Christopher Derrick, Ganesh Gopalakrishnan, and Beth R. Tibbitts, “GEM: Graphical Explorer for MPI Programs,” Parallel Software Tools and Tool Infrastructures (ICPP workshop), http://www.cs.utah.edu/fv/GEM, 2010.
Published, 09/01/2010.
http://www.cs.utah.edu/fv/GEM - Wei-Fan Chiang, Grzegorz Szubzda, Ganesh Gopalakrishnan, and Rajeev Thakur, “Dynamic Verification of Hybrid Programs,” EuroMPI, 2010, LNCS 6305, 298-301, Stuttgart, Germany.
Published, 09/01/2010.
http://www.cs.utah.edu/fv - Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, and Robert Kirby, “Precise Dynamic Analysis for Slack Elasticity: Adding Buffer Without Adding Bugs,” Recent Advances in the Message Passing Interface, 17th European MPI Users’ Group Meeting, EuroMPI 2010, September 2010, LNCS 6305, 152-159, Stuttgart, Germany.
Published, 09/01/2010.
http://www.cs.utah.edu/fv - Guodong Li, Robert Palmer, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, “Formal Specification of MPI 2.0: Case Study in Specifying a Practical Concurrent Programming API,” Electronic Edition Available at DOI URL http://dx.doi.org/10.1016/j.scico.2010.03.007, 2010.
Published, 08/01/2010.
http://dx.doi.org/10.1016/j.scico.2010.03.007, 201... - Anh Vo, Ganesh Gopalakrishnan, Sarvani Vakkalanka, Alan Humphrey and Christopher Derrick, “Seamless Integration of Two Approaches to Dynamic Formal Verification of MPI Programs,” Workshop on Advances in Message Passing, 2010.
Published, 06/01/2010.
http://www.cs.utah.edu/fv - Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou, “Efficient Methods for Formally Verifying Safety Properties of Hierarchical Cache Coherence Protocols,” Formal Methods in System Design, Volume 36, Number 1, February, 2010, Pages 37-64.
Published, 02/01/2010.
http://www.cs.utah.edu/fv - Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, “Formal methods applied to high performance computing software design: a case study of MPI one-sided communication based locking,” Software: Practice and Experience, Published online December 2009, Hardcopy issue is 2010: Vol 40, Issue 1, Pages 23-43.
Published, 02/01/2010.
http://www.cs.utah.edu/fv - Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan, “A symbolic verifier for CUDA programs,” PPOPP 2010: 357-358.
Published, 01/01/2010.
http://www.cs.utah.edu/fv
Research Keywords
- Software Testing
- Parallel Programming
- Formal Semantics
Presentations
- Symbolic AD with conditionals for error and instability analysis,
Workshop on Program Synthesis for Scientific Computing, Argonne (on Zoom).
Invited Talk/Keynote,
Presented, 08/04/2020.
https://prog-synth-science.github.io/2020/#agenda - The Grass is Really Green on the Other Side:
Empirical vs. Rigorous in Floating-Point Precision Analysis,
Reproducibility, Resilience
.
Invited Talk/Keynote,
Presented, 05/07/2020.
https://icerm.brown.edu/events/htw-20-vp - Keynote in CnC Workshop, Salt Lake City, ``How to Sugarcoat System Resilience?''
.
Invited Talk/Keynote,
Presented, 12/03/2019.
https://cnc-workshop.github.io/cnc2019/ - Invited Talk in the ROSS 2019 workshop (part of the Supercomputing Conference, 2019), ``System Resilience: Amplify Failures, Detect, or Both?" . Invited Talk/Keynote, Presented, 06/25/2019.
- "Can Formal Methods (alone) Rescue HPC Debugging?'', Distinguished Lecture, Department of Computer Science, University of California, Davis, CA.
Invited Talk/Keynote,
Presented, 05/10/2019.
https://ucdavis.app.box.com/s/i1k1lwnrs9a0bycj2e7r... - Keynote lecture, ``Making Formal Methods for HPC Disappear,'' Correctness 2018: Second International Workshop on Software Correctness for HPC Applications, Held in conjunction with Supercomputing, 2018.
Invited Talk/Keynote,
Presented, 11/12/2018.
https://correctness-workshop.github.io/2018/#progr... - Taught a 5-day International Course on High-Performance Computing at the National Institute of Technology, Kozhikode (Calicut), Kerala, India. This was under the GIAN program (auspices of the Government of India) that was competitively selected through a proposal written by my local host at NIT Calicut, Dr. Jayaraj, and myself. Faculty and students at NIT Calicut as well as from across India attended this course.
Invited Talk/Keynote,
Presented, 10/08/2018.
http://www.nitc.ac.in/GIAN/HPCCP/ - Workshop "Lightning Keynote", Software Engineering for Computational Science and Engineering .
Invited Talk/Keynote,
Presented, 11/17/2016.
http://sc16.supercomputing.org/presentation/?id=bo... - Colloquium, Dept of Computer Science, University of Waterloo, Canada. Other, Presented, 01/04/2016.
- Panelist, SC15 BoF on "REPRODUCIBILITY OF HIGH PERFORMANCE CODES AND SIMULATIONS – TOOLS, TECHNIQUES, DEBUGGING".
Invited Talk/Keynote,
Presented, 11/17/2015.
https://gcl.cis.udel.edu/sc15bof.php - Colloquium at the Univ of British Columbia. Invited Talk/Keynote, Presented, 06/01/2015.
- Colloquium at the Aalto University, Helsinki. Invited Talk/Keynote, Presented, 02/09/2015.
- Matthias S. Mu ̈ller, David Lecomber, Tobias Hilbrich, Mark OConnor, Bronis R. de Supinski, and Ganesh Gopalakrishnan, “Efficient Parallel Debugging for MPI, Threads, and Beyond” Full Day Tutorial, Supercomputing, New Orleans, November 2014. Other, Presented, 11/17/2014.
- Colloquium at Imperial College, London, November 2014. Invited Talk/Keynote, Presented, 11/04/2014.
- Diego Caminha B de Oliveira, Alan Humphrey, Qingyu Meng, Zvonimir Rakamaric, Martin Berzins and Ganesh Gopalakrishnan, “Systematic Debugging of Concurrent Systems Using Coalesced Stack Trace Graphs,” LCPC 2014. Conference Paper, Refereed, Presented, 09/01/2014.
- Invited Speaker, Challenges in 21st Century Experimental Mathematical Computation (July 21-25, 2014), Providence, RI. Invited Talk/Keynote, Presented, 07/21/2014.
- Invited talk on research, Microsoft Research, Redmond, WA, May 2014. Invited Talk/Keynote, Presented, 05/16/2014.
- Invited talk, Pacific Northern National Laboratory, Richland, WA, May 2014. Invited Talk/Keynote, Presented, 05/15/2014.
- Formal Methods for Parallel Computing, given at Washington University, St. Louis. Invited Talk/Keynote, Presented, 11/2013.
- Formal Methods for High Performance Computing, given at IISc Bangalore, India. Invited Talk/Keynote, Presented, 06/2013.
- Invited tutorial, Ganesh Gopalakrishnan, Matthias S. Mu ̈ller, Bronis R. de Supinski, David LeComber, “Scal- able Dynamic Formal Verification and Correctness Checking of MPI Applications,” Full Day Tutorial, Supercomputing, Seattle, Nov, 2011.
Other,
Presented, 11/01/2011.
http://www.cs.utah.edu/fv - Invited Talk, Haifa Verification Seminar, sponsored by Intel, Sep 2011.
Invited Talk/Keynote,
Presented, 09/13/2011.
http://www.cs.utah.edu/fv - Invited tutorial (2 one-hour lectures), UPMARC Summer School, Boson, Sweden, June 2011. Organized by Uppsala University, Sweden.
Invited Talk/Keynote,
Presented, 06/01/2011.
http://www.cs.utah.edu/fv - Ganesh Gopalakrishnan, Matthias S. Mu ̈ller, and Bronis R. de Supinski, “Scalable Dynamic Formal Verification and Correctness Checking of MPI Applications,” Half Day Tutorial, Supercomputing, New Orleans, Nov 15, 2010.
Other,
Presented, 11/01/2010.
http://www.cs.utah.edu/fv - Ganesh Gopalakrishnan, “Tutorial: Dynamic Verification of Message Passing and Threading,” PPoPP, Bangalore, January 2010.
Other,
Presented, 01/01/2010.
http://www.cs.utah.edu/fv - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - Guodong Li, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby,
``Formal Specification of the MPI-2.0 Standard in TLA+,''
Poster Paper, Principles and Practices of Parallel Programming (PPoPP),
283-284, 2008.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - 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.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - Sarvani Vakkalanka, Subodh V. Sharma, Ganesh Gopalakrishnan,
and Robert M. Kirby,
``ISP: A Tool for Model Checking MPI Programs,''
Poster Paper, Principles and Practices of Parallel Programming (PPoPP),
285-286, 2008.
Conference Paper,
Other, 2008.
http://www.cs.utah.edu/formal_verification - ``Inspect, ISP, and FIB: reduction-based verification and analysis
tools for
concurrent programs,''
talk given at Microsoft Research, Bangalore, India, June 6, 2008.
Invited Talk/Keynote,
Presented, 2008.
http://www.cs.utah.edu/formal_verification - Ganesh Gopalakrishnan and Yu Yang,
``Runtime Model Checking of Multithreaded C Programs using
Automated Instrumentation Dynamic Partial Order Reduction and
Distributed Checking,''
Half Day tutorial at
{\sl FM'08: 15th International Symposium on Formal Methods},
May 26 - 30, 2008, Abo Akademi University,
Turku, Finland.
Invited Talk/Keynote,
Presented, 2008.
http://www.cs.utah.edu/formal_verification - ``Inspect, ISP, and FIB:
Tools for dynamic analysis of MPI and Thread programs,''
talk given at the Dagstuhl Meeting 08332, {\sl Distributed Verification
and Grid Computing,} August 11, 2008.
Invited Talk/Keynote,
Presented, 2008.
http://www.cs.utah.edu/formal_verification
Research Groups
- FPBench, Other. 09/01/2020 - present. fpbench.org.
- Gauss Group, Other. School of Computing. 01/01/2014 - 02/01/2015.
- CPU Group - Center for Parallel Computing (or Compilers and Parallel Systems), Other. School of Computing. 07/01/2010 - 02/28/2030. www.parallel.utah.edu.
Geographical Regions of Interest
- Finland
I am supporting a Finnish visiting student Jarkko Savela during Summer 2016. I am hosting postdoc Anjum Omer Fall 2016 (Finnish supported). - India
- United Kingdom of Great Britain and Northern Ireland
Grants, Contracts & Research Gifts
- MCDA. PI: Ganesh Gopalakrishnan. http://www.cs.utah.edu/fv. SRC, 11/01/2009 - 10/31/2010. Total project budget to date: $15,000.00
Software Titles
- Satire. A rigorous floating-point error estimation tool. Release Date: 01/01/2021. Inventors: Arnab Das (PhD student), with new grad student Tanmay Tirpankar helping. http://formal.cs.utah.edu:8080/satire/. Distribution List: FPBench.org.
- Condensa. A Programmable Framework for Neural Network Compression. Release Date: 10/01/2020. Inventors: Vinu Joseph and coauthors in our IEEE Micro paper https://github.com/NVlabs/condensa#:~:text=Condensa%20is%20a%20framework%20for,hardware%20platform%2C%20and%20optimization%20objective. Distribution List: Nvidia publicizes this worldwide.
- FLiT (FLoating point LiTmus Tester). Floating-point Litmus Tests (FLiT) is a C++ test infrastructure for detecting variability in floating-point code caused by variations in compiler code generation, hardware and execution environments. It is used within the Lawrence Livermore National Laboratory in critical Export-Control Code to test whether it is safe to upgrade their compiler and/or port it to new machines, for fear of altering its numerics and invalidating prior simulation results. Release Date: 06/01/2019. Inventors: Michael Bentley, Ian Briggs, Ganesh Gopalakrishnan, Dong H. Ahn, Ignacio Laguna, and Gregory L. Lee. Distribution List: https://pruners.github.io/.
- FPTaylor. Computes floating-point precision rigorously. Release Date: 01/01/2019. Inventors: Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Zvonimir Rakamari\'c, and Ganesh Gopalakrishnan. Distribution List: https://github.com/soarlab/FPTaylor.
- Automaton Package Jove. Software that goes with my new book "Automata and Computability: A Programmer's Perspective". Release Date: 10/01/2018. Inventors: Authored by self. Distribution List: Public on Github at https://github.com/ganeshutah/Jove.git.
- Presage. Resilience solution to protect structured address generation. Release Date: 10/01/2016. Inventors: Vishal C. Sharma, Sriram Krishnamoorthy, Ganesh Gopalakrishnan. Distribution List: On Github at https://utahfmr.github.io/PRESAGE/.
- Archer: Data Race Checker for OpenMP. The first practical race-checker for OpenMP that has helped isolate and correct bugs in LLNL's Hypre package. Release Date: 03/01/2016. Inventors: Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamarić, Dong H. Anh, Ignacia Laguna, Martin Schulz, Gregory L. Lee, Joachim Protze, Matthias S. Muller. Distribution List: https://github.com/PRUNER/archer.
- VULFI: Vector mode Utah LLVM Fault Injector. First fault injector that simulates bit-flips in vector instruction sets. Release Date: 03/01/2016. Inventors: Vishal Sharma, Ganesh Gopalakrishnan, Sriram Krishnamoorthy. Distribution List: http://formalverification.cs.utah.edu/fmr/vulfi.
- GKLEE (SESA version). GKLEEp: Parameterized Concolic Analyzer of GPU Programs. AUTHORs: Peng Li. Release at http://www.cs.utah.edu/fv/GKLEE. GKLEEp is the only released symbolic execution based analyzer for GPU kernels that has successfully found bugs in leading benchmarks such as Parboil and Lonestar. Release Date: 11/01/2014. Inventors: Peng Li, Guodong Li, Ganesh Gopalakrishnan. Distribution List: http://www.cs.utah.edu/fv/GKLEE.
- CSTG. A Coalesced Stack Trace Graph tool (CSTG). AUTHOR: Postdoc Diego Oliveira. Release at http://www.cs.utah.edu/fv/CSTG. The CSTG tool supports differential verification by highlighting control-flow differences be- tween two versions of a concurrent system, and has been applied to a large-scale HPC com- putational framework. Release Date: 08/01/2014. Inventors: Diego Oliveira, Zvonimir Rakamaric', Ganesh Gopalakrishnan. Distribution List: http://www.cs.utah.edu/fv/CSTG.
- S3FP. S3FP, a search based floating-point precision analysis framework. AUTHOR: Wei-Fan Chiang (PhD student). Release at http://www.cs.utah.edu/fv/s3fp, 2014. S3FP is the first released tool for guided search over inputs to floating point functions that maximizes their exhibited round-off error. Release Date: 01/01/2014. Inventors: Wei-Fan Chiang, Alexey Solovyev, Zvonimir Rakamaric', Ganesh Gopalakrishnan. Distribution List: Website http://www.cs.utah.edu/fv.
- KULFI. KULFI: Kontrollable LLVM Fault Injector. AUTHORS: Vishal Sharma and Arvind Haran, co-supervised by Prof. Zvonimir Rakamari ́c. Release on Github and http://www.cs.utah.edu/fv/kulfi. KULFI is one of the first LLVM-level fault injectors that is in active use at the Lawrence Livermore National Laboratory and Louisiana State University for system resilience studies. Release Date: 01/01/2014. Inventors: Vishal C. Sharma, Arvind Haran, Zvonimir Rakamaric', Ganesh Gopalakrishnan. Distribution List: http://www.cs.utah.edu/fv/FMR.
- S3FP: Sour Spot Search for Floating Point. S3FP, a search based floating-point precision analysis framework, authored by Wei-Fan Chi- ang (PhD student), http://www.cs.utah.edu/fv/s3fp. This tool embodies the first heuris- tic random search based approach to measure the loss of precision due to lower floating point precision allocation. The tool is being evaluated by a group at Rice University. Release Date: 11/2013.
- Coalesced Stack Trace Graphs. CSTG, a Coalesced Stack Trace Graph tool authored by postdoc Diego Oliveira, http://www. cs.utah.edu/fv/CSTG. This is a tool that supports differential verification by highlighting differences in stack traces generated by two versions. Release Date: 11/2013.
- KULFI: Kontrollable LLVM Fault Injector,. authored by Vishal Sharma and Arvind Haran, co-supervised by Prof. Zvonimir Rakamari ́c. Release on Github. KULFI is being actively used by researchers at the Louisiana State University and Lawrence Livermore National Laboratory to support their own research. http://www.cs.utah.edu/fv/kulfi. Release Date: 05/2013.
- GKLEE. Concolic (Concrete + Symbolic) Verifier for GPU Programs. Release Date: 12/01/2011. Inventors: Main inventors are Guodong Li (original version), and in addition Peng Li, Ganesh Gopalakrishnan, and Geof Sawaya (current version). Additional : Tyler Sorensen, Brandon Gibson, Alan Humphrey. Distribution List: Website http://www.cs.utah.edu/fv/GKLEE.
- Graphical Explorer of Message Passing (GEM). Eclipse IDE Plug-in for the ISP Tool. Release Date: 12/01/2009. Inventors: Alan Humphrey, Christopher Derrick, and Ganesh Gopalakrishnan. Distribution List: Formally included as part of the Eclipse Parallel Tools Platform Release (PTP 3.0) .
- Distributed MPI Analyzer (DMA). A distributed implementation of our ISP tool. Release Date: 12/01/2009. Inventors: Anh Vo, Ganesh Gopalakrishnan, Bronis R. de Supinski, Martin Schulz, Greg Bronevetsky. Distribution List: Released only to LLNL at this point.
- Multicore Communications API Checker (MCC). A Dynamic Verifier for Multicore Communications API programs. Release Date: 12/01/2009. Inventors: Subodh Sharma, Ganesh Gopalakrishnan. Distribution List: Released to collaborators at BYU.
- Prover of User GPU Programs (PUG). A Race Checker for CUDA Kernels. Release Date: 11/01/2009. Inventors: Guodong Li, Ganesh Gopalakrishnan. Distribution List: Available upon request.
- ISP: A Formal Verification tool for MPI Programs. ISP formally verifies MPI programs. It is a huge and ongoing effort of our group. We made a major release which is now described. ISP runs under Linux, Microsoft Visual Studio With MPI libraries MPICH2, OpenMPI, Microsoft MPI With significant user interfaces in Java and Visual Studio User manuals for the Linux and Microsoft sides With over 150 pedagogical examples. Release Date: 12/01/2008. Inventors: Sarvani Vakkalanka, Anh Vo, Michael DeLisi, Sriram Aananthakrishnan, Subodh Sharma. PI: Ganesh Gopalakrishnan. Co-PI: Robert M. Kirby. Distribution List: Several scientists and close associates. Also will be releasing through major download sites for MPI.
- Inspect: Formal Verification tool for Pthread C programs. Inspect formally verifies Pthread C programs for safety properties. Release Date: 12/01/2008. Inventors: Yu Yang, with some help from Xiaofang Chen and Greg Szubzda. Distribution List: Several close associates. Also, a half-day tutorial on Inspect was offered at FM 2008, Turku, Finland.