JOHN REGEHR portrait
  • Professor, School Of Computing
please email instead

Publications

  • Vsevolod Livinskii (2023). Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages. ACM. Published, 06/2023.
    https://users.cs.utah.edu/~regehr/pldi23.pdf
  • Nuno P Lopes & Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu John, Regehr (2021). Alive2: Bounded Translation Validation for LLVM. ACM. Published, 06/2021.
    https://www.cs.utah.edu/~regehr/alive2-pldi21.pdf
  • Jubi Taneja (2020). Testing Static Analyses for Precision and Soundness. ACM. Published, 02/23/2020.
    http://www.cs.utah.edu/~regehr/cgo20.pdf
  • Nuno P. Lopes & David Menendez, Santosh Nagarakatte, and John Regehr (2018). Practical verification of peephole optimizations with Alive. ACM. Vol. 61. Published, 02/01/2018.
    https://dl.acm.org/citation.cfm?id=3166064
  • John Regehr & Peter Bailis (2017). Research for practice: vigorous public debates in academic computer science. ACM. Vol. 60. Published, 12/01/2017.
    https://dl.acm.org/citation.cfm?doid=3132257
  • Partha Pal, Rick Schantz, Aaron Paulos, John Regehr, and Mike Hibler. 2011. Advanced Adaptive Application (A3) Environment: initial experience. In Proceedings of the Middleware 2011 Industry Track Workshop (Middleware '11). ACM, New York, NY, USA. Published, 12/2011.
    http://dl.acm.org/citation.cfm?doid=2090181.209018...
  • ARMor: Fully Verified Software Fault Isolation. Lu Zhao, Guodong Li, Bjorn De Sutter, and John Regehr. In Proceedings of the 11th International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011. Published, 10/2011.
    http://www.cs.utah.edu/~regehr/papers/emsoft11.pdf
  • A Practical Logic Framework for Verifying Safety Properties of Executables. Lu Zhao, Guodong Li, and John Regehr. In Proceedings of the 2011 Workshop on Syntax and Semantics of Low-Level Languages (LOLA 2011). Toronto, Canada, June 2011. Published, 06/2011.
    http://www.cs.utah.edu/~regehr/papers/lola11.pdf
  • Finding and Understanding Bugs in C Compilers. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. To appear in Proceedings of 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011). San Jose, CA, USA, June 2011. Published, 01/2011.
    http://www.cs.utah.edu/~regehr/papers/pldi11-prepr...
  • Correctness Proofs for Device Drivers in Embedded Systems. Jianjun Duan and John Regehr. In Proceedings of the 5th International Workshop on Systems Software Verification (SSV), Vancouver, Canada, October 2010. Published, 10/2010.
    http://www.cs.utah.edu/~regehr/papers/ssv10.pdf
  • T-Check: Bug Finding for Sensor Networks. Peng Li and John Regehr. In Proceedings of the International Conference on Information Processing in Sensor Networks (IPSN), SPOTS track, Stockholm, Sweden, April 2010. Published, 04/2010.
    http://www.cs.utah.edu/~regehr/papers/ipsn553s-li....
  • Surviving Sensor Network Software Faults. Yang Chen, Omprakash Gnawali, Maria Kazandjieva, Philip Levis, and John Regehr. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP 2009), Big Sky, MT, USA, October 2009. Published, 2009.
    http://www.sigops.org/sosp/sosp09/papers/chen-sosp...
  • Eliminating the Call Stack to Save RAM. Xuejun Yang, Nathan Cooprider, and John Regehr. In Proceedings of the ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), Dublin, Ireland, June 2009. Published, 2009.
    http://www.cs.utah.edu/~regehr/papers/lctes062-yan...
  • Precise Garbage Collection for C. Jon Rafkind, Adam Wick, John Regehr, and Matthew Flatt. In Proceedings of the 2009 International Symposium on Memory Management (ISMM), Dublin, Ireland, June 2009. Published, 2009.
    http://www.cs.utah.edu/~regehr/papers/ismm15-rafki...

Research Keywords

  • Compilers

Presentations

  • "Building Compilers Using Data and Formal Methods.'' Programming Language Enthusiasts Mind Melt (PLEMM), September 2019. Invited Talk/Keynote, Presented, 09/01/2019.
  • Undefined Behavior in 2017. Invited Talk/Keynote, Presented, 10/01/2017.
    https://www.youtube.com/watch?v=v1COuU2vU_w
  • Testing Embedded Software. Keynote at the 2011 International Symposium on Software Testing and Analysis. Invited Talk/Keynote, Presented, 07/2011.
  • Finding and Understanding Bugs in C Compilers. Invited talk at the 18th International Workshop on Model Checking of Software, July 2011. Invited Talk/Keynote, Presented, 07/2011.
  • Exposing Difficult Compilers Bugs With Random Testing. Talk at the GCC Summit, Ottawa, Canada, October 2010. Other, Presented, 10/2010.
    http://blog.regehr.org/archives/289
  • Safety Analysis for Wireless Embedded Networks. Series of three lectures given at RWTH Aachen, February 17-19 2010. Invited Talk/Keynote, Presented, 02/2010.
    http://ds.informatik.rwth-aachen.de/teaching/ws091...
  • Edicts: Implementing Features with Flexible Binding Times. Venkat Chakravarthy, John Regehr, and Eric Eide. In Proceedings of the 7th International Conference on Aspect-Oriented Software Development (AOSD), Brussels, Belgium, March 2008. Conference Paper, Presented, 2008.
    http://www.cs.utah.edu/~regehr/papers/aosd08-prepr...
  • Volatiles Are Miscompiled, and What to Do about It. Eric Eide and John Regehr. In Proceedings of the ACM Conference on Embedded Software (EMSOFT), Atlanta, GA, October 2008. Conference Paper, Presented, 2008.
    http://www.cs.utah.edu/~regehr/papers/emsoft08-pre...
  • TinyOS 2.1: Adding Threads and Memory Protection to TinyOS. The TinyOS Alliance. Poster in Proceedings of The 6th ACM Conference on Embedded Networked Sensor Systems (SenSys '08). Raleigh, NC, November 2008 . Other, Presented, 2008.
    http://www.cs.utah.edu/~regehr/papers/t21poster.pd...

Grants, Contracts & Research Gifts

  • SHF: Small: Xsmith, A Configurable Generator of Highly Effective Fuzz Testers (1527638). PI: Eric N Eide. Co-PI(s): JOHN REGEHR. National Science Foundation, 2015 - 08/31/2018. Total project budget to date: $499,998.00
  • TWC: Small: XCap: Practical Capabilities and Least Authority for Virtualized Environments (1319076). PI: John D Regehr. National Science Foundation, 2013 - 09/30/2016. Total project budget to date: $499,912.00
  • CSR: Small: Beating Implementations of C++11 Concurrency Into Shape (1218022). PI: John D Regehr. National Science Foundation, 2012 - 08/31/2015. Total project budget to date: $467,740.00
  • SHF: Small: Collaborative Research: Diversity and Feedback in Random Testing for Systems Software (1218026). PI: John D Regehr. National Science Foundation, 2012 - 08/31/2015. Total project budget to date: $249,036.00
  • CRI: CRD: Keeping Emulab Tuned and Humming (0709427). PI: Regehr, John. National Science Foundation, 2007 - 08/31/2014. Total project budget to date: $1,999,873.00
  • MRI: Evolutionary Development of an Advanced Distributed Testbed (0723248). PI: Regehr, John. National Science Foundation, 2007 - 08/31/2013. Total project budget to date: $1,704,000.00
  • Collaborative Research: CSR---EHS: Improving Sensor Network Software Reliability through Language, Tool, and OS Co-Design (0615367). PI: Regehr, John. National Science Foundation, 2006 - 08/31/2009. Total project budget to date: $210,000.00
  • NeTS-FIND: Collaborative Research: Towards Complexity-Oblivious Network Management (0627086). PI: Regehr, John. National Science Foundation, 2006 - 08/31/2009. Total project budget to date: $300,000.00
  • CAREER: Vertically Integrated Program Analysis for Embedded Software (0448047). PI: Regehr, John. National Science Foundation, 2005 - 04/30/2010. Total project budget to date: $400,000.00

Software Titles

  • Alive. A verifier for LLVM optimizations. Release Date: 08/2014. Inventors: John Regehr, Nuno Lopes, David Menendez, Santosh Nagarakatte. Distribution List: https://github.com/nunoplopes/alive.
  • IOC. IOC is an integer overflow checker for C/C++ code. Release Date: 09/2011. Inventors: Will Dietz, Vikram Adve, Peng Li, John Regehr. Distribution List: http://embed.cs.utah.edu/ioc/.
  • Csmith. a random test case generator for finding C compiler bugs, which has resulted in the discovery and reporting of 425 compiler bugs so far. Release Date: 04/2011. Inventors: John Regehr, Eric Eide, Yang Chen, Xuejun Yang. Distribution List: http://embed.cs.utah.edu/csmith/.
  • Safe TinyOS. Support for type-safe compilation of TinyOS applications. Release Date: 08/22/2008. Inventors: John Regehr, Nathan Cooprider, William Archer, David Gay, Yang Chen.