Elementary Bounds for Presburger Arithmetic - Derek C. Oppen (STOC, 1973)

An Assertion Language for Data Structures. - Stephen A. Cook; Derek C. Oppen (POPL, 1975)

Proving Assertions about Programs that Manipulate Data Structures - Derek C. Oppen; Stephen A. Cook (STOC, 1975)

Fast Decision Algorithms Based on Union and Find - Greg Nelson; Derek C. Oppen (FOCS, 1977)

Unrestricted Procedure Calls in Hoare's Logic. - Robert Cartwright; Derek C. Oppen (POPL, 1978)

A Simplifier Based on Efficient Decision Algorithms. - Charles G. Nelson; Derek C. Oppen (POPL, 1978)

A 2^2^2^pn Upper Bound on the Complexity of Presburger Arithmetic. - Derek C. Oppen (J. Comput. Syst. Sci., 1978)

Simplification by Cooperating Decision Procedures. - Greg Nelson; Derek C. Oppen (ACM Trans. Program. Lang. Syst., 1979)

Fast Decision Procedures Based on Congruence Closure. - Greg Nelson; Derek C. Oppen (J. ACM, 1980)

Reasoning About Recursively Defined Data Structures. - Derek C. Oppen (J. ACM, 1980)

Complexity, Convexity and Combinations of Theories. - Derek C. Oppen (Theor. Comput. Sci., 1980)

Prettyprinting. - Derek C. Oppen (ACM Trans. Program. Lang. Syst., 1980)

The Logic of Aliasing. - Robert Cartwright; Derek C. Oppen (Acta Informatica, 1981)

The Clearinghouse: A Decentralized Agent for Locating Named Objects in a Distributed Environment. - Derek C. Oppen; Yogen K. Dalal (ACM Trans. Inf. Syst., 1983)