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. Fundamental Proof Methods in Computer Science: A Computer-Based Approach,, co-authored with Konstantine Arkoudas, is firmly based on this new approach.