Awards

Recognition for research, software, and contributions to formal methods.

Awards and recognition

2021Formal Methods in Outer Space

A workshop and festschrift at ISoLA 2021, organized by Ezio Bartocci, Ylies Falcone, and Martin Leucker for my 65th birthday.

Workshop program · Proceedings

2020JPL Magellan Award

For excellence in research and contributions to runtime verification of software systems. September 2020; $10,000 prize.

2020SIGSOFT Impact Paper Award

Model checking programs, Willem Visser, Klaus Havelund, Guillaume Brat, and SeungJoon Park. Originally published at ASE 2000.

2018RV competition best benchmark

The DejaVu Runtime Verification Benchmark, K. Havelund, D. Peled, and D. Ulus. Awarded at the RV competition, affiliated with RV 2018, Limassol, Cyprus, November 10–13.

2018RV Test of Time Award

Monitoring Java Programs with Java PathExplorer, Klaus Havelund and Grigore Rosu. Originally presented at RV 2001, Paris, July 23; Electronic Notes in Theoretical Computer Science, 55(2).

2017JPL Voyager Award

For research contributions, including publications, tool development, and conference organization. August 2017.

2016ASE Most Influential Paper Award

Monitoring Programs using Rewriting, Klaus Havelund and Grigore Rosu. Originally published at ASE 2001. Award.

2015CRV competition winner — LogFire

LogFire won the offline log-analysis track of CRV 2015, held with RV 2015 in Vienna, September 22–25. Paper.

2014ASE Most Influential Paper Award

Model checking programs, Willem Visser, Klaus Havelund, Guillaume Brat, and SeungJoon Park. Originally published at ASE 2000. Award.

2011JPL Mariner Award

For establishing automated checking of C, C++, and Java coding standards at JPL. August 2011.

2011RV best paper

Runtime Verification with State Estimation, S. D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S. A. Smolka, and E. Zadok. RV 2011, San Francisco, October 27–30.

2010JPL Ranger Award

For developing a Java coding standard and its automated checker. July 2010.

2009JPL Mariner Award

For delivering LogScope to the Mars Science Laboratory testing team. The tool checks execution logs against formal specifications to support flight software testing. July 2009.

2009Outstanding Technology Development Award

For Java PathFinder, Federal Laboratory Consortium, Far West Region Awards. July 2009.

2008–2009Distinguished visiting fellowship

Royal Academy of Engineering fellowship at the University of Manchester.

2008ACM Distinguished Paper Award

Racer: Effective Race Detection Using AspectJ, Eric Bodden and Klaus Havelund. ISSTA 2008, Seattle, July.

2008NASA Group Achievement Award

Awarded to the Launch Control System Proof-of-Concept team for demonstrating an architecture for the Constellation Program's Command, Control and Communication Project at Kennedy Space Center. Signed by NASA Administrator Michael D. Griffin, May 8.

2006NASA Tech Brief contribution award

For contributing to ARC-15244-1, Automated Testing using Symbolic Execution and Temporal Monitoring, highlighting a NASA Ames innovation. September 2006.

2003Turning Goals Into Reality Award

NASA Office of Aerospace Technology Engineering Innovation Award for Java PathFinder. June 2003. Story.

2002EASST best software science paper

Synthesizing Monitors for Safety Properties, Klaus Havelund and Grigore Rosu. TACAS at ETAPS 2002, Grenoble, April.