David R. Musser
Computer Science Department
Rensselaer Polytechnic Institute
||The generic programming approach to design and systematic classification of software components, with the goals of correctness, efficiency, and generality of algorithms and data structures. Application of formal logic and proof-checking programs to understanding and verifying correctness, safety, and security properties of generic software components. For recent work, including joint work with Konstantine Arkoudas on development and application of the Athena interactive proof system, and with Carlos Varela on the actor model of distributed computation, see the Proof Central web site.|
David R. Musser and Carlos A. Varela. Structured reasoning about actor systems. This is a minor revision of a paper presented at AGERE! 13, SPLASH Conference, Indianapolis, Indiana, USA, October 2013.
Books on the Standard Template Library:
David R. Musser, Gilmer J. Derge, and Atul Saini, STL Tutorial and Reference Guide, Second Edition: C++ Programming with the Standard Template Library, Addison-Wesley, Reading, MA, 2001 (First Edition: 1996).
P.J. Plauger, Alexander A. Stepanov, Meng Lee, and David R. Musser, The C++ Standard Template Library, Prentice Hall, Upper Saddle River, NJ, 2000.
For other publications, see Curriculum Vita (2006).
Email: musser at cs dot rpi dot edu
Home Page: http://www.cs.rpi.edu/~musser (this page)
Phone: [Please use email]
Postal Address: Computer Science Department, Rensselaer Polytechnic Institute, Troy, NY 12180-3590
Dave Musser, Professor of Computer Science, retired in 2007 after a
37-year career combining academic, industry, and research-institute
positions, including almost 20 years at Rensselaer. Upon receiving
his doctorate from the University of Wisconsin at Madison, he
spent the early part of his career on the computer science faculty at
the University of Texas at Austin and in DARPA-sponsored research at
Information Sciences Institute (ISI) in Marina del Rey, California. In
1979 he joined the research staff at GE's Labs in Niskayuna, New York,
where he spent the next eight years and briefly served also as an
adjunct faculty member at Rensselaer. He joined Rensselaer's Computer
Science Department full-time in 1988, first as a research professor;
he was named a tenured full professor in 1995. During sabbaticals he
conducted research at the Technical University of Vienna in Austria
and Tübingen University in Germany (in 1998) and at Google, Inc.,
in New York (in 2006). Through contracts and as a consultant, he also
took part in numerous industry-based research and development projects
at Hewlett Packard, IBM, Silicon Graphics, and SRI International.
His early research focused on applications of formal logic and proof-checking programs to understanding and verifying correctness, safety, and security properties of computer software and hardware. He discovered the fundamental proof method now known as ``inductionless induction'' or ``proof by consistency.'' This work was part of the basis of program verification systems called Affirm (which he co-developed at ISI), Affirm-85 (at GE), and Tecton (at Rensselaer). In research begun at GE and continued at Rensselaer, he collaborated in developing the generic programming approach to design and systematic classification of software components. Some of the results of this work are familiar to many software developers in the form of the Standard Template Library (STL), now a core part the C++ programming language's Standard Library. His most recent work combines some of these themes, towards methods of proof-checking applicable to properties of generic software components like those in the STL.
In continuing his relationship with Rensselaer as a professor emeritus, he is engaged in further research on proof-based software development, including its potential as a new approach to teaching logic and proof methods to computer science students.
This page was last updated on January 7, 2014.