Static program analysis at NASA

Software is an increasingly critical component in aerospace systems. Since the Shuttle started operation in 1980, sixteen highly-critical software errors have been discovered in the released software. These problems occurred despite NASA having one of the most thorough and sophisticated software development and verification processes in existence. The risk of software errors can be reduced through automated software verification and validation using formal methods, and in particular, static program analysis.

In this talk, I will describe our attempts at infusing static program analysis at NASA, which led us to design our own static analyzers. I will introduce what static program analysis is and what it can do for software developers. Using real examples, I will show how useful it can be and what you might expect from using such tools. I will finish the talk by taking a look at where the research in the field might lead in a few more years.

Dr. Brat is Deputy Director at the Research Institute for Advanced Computer Science. He is also a member of the Robust Software Engineering group at NASA Ames Research Center. He received his Ph.D. in Electrical & Computer Engineering from The University of Texas at Austin. His work at NASA focuses on software verification and validation, in particular, the application of static program analysis to large software systems. He co-developed C Global Surveyor (a static analyzer for C) and applied static analysis tools based on abstract interpretation to the verification of software for Mars missions and the International Space Station.

Further Reading:

• Guillaume Brat, Arnaud Venet, "Precise and Scalable Static Program Analysis of NASA Flight Software," IEEE Aerospace Conference, Big Sky, MT, March, 2005.
• Arnaud Venet, Guillaume Brat, "Precise and Efficient Static Array Bound Checking for Large Embedded C Programs," Proc. PLDI'04: ACM SIGPLAN Conf. on Programming Language Design and Implementation, Washington DC, USA, pp. 231-242, June 9-11, 2004.
• Guillaume Brat, Roger Klemm, "Static Analysis of the Mars Exploration Rover flight software," Proc. 1st Int'l Space Mission Challenge for Information Technology, Pasadena, CA., pp. 321-326, Oct. 15-18, 2003.

Dr. Brat's presentation materials

Intellectual Property and Public Policy

The term "intellectual property" or "I.P." embraces several distinct but related bodies of law, including patents (utility patents, plant patents, and design patents), copyrights, trademarks, and unfair competition law. Utility patent law deals with exclusive rights in inventions; copyright in works of authorship such as literature, music, and software; and trademarks in source identifiers such as brand names.

In this talk, I will present an overview of three of these bodies of IP law (trade secrets, copyright, and patents), with a special emphasis on their relation to software. I will discuss, among other things, the protectability of software under these three bodies of law; how courts determine whether a competing software program infringes the copyright in another program; reverse engineering as a fair use of software; software-related issues under the Digital Millennium Copyright Act; and the current controversy over the patentability of software-related innovations, including business methods that involve the use of computers. We will also discuss how courts determine who owns an invention or work of authorship.

Prof. Thomas F. Cotter is the Briggs and Morgan Professor of Law and a Solly Robins Distinguished Research Fellow at the University of Minnesota Law School. Professor Cotter’s principal research and teaching interests are in the fields of domestic and international intellectual property law, antitrust, and law and economics. He is the coauthor, with Roger D. Blair, of Intellectual Property: Economic and Legal Dimensions of Rights and Remedies, published by Cambridge University Press in 2005. He has authored or coauthored other 30 other scholarly works, including articles in the California Law Review, the Georgetown Law Journal, the Iowa Law Review (forthcoming), the Minnesota Law Review, the University of Illinois Law Review, the William & Mary Law Review, the North Carolina Law Review, the Notre Dame Law Review, and the Tulane Law Review. Prior to joining the faculty at the University of Minnesota, Professor Cotter clerked for a federal judge; practiced law in New York and Chicago; and taught at the University of Florida and at Washington and Lee University.

Further Reading:

• Computer Associates, Inc. v. Altai, Inc. 982 F.2d 693 (2d Cir. 1992).
• Diamond v. Diehr, 450 U.S. 175 (1982).
• In re Comiskey, 499 F.2d 1365 (Fed. Cir. 2007), with corrections.

Writing Workshop

Agile Workshop