Computers are amazingly fun and useful, but why do they crash and hang? Why are they so terrifyingly insecure? The problem is many-faceted, but an important aspect is that people who develop software must consider a huge number of possible executions of their code, and the human mind doesn't turn out to be all that good at this. Even a single execution of a medium-sized piece of software can be mind-numbingly complex, requiring many hours before an expert can understand what is going on.

The part of the solution to the software problem that I am most interested in is using software tools to make it easier to develop correct and efficient software. Basically, we can create programs to show us possibilities inherent in our software -- such as crashes -- that we did not know about, or better yet create programs to verify that such possibilities do not exist. Similarly, good abstractions such as high-level programming languages make it easier to express our intent, and then we can offload to software tools the problem of making programs run quickly.

The software tool developed by my group that I am most proud of is Csmith, which generates random C programs; here is a fragment of one. Although it sounds easy to generate random code, it is not: C has hundreds of rules that must be followed, and violating any one of them renders the randomly generated code useless. Over several years we used Csmith to find serious bugs in every compiler that we tested, including those that are used to compile safety-critical avionics software. The worst kind of compiler bug, and the kind we specialized in finding, causes the compiler to silently generate incorrect executable code. We found so many bugs (around 500) that we had to write a new tool, C-Reduce, to take large programs that trigger compiler bugs and reduce them to tiny programs that people can understand. Since Csmith is open source software, everyone is free to use it. One time Csmith received a Christmas card from a development team at a compiler company!

(Top)

• Github page, where my group's recent software lives, including: Souper, a synthesis-based superoptimizer for LLVM; C-Reduce, a test-case reducer for C, C++, and OpenCL; and, Csmith, a random C program generator that helped us discover and report hundreds of bugs in production-quality compilers.
• Blog, where I post mostly-technical content that doesn't seem to belong in peer-reviewed publications. I've found that people are a lot more likely to read a blog post than a paper!
• Google Scholar and DBLP pages.
• CV.
• Personal web page.

(Top)

Recent Teaching

• CS 6475, Advanced Compilers, Fall 2024
• CS 1810, Intro to Computing Systems, Spring 2024
• CS 4500, Senior Capstone Project, Fall 2023
• CS 4500, Senior Capstone Project, Spring 2022
• CS 6465, Advanced Operating Systems, Fall 2021
• CS 4470, Intro to Compilers, Spring 2021

(Top)

Papers

• Minotaur: A SIMD-Oriented Synthesizing Superoptimizer. Zhengyang Liu, Stefan Mada, and John Regehr. 2024. In Object-oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2024.
• Hydra: Generalizing Peephole Optimizations with Program Synthesis. Manasij Mukherjee and John Regehr. 2024. In Object-oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2024.
• High-Throughput, Formal-Methods-Assisted Fuzzing for LLVM. Yuyou Fan and John Regehr. 2024. In Proceedings of the International Symposium on Code Generation and Optimization (CGO), March 2024.
• Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages. Vsevolod Livinskii, Dmitry Babokin, and John Regehr. 2023. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), June 2023.
• Alive2: Bounded Translation Validation for LLVM. Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021), June 2021.
• Dataflow-based Pruning for Speeding up Superoptimization. Manasij Mukherjee, Pranav Kant, Zhengyang Liu, John Regehr. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020, November 2020.
• Random Testing for C and C++ Compilers with YARPGen. Vsevolod Livinskii, Dmitry Babokin, and John Regehr. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020, November 2020.
• Testing Static Analyses for Precision and Soundness. Jubi Taneja, Zhengyang Liu, and John Regehr. In Proceedings of the International Symposium on Code Generation and Optimization (CGO) 2020, San Diego, CA, USA, February 2020.
• Future Directions for Optimizing Compilers. Nuno P. Lopes and John Regehr.
• Reconciling High-level Optimizations and Low-level Code in LLVM. Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, and Nuno P. Lopes. In OOPSLA 2018. (Supplementary material.)
• Practical Verification of Peephole Optimizations with Alive. Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Communications of the ACM. Volume 61 Issue 2, February 2018.
• Souper: A Synthesizing Superoptimizer. Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, John Regehr. arXiv paper. Revised April 2018.
• Research for practice: vigorous public debates in academic computer science. John Regehr. Communications of the ACM. Volume 60 Issue 12, December 2017.
• Taming Undefined Behavior in LLVM. Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. In Proceedings of 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), Barcelona, Spain, June 2017.
• Abstractions for Practical Virtual Machine Replay. Anton Burtsev, David Johnson, Mike Hibler, Eric Eide, and John Regehr. In Proceedings of the 12th International Conference on Virtual Execution Environments (VEE'16), Atlanta, GA, USA, April 2016.
• Cause reduction: delta debugging, even without bugs. Alex Groce, Mohammad Amin Alipour, Chaoqiang Zhang, Yang Chen, and John Regehr. In Software Testing, Verification and Reliability, Volume 26 Issue 1, January 2016.
• Understanding Integer Overflow in C/C++. Will Dietz, Peng Li, John Regehr, and Vikram Adve. ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 25, Issue 1, November 2015. (ACM link.) This is an updated and expanded version of our ICSE 2012 paper.
• Deniable Backdoors Using Compiler Bugs. Scotty Bauer, Pascal Cuoq, and John Regehr. International Journal of PoC||GTFO 0x08, June 2015.
• Provably Correct Peephole Optimizations with Alive. Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. In Proceedings of 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), Portland, OR, USA, June 2015. This paper won a Distinguished Paper Award.
• Intent fuzzer: crafting intents of death. Raimondas Sasnauskas and John Regehr. In Proceedings of the 2014 Joint International Workshop on Dynamic Analysis (WODA) and Software and System Performance Testing, Debugging, and Analytics (PERTEA). San Jose, CA, USA, July 2014.
• Cause Reduction for Quick Testing. Alex Groce, Amin Alipour, Chaoqiang Zhang, Yang Chen, and John Regehr. In IEEE International Conference on Software Testing, Verification and Validation (ICST), Cleveland, Ohio, March-April 2014. (ICST 2014 Best Paper Award)
• Help, help, I'm being suppressed! The significance of suppressors in software testing. Alex Groce, Chaoqiang Zhang, Mohammad Amin Alipour, Eric Eide, Yang Chen, John Regehr. In Proceedings of the 24th International Symposium on Software Reliability Engineering (ISSRE), Pasadena, CA, USA, November 2013.
• Taming Compiler Fuzzers. Yang Chen, Alex Groce, Chaoqiang Zhang, Weng-Keen Wong, Xiaoli Fern, Eric Eide, and John Regehr. In Proceedings of 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013), Seattle, WA, USA, June 2013.
• Swarm Testing. Alex Groce, Chaoqiang Zhang, Eric Eide, Yang Chen, and John Regehr. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA 2012), Minneapolis, MN, USA, July 2012.
• Test-Case Reduction for C Compiler Bugs. John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. In Proceedings of 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012), Beijing, China, June 2012.
• Understanding Integer Overflow in C/C++. Will Dietz, Peng Li, John Regehr, and Vikram Adve. In Proceedings of the 34th International Conference on Software Engineering (ICSE 2012). Zurich, Switzerland, June 2012. (ACM SIGSOFT Distinguished Paper Award)
• Testing static analyzers with randomly generated programs. Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, and Xuejun Yang. Short paper in Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012). Norfolk, Virginia, USA, April 2012.
• Advanced Adaptive Application (A3) Environment: Initial Experience. Partha Pal, Rick Schantz, Aaron Paulos, John Regehr, and Mike Hibler. In Proceedings of the Middleware 2011 Industry Track Workshop (Middleware '11), New York, NY, USA. December 2011.
• 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.
• 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.
• Finding and Understanding Bugs in C Compilers. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. In Proceedings of 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011). San Jose, CA, USA, June 2011.
• 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. Slides.
• 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.
• 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.
• 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.
• 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.
• 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
• 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. Software page.
• 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.
• Runtime Verification for Wireless Sensor Network Applications. Usa Sammapun, John Regehr, Insup Lee, and Oleg Sokolsky. In Proceedings of the Dagstuhl Seminar 07011 on Runtime Verification.
• Efficient Memory Safety for TinyOS. Nathan Cooprider, William Archer, Eric Eide, David Gay, John Regehr. In Proceedings of the 5th ACM Conference on Embedded Networked Sensor Systems (SenSys 2007), Sydney, Australia, November 2007.
• High Confidence TinyOS. John Regehr and Phil Levis. In Proceedings of the Composable and Systems Technology for High Confidence Cyber-Physical Systems Workshop, Arlington, VA, July 2007.
• Offline Compression for On-Chip RAM. Nathan Cooprider and John Regehr. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI 2007), San Diego, CA, June 2007.
• Interface Contracts for TinyOS. Will Archer, Philip Levis, and John Regehr. In Proceedings of the International Conference on Information Processing in Sensor Networks (IPSN) 2007, SPOTS track, Cambridge, MA, April 2007.
• Safe and Structured Use of Interrupts in Real-Time and Embedded Software. John Regehr. Chapter in Handbook of Real-Time and Embedded Systems, CRC Press, 2007.
• Atomicity and Visibility in Tiny Embedded Systems. John Regehr, Nathan Cooprider, and David Gay. In Proceedings of the PLOS 2006 Workshop on Linguistic Support for Modern Operating Systems, San Jose, CA, October 2006.
• Efficient Type and Memory Safety for Tiny Embedded Systems. John Regehr, Nathan Cooprider, Will Archer, and Eric Eide. In Proceedings of the PLOS 2006 Workshop on Linguistic Support for Modern Operating Systems, San Jose, CA, October 2006.
• Thread Verification vs. Interrupt Verification. John Regehr. In Proceedings of the Workshop on Multithreading in Hardware and Software: Formal Approaches to Design and Verification (TV06), Seattle, WA, August 2006.
• Teaching Reliability. John Regehr. IEEE Distributed Systems Online, vol. 7, no. 5, 2006, art. no. 0605-o5002.
• Pluggable Abstract Domains for Analyzing Embedded Software. Nathan Cooprider and John Regehr. In Proceedings of the ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Canada, June 2006.
• Deriving Abstract Transfer Functions for Analyzing Embedded Software. John Regehr and Usit Duongsaa. In Proceedings of the ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Canada, June 2006.
• Eliminating stack overflow by abstract interpretation. John Regehr, Alastair Reid, and Kirk Webb. (An expanded and revised version of our EMSOFT 2003 paper.) ACM Transactions on Embedded Computing Systems, 4(4):751-778, November 2005.
• Random testing of interrupt-driven software. John Regehr. In Proceedings of the ACM Conference on Embedded Software (EMSOFT), Jersey City, NJ, September 2005.
• Preventing interrupt overload. John Regehr and Usit Duongsaa. In Proceedings of the ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2005), Chicago, IL, June 2005.
• Say No To Stack Overflow. John Regehr. Embedded Systems Programming, 17(10), October 2004. (Cover article!)
• HOIST: A system for automatically deriving static analyzers for embedded systems. John Regehr and Alastair Reid. In Shubu Mukherjee and Kathryn S. McKinley, editors, Proceedings of the Eleventh International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XI), pages 133-143, Boston, MA, October 9-13 2004. ISBN 1-58113-804-0.
• Dynamic CPU Management for Real-Time, Middleware-Based Systems. Eric Eide, Tim Stack, John Regehr, and Jay Lepreau. In Proceedings of the 10th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Toronto, Canada, May 25-28 2004.
• Evolving real-time systems using hierarchical scheduling and concurrency analysis. John Regehr, Alastair Reid, Kirk Webb, Michael Parker, and Jay Lepreau. In Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS 2003), Cancun, Mexico, December 3-5 2003.
• Vertically integrated analysis and transformation for embedded software. John Regehr. In Proceedings of the 2003 Workshop on Compilers and Tools for Constrained Embedded Systems (CTCES), San Jose, CA, October 29 2003.
• Eliminating stack overflow by abstract interpretation. John Regehr, Alastair Reid, and Kirk Webb. In Proceedings of the Third International Conference on Embedded Software (EMSOFT 2003), Philadelphia, PA, October 15-17 2003. Also see the Stacktool page.
• Lock inference for systems software. John Regehr and Alastair Reid. In Proceedings of the Second AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software (ACP4IS), Boston, MA, March 17 2003.
• How to Rapidly Prototype a Real-Time Scheduler. Luca Abeni and John Regehr. In the Work in Progress session of the 23rd IEEE Real-Time Systems Symposium (RTSS 2002), Austin, TX, December 3-5 2002.
• Scheduling Tasks with Mixed Preemption Relations for Robustness to Timing Faults, John Regehr. In Proceedings of the 23rd IEEE Real-Time Systems Symposium (RTSS 2002), Austin, TX, December 3-5 2002.
• Inferring Scheduling Behavior with Hourglass, John Regehr. In Proceedings of the 2002 USENIX Annual Technical Conference FREENIX track, Monterey, CA, June 10-15 2002.
• Static and Dynamic Structure in Design Patterns, Eric Eide, Alastair Reid, John Regehr, and Jay Lepreau. In Proceedings of the 2002 International Conference on Software Engineering (ICSE), Orlando, FL, May 19-25 2002.
• HLS: A Framework for Composing Soft Real-Time Schedulers, John Regehr and John A. Stankovic. In Proceedings of the 22nd IEEE Real-Time Systems Symposium (RTSS 2001), London, UK, December 3-6 2001.
• The Case for Using Middleware to Manage Diverse Soft Real-Time Schedulers, John Regehr and Jay Lepreau. In Proceedings of the International Workshop on Multimedia Middleware (M3W '01), Ottawa, Canada, October 2001.
• Augmented CPU Reservations: Towards Predictable Execution on General-Purpose Operating Systems, John Regehr and John A. Stankovic. In Proceedings of the 7th Real-Time Technology and Applications Symposium (RTAS 2001), Taipei, Taiwan, May 30-June 1 2001.
• Two Case Studies in Predictable Application Scheduling Using Rialto/NT, Michael B. Jones, John Regehr, and Stefan Saroiu. In Proceedings of the 7th Real-Time Technology and Applications Symposium (RTAS 2001), Taipei, Taiwan, May 30-June 1 2001.
• Using Hierarchical Scheduling to Support Soft Real-Time Applications on General-Purpose Operating Systems, John Regehr. PhD thesis, University of Virginia, May 2001.
• Predictable Scheduling for Digital Audio, Michael B. Jones and John Regehr. Microsoft Research Technical Report MSR-TR-2000-87, December 2000.
• CPU Reservations and Time Constraints: Implementation Experience on Windows NT, Michael B. Jones and John Regehr. In Proceedings of the 3rd USENIX Windows NT Symposium, Seattle, WA, July 1999.
• The Problems You're Having May Not Be the Problems You Think You're Having: Results from a Latency Study of Windows NT, Michael B. Jones and John Regehr. In Proceedings of the 7th Workshop on Hot Topics in Operating Systems (HotOS VII), Rio Rico, AZ, March 1999.
• Issues in Using Commodity Operating Systems for Time-Dependent Tasks: Experiences from a Study of Windows NT, Michael B. Jones and John Regehr. In Proceedings of the 8th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV 98), Cambridge, England, July 1998.
• An Isotach Implementation for Myrinet, John Regehr. Department of Computer Science, University of Virginia Technical Report CS-97-12, May 1997. (TR version of my masters work)

(Top)

Please address me as Dr Regehr, Professor Regehr, or John. My pronouns are he/him.

I prefer to avoid phone calls and video chats with people I don't know yet; I can be contacted at regehr@cs.utah.edu. My office is MEB 4148 (map). Feel free to drop in any time my door's open. If I'm too busy to talk I'll let you know, and we'll find a different time. It's pretty common for me to be traveling or working from home -- if you're having trouble finding me, send email and we'll sort things out.

Some contact information can be found at the bottom of the Utah CS web site. If it's an emergency and you can't reach me any other way, it may be useful to contact the Utah CS front office or mail my wife sarah.creem@psych.utah.edu.

(Top)