Ganesh Gopalakrishnan
  • Director, Center for Parallel Computing at Utah (CPU)
  • Professor, School Of Computing

Publications

  • Ganesh L. Gopalakrishnan (date unknown). Automata and Computability: A Programmer's Perspective. (pp. 328). CRC Press. Accepted, .
  • Joachim Protze (date unknown). 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 Appli... LLVM Compiler Infrastructure in HPC Workshop. Accepted, .
  • Peng Li (date unknown). Peng Li, Guodong Li, and Ganesh Gopalakrishnan, “Practical Symbolic Checking of GPU Programs,” Supercomputing (SC 2014). Practical Symbolic Checking of GPU Programs: Supercomputing. Accepted, .
  • Mohammed Saeed Al-Mahfoudh (date unknown). 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. Workshop on Formal Methods in Software Engineering (FormaliSE). Accepted, .
  • Vishal C. Sharma (date unknown). 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. The 23rd annual IEEE International Conference on High Performance Computing, Data, and Analytics (HiPC). Accepted, .
  • Sriram Aananthakrishnan (date unknown). 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. The 29th International Workshop on Languages and Compilers for Parallel Computing (LCPC). Accepted, .
  • Tyler Sorensen (date unknown). 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. Accepted, .
  • Vishal C. Sharma (date unknown). 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. <... 19th IEEE Pacific Rim International Symposium on Dependable Computing. Accepted, .
  • Peng Li (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • Anh Vo (date unknown). 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. Accepted, .
  • Diego Oliveira (date unknown). 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. ... Systematic Debugging of Concurrent Systems Using Coalesced Stack Trace Graphs. Accepted, .
  • Subodh Sharma (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). Wei-Fan Chiang, Grzegorz Szubzda, Ganesh Gopalakrishnan, and Rajeev Thakur, “Dynamic Verification of Hybrid Programs,” EuroMPI, 2010, LNCS 6305, 298-301, Stuttgart, Germany. Accepted, .
  • Solovyev et al (date unknown). 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. Taylor Expansions. Accepted, .
  • Simone Atzeni (date unknown). 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. ARCHER: Effectively Spotting Data Races in Large OpenMP. Accepted, .
  • Wei-Fan Chiang (date unknown). 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. Accepted, .
  • Vishal C. Sharma (date unknown). 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. 21st IEEE Workshop on Dependable Parallel Distributed and Network-Centric Systems (DPDNS). Accepted, .
  • Mohammed Saeed Al-Mahfoudh (date unknown). Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman, ``Toward Bringing Distributed Systems Design upon Rigorous Footing,'' Workshop on Formal Methods and Integration (FMi). 2016. Accepted, .
  • Caitlin Sadowski (date unknown). 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. Accepted, .
  • Alglave et al (date unknown). 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. GPU concurrency: Weak behaviours and programming assumption. Accepted, .
  • Vishal Chandra Sharma (date unknown). 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. 10th Workshop on Silicon Errors in Logic - System Effects (SELSE). Accepted, .
  • Wei-Fan Chiang (date unknown). 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.... Principles and Practices of Parallel Programming (PPoPP). Accepted, .
  • Guodong Li (date unknown). 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. Accepted, .
  • Stephen Siegel (date unknown). 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. Accepted, .
  • (date unknown). Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan, “A symbolic verifier for CUDA programs,” PPOPP 2010: 357-358. Accepted, .
  • First author (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • Alan Humphrey (date unknown). Alan Humphrey, Qingyu Meng, Martin Berzins, Diego Caminha B. de Oliveira, Zvonimir Rakamari ́c, and Ganesh Gopalakrishnan, “Systematic Debugging Methods for Large Scale HPC Computational Frameworks,” accepted by the IEEE Computing in Science and Engi- neering Magazine (IEEE Compute... Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). 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. Accepted, .
  • (date unknown). Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, ``Formal Verification of Programs that use MPI One-sided Communication,'' Software Practice and Experience. Accepted for publication. Accepted, .
  • Vinu Joseph, Saurav Muralidharan, Animesh Garg, Michael Garland, and Ganesh Gopalakrishnan (date unknown). A Programmable Approach to Model Compression. (pp. 13). arxiv. Accepted, .
  • Jacobsen et al. (date unknown). 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. Electronic Notes in Theoretical Computer Science. Accepted, .
  • Chiang et al (date unknown). 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. Workshop on Numerical Software Verification. Accepted, .
  • Tyler Sorensen (date unknown). 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. Proceedings of the 27th international ACM conference on International conference on supercomputing. Accepted, .
  • Sriram Aananthakrishnan (date unknown). 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. ... Accepted, .
  • Ganesh Gopalakrishnan (date unknown). Ganesh Gopalakrishnan, “Formal Methods for Surviving the Jungle of Heterogeneous Parallelism,” EduPar (An IPDPS 2012 Workshop). Accepted, .
  • Guodong Li (date unknown). Guodong Li and Ganesh Gopalakrishnan, “Parameterized Verification of GPU Kernels,” PLC Work- shop 2012 (An IPDPS 2012 Workshop). Accepted, .
  • Ganesh Gopalakrishnan (date unknown). Ganesh Gopalakrishnan and Tyler Sorensen, “Integrating Formal Methods for Parallelism and Concurrency into Existing CS Curricula,” EduPar Poster (An IPDPS 2012 Workshop). Accepted, .
  • (date unknown). 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. Accepted, .
  • Diego Caminha (date unknown). 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 a... 7th International Workshop on Software Engineering for Computational Science and Engineering. Accepted, .
  • Wei-Fan Chiang (date unknown). 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. ... Accepted, .

Research Keywords

  • Relaxation Phenomenon
  • Cosmochemistry

Presentations

  • Symbolic AD with conditionals for error and instability analysis, Workshop on Program Synthesis for Scientific Computing, Argonne (on Zoom). , Presented, 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. , Presented, 2020.
    https://icerm.brown.edu/events/htw-20-vp
  • Keynote in CnC Workshop, Salt Lake City, ``How to Sugarcoat System Resilience?''. , Presented, 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?". , Presented, 2019.
  • "Can Formal Methods (alone) Rescue HPC Debugging?'', Distinguished Lecture, Department of Computer Science, University of California, Davis, CA. , Presented, 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. , Presented, 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. , Presented, 2018.
    http://www.nitc.ac.in/GIAN/HPCCP/
  • Workshop "Lightning Keynote", Software Engineering for Computational Science and Engineering. , Presented, 2016.
    http://sc16.supercomputing.org/presentation/?id=bo...
  • Panelist, SC15 BoF on "REPRODUCIBILITY OF HIGH PERFORMANCE CODES AND SIMULATIONS – TOOLS, TECHNIQUES, DEBUGGING". , Presented, 2015.
    https://gcl.cis.udel.edu/sc15bof.php
  • Colloquium at the Univ of British Columbia. , Presented, 2015.
  • Colloquium at the Aalto University, Helsinki. , Presented, 2015.
  • Colloquium at Imperial College, London, November 2014. , Presented, 2014.
  • Invited Speaker, Challenges in 21st Century Experimental Mathematical Computation (July 21-25, 2014), Providence, RI. , Presented, 2014.
  • Invited talk on research, Microsoft Research, Redmond, WA, May 2014. , Presented, 2014.
  • Invited talk, Pacific Northern National Laboratory, Richland, WA, May 2014. , Presented, 2014.
  • Formal Methods for Parallel Computing, given at Washington University, St. Louis. , Presented, 2013.
  • Formal Methods for High Performance Computing, given at IISc Bangalore, India. , Presented, 2013.
  • Invited Talk, Haifa Verification Seminar, sponsored by Intel, Sep 2011. , Presented, 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. , Presented, 2011.
    http://www.cs.utah.edu/fv
  • 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. , 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. , Presented, 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. , Presented, 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. , Other, 2008.
    http://www.cs.utah.edu/formal_verification
  • 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. , 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. , 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. , 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. , 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. , 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. , 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. , Other, 2008.
    http://www.cs.utah.edu/formal_verification
  • Colloquium, Dept of Computer Science, University of Waterloo, Canada. Other, Presented, 2016.
  • 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, 2014.
  • 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, 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, 2010.
    http://www.cs.utah.edu/fv
  • Ganesh Gopalakrishnan, “Tutorial: Dynamic Verification of Message Passing and Threading,” PPoPP, Bangalore, January 2010. Other, Presented, 2010.
    http://www.cs.utah.edu/fv
  • 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. , Presented, 2014.

Research Groups

  • FPBench, . 2020 - present. fpbench.org.
  • Gauss Group, . School of Computing. 2014 - 2015.
  • CPU Group - Center for Parallel Computing (or Compilers and Parallel Systems), . School of Computing. 2010 - 2030. www.parallel.utah.edu.

Geographical Regions of Interest

  • India
  • United Kingdom
  • Finland
    I am supporting a Finnish visiting student Jarkko Savela during Summer 2016. I am hosting postdoc Anjum Omer Fall 2016 (Finnish supported).

Software Titles

  • Satire. A rigorous floating-point error estimation tool. Release Date: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 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: 2014. Inventors: Vishal C. Sharma, Arvind Haran, Zvonimir Rakamaric', Ganesh Gopalakrishnan. Distribution List: http://www.cs.utah.edu/fv/FMR.
  • 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: 2013.
  • 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: 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: 2013.
  • GKLEE. Concolic (Concrete + Symbolic) Verifier for GPU Programs. Release Date: 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.
  • Distributed MPI Analyzer (DMA). A distributed implementation of our ISP tool. Release Date: 2009. Inventors: Anh Vo, Ganesh Gopalakrishnan, Bronis R. de Supinski, Martin Schulz, Greg Bronevetsky. Distribution List: Released only to LLNL at this point.
  • Graphical Explorer of Message Passing (GEM). Eclipse IDE Plug-in for the ISP Tool. Release Date: 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) .
  • Multicore Communications API Checker (MCC). A Dynamic Verifier for Multicore Communications API programs. Release Date: 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: 2009. Inventors: Guodong Li, Ganesh Gopalakrishnan. Distribution List: Available upon request.
  • Inspect: Formal Verification tool for Pthread C programs. Inspect formally verifies Pthread C programs for safety properties. Release Date: 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.
  • 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: 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.