David F. Martin - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 23 from 23

2003

Secure mechanical verification of mutually recursive proceduresPeter V. Homeier, David F. Martin. iandc, 187(1):1-19, 2003. [doi]

1998

Mechanical Verification of Total Correctness through Diversion Verification ConditionsPeter V. Homeier, David F. Martin. tphol 1998: 189-206

1996

Mechanical Verification of Mutually Recursive ProceduresPeter V. Homeier, David F. Martin. cade 1996: 201-215

1995

A Mechanically Verified Verification Condition GeneratorPeter V. Homeier, David F. Martin. cj, 38(2):131-141, 1995.

1994

Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition GeneratorPeter V. Homeier, David F. Martin. tphol 1994: 269-284

1991

Case Studies in Compiler Correctness Using HOLDavid F. Martin, R. J. Toal. tphol 1992: 242-252

1989

A Debugger for Ada TaskingAnne F. Brindle, Richard N. Taylor, David F. Martin. TSE, 15(3):293-304, 1989. [doi]

1986

Toward Compiler Implementation Correctness ProofsLaurian M. Chirica, David F. Martin. TOPLAS, 8(2):185-214, 1986. [doi]

1982

Testing the INRIA Ada formal definition: the USC-ISI formal semantics projectVittal Kini, David F. Martin, Allen Stoughton. adatec 1982: 120-128 [doi]

1979

An Order-Algebraic Definition of Knuthian SemanticsLaurian M. Chirica, David F. Martin. mst, 13:1-27, 1979.

1978

1976

An Algebraic Formulation of Knuthian SemanticsLaurian M. Chirica, David F. Martin. focs 1976: 127-136

1975

An approach to compiler correctnessLaurian M. Chirica, David F. Martin. relsoft 1975: 96-103 [doi]

1973

On the time required for retentionDaniel M. Berry, Laurian M. Chirica, John B. Johnston, David F. Martin, Arthur Sorkin. hllca 1973: 165-178 [doi]

Two PARALLEL EULER run time models: The dangling reference, impostor environment, and label problemsLaurian M. Chirica, David F. Martin, Timothy A. Dreisbach, J. G. Peetz, Arthur Sorkin. hllca 1973: 141-151 [doi]

1972

A Boolean Matrix Method for the Computation of Linear Precedence FunctionsDavid F. Martin. CACM, 15(6):448-454, 1972.

1970

On Syntax-Directed Transduction and Tree TransducersDavid F. Martin, Steven A. Vere. stoc 1970: 129-135

1969

Path Length Computations on Graph Models of ComputationsDavid F. Martin, Gerald Estrin. TC, 18(6):530-536, 1969. [doi]

1968

Programming Languages: Boolean matrix methods for the detection of simple precedence grammarsDavid F. Martin. CACM, 11(10):685-687, 1968. [doi]

1967

Experiments on Models of Computations and SystemsDavid F. Martin, Gerald Estrin. TC, 16(1):59-69, 1967. [doi]

Models of Computational Systems-Cyclic to Acyclic Graph TransformationsDavid F. Martin, Gerald Estrin. TC, 16(1):70-79, 1967. [doi]

Sign in or sign up to see more results.

runs on WebDSL