Models of Computations and Systems - Evaluation of Vertex Probabilities in Graph Models of Computations. - David F. Martin; Gerald Estrin (J. ACM, 1967)

Experiments on Models of Computations and Systems. - David F. Martin; Gerald Estrin (IEEE Trans. Electron. Comput., 1967)

Models of Computational Systems-Cyclic to Acyclic Graph Transformations. - David F. Martin; Gerald Estrin (IEEE Trans. Electron. Comput., 1967)

Programming Languages: Boolean matrix methods for the detection of simple precedence grammars. - David F. Martin (Commun. ACM, 1968)

Path Length Computations on Graph Models of Computations. - David F. Martin; Gerald Estrin (IEEE Trans. Computers, 1969)

On Syntax-Directed Transduction and Tree Transducers - David F. Martin; Steven A. Vere (STOC, 1970)

A Boolean Matrix Method for the Computation of Linear Precedence Functions. - David F. Martin (Commun. ACM, 1972)

On the time required for retention. - Daniel M. Berry; Laurian M. Chirica; John B. Johnston; David F. Martin; Arthur Sorkin (HLLCA, 1973)

Two PARALLEL EULER run time models: The dangling reference, impostor environment, and label problems. - Laurian M. Chirica; David F. Martin; Timothy A. Dreisbach; J. G. Peetz; Arthur Sorkin (HLLCA, 1973)

An approach to compiler correctness. - Laurian M. Chirica; David F. Martin (Reliable Software, 1975)

An Algebraic Formulation of Knuthian Semantics - Laurian M. Chirica; David F. Martin (FOCS, 1976)

Time required for reference count management in retention block-structured languages. Part 1. - Daniel M. Berry; Laurian M. Chirica; John B. Johnston; David F. Martin; Arthur Sorkin (Int. J. Parallel Program., 1978)

On the time required for reference count management in retention block-structured languages. Part 2. - Daniel M. Berry; Laurian M. Chirica; John B. Johnston; David F. Martin; Arthur Sorkin (Int. J. Parallel Program., 1978)

Algebraic Properties of Operator Precedence Languages - Stefano Crespi-Reghizzi; Dino Mandrioli; David F. Martin (Inf. Control., 1978)

An Order-Algebraic Definition of Knuthian Semantics. - Laurian M. Chirica; David F. Martin (Math. Syst. Theory, 1979)

Testing the INRIA Ada formal definition: the USC-ISI formal semantics project. - Vittal Kini; David F. Martin; Allen Stoughton (AdaTEC Conference on Ada, 1982)

Toward Compiler Implementation Correctness Proofs. - Laurian M. Chirica; David F. Martin (ACM Trans. Program. Lang. Syst., 1986)

A Debugger for Ada Tasking. - Anne F. Brindle; Richard N. Taylor; David F. Martin (IEEE Trans. Software Eng., 1989)

Case Studies in Compiler Correctness Using HOL. - David F. Martin; R. J. Toal (TPHOLs, 1991)

Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator. - Peter V. Homeier; David F. Martin (TPHOLs, 1994)

A Mechanically Verified Verification Condition Generator. - Peter V. Homeier; David F. Martin (Comput. J., 1995)

Mechanical Verification of Mutually Recursive Procedures. - Peter V. Homeier; David F. Martin (CADE, 1996)

Mechanical Verification of Total Correctness through Diversion Verification Conditions. - Peter V. Homeier; David F. Martin (TPHOLs, 1998)

Secure mechanical verification of mutually recursive procedures. - Peter V. Homeier; David F. Martin (Inf. Comput., 2003)