• IEEE.org
  • IEEE CS Standards
  • Career Center
  • About Us
  • Subscribe to Newsletter

0

IEEE
CS Logo
  • MEMBERSHIP
  • CONFERENCES
  • PUBLICATIONS
  • EDUCATION & CAREER
  • VOLUNTEER
  • ABOUT
  • Join Us
CS Logo

0

IEEE Computer Society Logo
Sign up for our newsletter
IEEE COMPUTER SOCIETY
About UsBoard of GovernorsNewslettersPress RoomIEEE Support CenterContact Us
COMPUTING RESOURCES
Career CenterCourses & CertificationsWebinarsPodcastsTech NewsMembership
BUSINESS SOLUTIONS
Corporate PartnershipsConference Sponsorships & ExhibitsAdvertisingRecruitingDigital Library Institutional Subscriptions
DIGITAL LIBRARY
MagazinesJournalsConference ProceedingsVideo LibraryLibrarian Resources
COMMUNITY RESOURCES
GovernanceConference OrganizersAuthorsChaptersCommunities
POLICIES
PrivacyAccessibility StatementIEEE Nondiscrimination PolicyIEEE Ethics ReportingXML Sitemap

Copyright 2025 IEEE - All rights reserved. A public charity, IEEE is the world’s largest technical professional organization dedicated to advancing technology for the benefit of humanity.

  • Home
  • /Press Room
  • /News Archive
  • Home
  • /Press Room
  • /News Archive

2014 Mills Award to Holzmann

LOS ALAMITOS, Calif., 16 December 2014 – Gerard J. Holzmann, head of the Laboratory for Reliable Software at NASA's Jet Propulsion Laboratory, has been named recipient of the 2015 IEEE Computer Society Harlan D. Mills Award.

The Mills Award recognizes researchers and practitioners who have demonstrated longstanding contributions to information science theory and practice, focusing on applying sound theory to software engineering practice.

Holzmann is being recognized "for fundamental contributions to improving software quality, in particular through model-checking tools and coding standards, and for successfully transferring these contributions to practitioners developing mission-critical software."

Holzmann designed the coding standard that has become the standard for all flight software development at NASA’s Jet Propulsion Laboratory, and was responsible for the design of a new code review tool that was first used in the flight software team for the Mars Science Laboratory mission. Earlier, he designed and built the Spin model checker. Spin is an efficient tool for the formal verification of distributed software systems. The software has been freely available since 1991, and continues to evolve in line with new developments in the field.

Holzmann received his PhD in Technical Sciences from the Delft University of Technology in The Netherlands in 1979. He worked as a computing science researcher in the Unix group at Bell Laboratories from 1980 to 2003. In 2003, he left Bell Labs to start the new Laboratory for Reliable Software at NASA's Jet Propulsion Laboratory.

Most recently, Holzmann received the NASA Exceptional Engineering Achievement Medal in October 2012, and was part of the team that was awarded the NASA Software of the Year in 2013 for the development of the flight software for the Mars Science Laboratory mission to Mars.

He is a JPL Fellow, an ACM Fellow, and a member of the US National Academy of Engineering. He also serves as senior faculty associate in Computing Science at the California Institute of Technology.

The late Harlan D. Mills was widely recognized for his contributions as a mathematician concerned with bringing more rigor into systems and software development. The award  consists of a $3,000 honorarium, memento, and an invited talk at the 2015 International Conference on Software Engineering (ICSE), which is co-sponsored by the IEEE Computer Society Technical Council on Software Engineering (TCSE). View more information on the Mills Award.

LATEST NEWS
IEEE Uganda Section: Tackling Climate Change and Food Security Through AI and IoT
IEEE Uganda Section: Tackling Climate Change and Food Security Through AI and IoT
Blockchain Service Capability Evaluation (IEEE Std 3230.03-2025)
Blockchain Service Capability Evaluation (IEEE Std 3230.03-2025)
Autonomous Observability: AI Agents That Debug AI
Autonomous Observability: AI Agents That Debug AI
Disaggregating LLM Infrastructure: Solving the Hidden Bottleneck in AI Inference
Disaggregating LLM Infrastructure: Solving the Hidden Bottleneck in AI Inference
Copilot Ergonomics: UI Patterns that Reduce Cognitive Load
Copilot Ergonomics: UI Patterns that Reduce Cognitive Load
Read Next

IEEE Uganda Section: Tackling Climate Change and Food Security Through AI and IoT

Blockchain Service Capability Evaluation (IEEE Std 3230.03-2025)

Autonomous Observability: AI Agents That Debug AI

Disaggregating LLM Infrastructure: Solving the Hidden Bottleneck in AI Inference

Copilot Ergonomics: UI Patterns that Reduce Cognitive Load

The Myth of AI Neutrality in Search Algorithms

Gen AI and LLMs: Rebuilding Trust in a Synthetic Information Age

How AI Is Transforming Fraud Detection in Financial Transactions

FacebookTwitterLinkedInInstagramYoutube
Get the latest news and technology trends for computing professionals with ComputingEdge
Sign up for our newsletter