John Regehr's Papers

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.
This paper received the 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.

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.

Memory Safety and Untrusted Extensions for TinyOS.
John Regehr, Nathan Cooprider, Will Archer, and Eric Eide.
Technical Report number UUCS-06-007, School of Computing, University of Utah, June 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.

Proofs as a substrate for tool integration supporting high-confidence embedded software.
John Regehr, Konrad Slind, and Elsa Gunter.
In Proceedings of the High Confidence Medical Device Software and Systems (HCMDSS) Workshop, Philadelphia, PA, June 2005.

The final project report for NSF Award CCR-0209185, "Composable Execution Environments: A Foundation for Building Robust Embedded Systems"
PI Jay Lepreau, co-PI John Regehr.
July 2002-June 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.

Compiling for Resource-Constrained Platforms using ASSHes: Application- and System-Specific Heuristics.
Alastair Reid, Nathan Cooprider, and John Regehr.
Unpublished draft, November 2004.

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.

High-Level Optimizations for Low-Level Software.
John Regehr.
Presented as a work in progress at the 19th ACM Symposium on Operating System Principles (SOSP), Bolton Landing, New York, October 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.

Task/Scheduler Logic: Reasoning about Concurrency in Component-Based Systems Software.
Alastair Reid and John Regehr.
September 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.

Composable Execution Environments,
John Regehr, Alastair Reid, Kirk Webb, and Jay Lepreau.
Flux Group Technical Note 2002-02, May 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.

Some Guidelines for Proportional Share CPU Scheduling in General-Purpose Operating Systems,
John Regehr.
Presented as a work in progress at 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.

Operating System Support for Multimedia: The Programming Model Matters,
John Regehr, Michael B. Jones, and John A. Stankovic.
Microsoft Research Technical Report MSR-TR-2000-89, September 2000.

The Case for Hierarchical Loadable Schedulers With Performance Guarantees,
John Regehr, John A. Stankovic, and Marty Humphrey.
Department of Computer Science, University of Virginia Technical Report CS-2000-07, March 2000.

Hierarchical Schedulers, Performance Guarantees, and Resource Management,
John Regehr and John A. Stankovic.
Presented as a work in progress at the 17th SOSP, Kiawah Island, South Carolina, December 1999. (Slides)

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.

Hierarchical Loadable Schedulers,
John Regehr.
PhD proposal, University of Virginia, April 1999. (PDF, Slides)

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.


Back to John's Homepage