Detecting boundaries in a vector field. - Hsien-Che Lee; David R. Cok (IEEE Trans. Signal Process., 1991)

How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification. - Gary T. Leavens; Yoonsik Cheon; Curtis Clifton; Clyde Ruby; David R. Cok (FMCO, 2002)

ESC/Java2: Uniting ESC/Java and JML. - David R. Cok; Joseph Kiniry (CASSIS, 2004)

Reasoning with specifications containing method calls and model fields. - David R. Cok (J. Object Technol., 2005)

How the design of JML accommodates both runtime assertion checking and formal verification. - Gary T. Leavens; Yoonsik Cheon; Curtis Clifton; Clyde Ruby; David R. Cok (Sci. Comput. Program., 2005)

An overview of JML tools and applications. - Lilian Burdy; Yoonsik Cheon; David R. Cok; Michael D. Ernst; Joseph R. Kiniry; Gary T. Leavens; K. Rustan M. Leino; Erik Poll (Int. J. Softw. Tools Technol. Transf., 2005)

Specifying java iterators with JML and Esc/Java2. - David R. Cok (SAVCBS@FSE, 2006)

Improved usability and performance of SMT solvers for debugging specifications. - David R. Cok (Int. J. Softw. Tools Technol. Transf., 2010)

PEASOUP: preventing exploits against software of uncertain provenance (position paper). - Michele Co; Jack W. Davidson; Jason D. Hiser; John C. Knight; Anh Nguyen-Tuong; David R. Cok; Denis Gopan; David Melski; Wenke Lee; Chengyu Song; Thomas Bracewell; David Hyde 002; et al. (SESS@ICSE, 2011)

Local vs. global models for effort estimation and defect prediction. - Tim Menzies; Andrew Butcher; Andrian Marcus; Thomas Zimmermann 001; David R. Cok (ASE, 2011)

OpenJML: JML for Java 7 by Extending OpenJDK. - David R. Cok (NASA Formal Methods, 2011)

jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2. - David R. Cok (NASA Formal Methods, 2011)

The 2012 SMT Competition. - David R. Cok; Alberto Griggio; Roberto Bruttomesso; Morgan Deters (SMT@IJCAR, 2012)

Active Learning and Effort Estimation: Finding the Essential Content of Software Effort Estimation Data. - Ekrem Kocaguneli; Tim Menzies; Jacky Keung; David R. Cok; Raymond J. Madachy (IEEE Trans. Software Eng., 2013)

Local versus Global Lessons for Defect Prediction and Effort Estimation. - Tim Menzies; Andrew Butcher; David R. Cok; Andrian Marcus; Lucas Layman; Forrest Shull; Burak Turhan; Thomas Zimmermann 001 (IEEE Trans. Software Eng., 2013)

OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. - David R. Cok (F-IDE, 2014)

SPEEDY: An Eclipse-based IDE for invariant inference. - David R. Cok; Scott C. Johnson (F-IDE, 2014)

The 2014 SMT Competition. - David R. Cok; David Déharbe; Tjark Weber (J. Satisf. Boolean Model. Comput., 2014)

Report on SL-COMP 2014. - Mihaela Sighireanu; David R. Cok (J. Satisf. Boolean Model. Comput., 2014)

The 2013 Evaluation of SMT-COMP and SMT-LIB. - David R. Cok; Aaron Stump; Tjark Weber (J. Autom. Reason., 2015)

Polymorphic type inference for machine code. - Matthew Noonan; Alexey Loginov; David R. Cok (PLDI, 2016)

An algorithm and tool to infer practical postconditions. - John L. Singleton; Gary T. Leavens; Hridesh Rajan; David R. Cok (ICSE (Companion Volume), 2018)

Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects. - David R. Cok (ISoLA (4), 2018)

Runtime Assertion Checking and Static Verification: Collaborative Partners. - Fonenantsoa Maurica; David R. Cok; Julien Signoles (ISoLA (2), 2018)

Reasoning about functional programming in Java and C++. - David R. Cok (ISSTA/ECOOP Workshops, 2018)

Practical Methods for Reasoning About Java 8's Functional Programming Features. - David R. Cok; Serdar Tasiran (VSTTE, 2018)

Inferring Concise Specifications of APIs. - John L. Singleton; Gary T. Leavens; Hridesh Rajan; David R. Cok (CoRR, 2019)

JML and OpenJML for Java 16. - David R. Cok (FTfJP@ECOOP, 2021)

Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods. - Amirfarhad Nilizadeh; Gary T. Leavens; Xuan-Bach Dinh Le 001; Corina S. Pasareanu; David R. Cok (ICST, 2021)

Specifying the Boundary Between Unverified and Verified Code. - David R. Cok; K. Rustan M. Leino (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Further Lessons from the JML Project. - Gary T. Leavens; David R. Cok; Amirfarhad Nilizadeh (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Documentation and Educational Materials for a 2nd Edition of the Java Modeling Language. - David R. Cok (FTfJP@ECOOP, 2022)

Automated Reasoning Repair. - Amirfarhad Nilizadeh; Gary T. Leavens; David R. Cok (FTfJP@ECOOP, 2022)

Generating Counterexamples in the form of Unit Tests from Hoare-style Verification Attempts. - Amirfarhad Nilizadeh; Marlon Calvo; Gary T. Leavens; David R. Cok (FormaliSE@ICSE, 2022)

Abstraction in Deductive Verification: Model Fields and Model Methods. - David R. Cok; Gary T. Leavens (ISoLA (1), 2022)

Does Going Beyond Branch Coverage Make Program Repair Tools More Reliable? - Amirfarhad Nilizadeh; Gary T. Leavens; Corina S. Pasareanu; Xuan-Bach Dinh Le 001; David R. Cok (ICST, 2024)

Toward Using Fuzzers and Lightweight Specifications to Reveal Semantic Bugs. - Amirfarhad Nilizadeh; Gary T. Leavens; David R. Cok (J. Object Technol., 2024)