Automatic Verification of Sequential Circuits Using Temporal Logic. - Michael C. Browne; Edmund M. Clarke; David L. Dill; Bud Mishra (IEEE Trans. Computers, 1986)

Trace theory for automatic hierarchical verification of speed-independent circuits. - David L. Dill (MIT Press, 1989)

Timing Assumptions and Verification of Finite-State Concurrent Systems. - David L. Dill (Automatic Verification Methods for Finite State Systems, 1989)

Practicality of state-machine verification of speed-independent circuits. - Steven M. Nowick; David L. Dill (ICCAD, 1989)

Automatic verification of speed-independent circuits with Petri net specifications. - David L. Dill; Steven M. Nowick; Robert F. Sproull (ICCD, 1989)

Complete Trace Structures. - David L. Dill (Hardware Specification, Verification and Synthesis, 1989)

Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. - Paul Loewenstein; David L. Dill (CAV, 1990)

Synthesizing Processes and Schedulers from Temporal Specifications. - Howard Wong-Toi; David L. Dill (CAV, 1990)

Sequential Circuit Verification Using Symbolic Model Checking. - Jerry R. Burch; Edmund M. Clarke; Kenneth L. McMillan; David L. Dill (DAC, 1990)

Automata For Modeling Real-Time Systems. - Rajeev Alur; David L. Dill (ICALP, 1990)

Formal verification of cache systems using refinement relations. - Paul Loewenstein; David L. Dill (ICCD, 1990)

Model-Checking for Real-Time Systems - Rajeev Alur; Costas Courcoubetis; David L. Dill (LICS, 1990)

Checking for Language Inclusion Using Simulation Preorders. - David L. Dill; Alan J. Hu; Howard Wong-Toi (CAV, 1991)

Model-Checking for Probabilistic Real-Time Systems (Extended Abstract). - Rajeev Alur; Costas Courcoubetis; David L. Dill (ICALP, 1991)

Automatic Synthesis of Locally-Clocked Asynchronous State Machines. - Steven M. Nowick; David L. Dill (ICCAD, 1991)

Synthesis of Asynchronous State Machines Using A Local Clock. - Steven M. Nowick; David L. Dill (ICCD, 1991)

Verifying Automata Specifications of Probabilistic Real-time Systems. - Rajeev Alur; Costas Courcoubetis; David L. Dill (REX Workshop, 1991)

Verification with Real-Time COSPAN. - Costas Courcoubetis; David L. Dill; Magda Chatzaki; Panagiotis Tzounakis (CAV, 1992)

Higher-Level Specification and Verification with BDDs. - Alan J. Hu; David L. Dill; Andreas J. Drexler; C. Han Yang (CAV, 1992)

Minimization of Timed Transition Systems. - Rajeev Alur; Costas Courcoubetis; Nicolas Halbwachs; David L. Dill; Howard Wong-Toi (CONCUR, 1992)

Automatic synthesis of 3D asynchronous state machines. - Kenneth Y. Yun; David L. Dill (ICCAD, 1992)

Protocol Verification as a Hardware Design Aid. - David L. Dill; Andreas J. Drexler; Alan J. Hu; C. Han Yang (ICCD, 1992)

Algorithms for Interface Timing Verification. - Kenneth L. McMillan; David L. Dill (ICCD, 1992)

Practical Asynchronous Controller Design. - Steven M. Nowick; Kenneth Y. Yun; David L. Dill (ICCD, 1992)

Synthesis of 3D Asynchronous State Machines. - Kenneth Y. Yun; David L. Dill; Steven M. Nowick (ICCD, 1992)

An implementation of three algorithms for timing verification based on automata emptiness. - Rajeev Alur; Costas Courcoubetis; David L. Dill; Nicolas Halbwachs; Howard Wong-Toi (RTSS, 1992)

Specification and Automatic Verification of Self-Timed Queues. - David L. Dill; Steven M. Nowick; Robert F. Sproull (Formal Methods Syst. Des., 1992)

Symbolic Model Checking: 10^20 States and Beyond - Jerry R. Burch; Edmund M. Clarke; Kenneth L. McMillan; David L. Dill; L. J. Hwang (Inf. Comput., 1992)

Efficient Verification with BDDs using Implicitly Conjoined Invariants. - Alan J. Hu; David L. Dill (CAV, 1993)

Reducing BDD Size by Exploiting Functional Dependencies. - Alan J. Hu; David L. Dill (DAC, 1993)

Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs. - Polly Siegel; Giovanni De Micheli; David L. Dill (DAC, 1993)

Modeling hierarchical combinational circuits. - Jerry R. Burch; David L. Dill; Elizabeth Wolf; Giovanni De Micheli (ICCAD, 1993)

Unifying synchronous/asynchronous state machine synthesis. - Kenneth Y. Yun; David L. Dill (ICCAD, 1993)

Efficient Verification of Symmetric Concurrent Systems. - C. Norris Ip; David L. Dill (ICCD, 1993)

The design of a high-performance cache controller: a case study in asynchronous synthesis. - Steven M. Nowick; Mark E. Dean; David L. Dill; Mark Horowitz (Integr., 1993)

Model-Checking in Dense Real-time - Rajeev Alur; Costas Courcoubetis; David L. Dill (Inf. Comput., 1993)

Automatic verification of Pipelined Microprocessor Control. - Jerry R. Burch; David L. Dill (CAV, 1994)

Hierarchical Models of Synchronous Circuits (Abstract). - David L. Dill (CONCUR, 1994)

New Techniques for Efficient Verification with Implicitly Conjoined BDDs. - Alan J. Hu; Gary York; David L. Dill (DAC, 1994)

Performance-driven synthesis of asynchronous controllers. - Kenneth Y. Yun; Bill Lin 001; David L. Dill; Srinivas Devadas (ICCAD, 1994)

Symbolic model checking for sequential circuit verification. - Jerry R. Burch; Edmund M. Clarke; David E. Long; Kenneth L. McMillan; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

A Theory of Timed Automata. - Rajeev Alur; David L. Dill (Theor. Comput. Sci., 1994)

Self-timed logic using Current-Sensing Completion Detection (CSCD). - Mark E. Dean; David L. Dill; Mark Horowitz (J. VLSI Signal Process., 1994)

Verification of Real-Time Systems by Successive Over and Under Approximation. - David L. Dill; Howard Wong-Toi (CAV, 1995)

Automatic verification of the SCI cache coherence protocol. - Ulrich Stern; David L. Dill (CHARME, 1995)

Improved probabilistic verification by hash compaction. - Ulrich Stern; David L. Dill (CHARME, 1995)

Efficient validity checking for processor verification. - Robert B. Jones; David L. Dill; Jerry R. Burch (ICCAD, 1995)

A high-performance asynchronous SCSI controller. - Kenneth Y. Yun; David L. Dill (ICCD, 1995)

Architecture Validation for Processors. - Richard C. Ho; C. Han Yang; Mark Horowitz; David L. Dill (ISCA, 1995)

An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order). - Seungjoon Park; David L. Dill (SPAA, 1995)

Exact two-level minimization of hazard-free logic with multiple-input changes. - Steven M. Nowick; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995)

The Murphi Verification System. - David L. Dill (CAV, 1996)

Verifying Systems with Replicated Components in Murphi. - C. Norris Ip; David L. Dill (CAV, 1996)

Protocol Verification by Aggregation of Distributed Transactions. - Seungjoon Park; David L. Dill (CAV, 1996)

State Reduction Using Reversible Rules. - C. Norris Ip; David L. Dill (DAC, 1996)

Validity Checking for Combinations of Theories with Equality. - Clark W. Barrett; David L. Dill; Jeremy R. Levitt (FMCAD, 1996)

Self-Consistency Checking. - Robert B. Jones; Carl-Johan H. Seger; David L. Dill (FMCAD, 1996)

Automatic Generation of Invariants in Processor Verification. - Jeffrey X. Su; David L. Dill; Clark W. Barrett (FMCAD, 1996)

A New Scheme for Memory-Efficient Probabilistic Verification. - Ulrich Stern; David L. Dill (FORTE, 1996)

Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. - Seungjoon Park; David L. Dill (SPAA, 1996)

An Invitation to Formal Methods. - Jonathan P. Bowen; Ricky W. Butler; David L. Dill; Robert L. Glass; David Gries; Anthony Hall; Michael G. Hinchey; C. Michael Holloway; Daniel Jackson 001; Cliff B. Jones; Michael J. Lutz; David Lorge Parnas; et al. (Computer, 1996)

Better Verification Through Symmetry. - C. Norris Ip; David L. Dill (Formal Methods Syst. Des., 1996)

More Accurate Polynomial-Time Min-Max Timing Simulation. - Supratik Chakraborty; David L. Dill (ASYNC, 1997)

Timing Analysis of Extended Burst-Mode Circuits. - Supratik Chakraborty; David L. Dill; Kun-Yung Chang; Kenneth Y. Yun (ASYNC, 1997)

Parallelizing the Murphi Verifier. - Ulrich Stern; David L. Dill (CAV, 1997)

Automatic Checking of Aggregation Abstractions Through State Enumeration. - Seungjoon Park; Satyaki Das; David L. Dill (FORTE, 1997)

Approximate algorithms for time separation of events. - Supratik Chakraborty; David L. Dill (ICCAD, 1997)

Formal Verification of Out-of-Order Execution Using Incremental Flushing. - Jens U. Skakkebæk; Robert B. Jones; David L. Dill (CAV, 1998)

Using Magnatic Disk Instead of Main Memory in the Murphi Verifier. - Ulrich Stern; David L. Dill (CAV, 1998)

Practical timing analysis of asynchronous circuits using time separation of events. - Supratik Chakraborty; Kenneth Y. Yun; David L. Dill (CICC, 1998)

A Decision Procedure for Bit-Vector Arithmetic. - Clark W. Barrett; David L. Dill; Jeremy R. Levitt (DAC, 1998)

What's Between Simulation and Formal Verification? (Extended Abstract). - David L. Dill (DAC, 1998)

Approximate Reachability with BDDs Using Overlapping Projections. - Shankar G. Govindaraju; David L. Dill; Alan J. Hu; Mark Horowitz (DAC, 1998)

Validation with Guided Search of the State Space. - C. Han Yang; David L. Dill (DAC, 1998)

Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. - Robert B. Jones; Jens U. Skakkebæk; David L. Dill (FMCAD, 1998)

Formally Verifying Data and Control with Weak Reachability Invariants. - Jeffrey X. Su; David L. Dill; Jens U. Skakkebæk (FMCAD, 1998)

Checking properties of safety critical specifications using efficient decision procedures. - David Y. W. Park; Jens U. Skakkebæk; Mats Per Erik Heimdahl; Barbara J. Czerny; David L. Dill (FMSP, 1998)

Static Analysis to Identify Invariants in RSML Specifications. - David Y. W. Park; Jens U. Skakkebæk; David L. Dill (FTRTFT, 1998)

Verification by approximate forward and backward reachability. - Shankar G. Govindaraju; David L. Dill (ICCAD, 1998)

Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions. - Seungjoon Park; David L. Dill (Theory Comput. Syst., 1998)

BDD-based synthesis of extended burst-mode controllers. - Kenneth Y. Yun; Bill Lin 001; David L. Dill; Srinivas Devadas (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998)

Experience with Predicate Abstraction. - Satyaki Das; David L. Dill; Seungjoon Park (CAV, 1999)

Alternative Approaches to Hardware Verification (abstract). - David L. Dill (CAV, 1999)

Improved Approximate Reachability Using Auxiliary State Variables. - Shankar G. Govindaraju; David L. Dill; Jules P. Bergmann (DAC, 1999)

Formal verification meets simulation (tutorial abstract). - Ellen Sentovich; David L. Dill; Serdar Tasiran (ICCAD, 1999)

Approximate Symbolic Model Checking using Overlapping Projections. - Shankar G. Govindaraju; David L. Dill (SMC@FLoC, 1999)

Verifying Systems with Replicated Components in Mur[b.phiv]. - C. Norris Ip; David L. Dill (Formal Methods Syst. Des., 1999)

An Executable Specification and Verifier for Relaxed Memory Order. - Seungjoon Park; David L. Dill (IEEE Trans. Computers, 1999)

Timing analysis of asynchronous systems using time separation of events. - Supratik Chakraborty; Kenneth Y. Yun; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Automatic synthesis of extended burst-mode circuits. I.(Specification and hazard-free implementations). - Kenneth Y. Yun; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Automatic synthesis of extended burst-mode circuits. II. (Automaticsynthesis). - Kenneth Y. Yun; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

A Framework for Cooperating Decision Procedures. - Clark W. Barrett; David L. Dill; Aaron Stump (CADE, 2000)

Reliable verification using symbolic simulation with scalar values. - Chris Wilson; David L. Dill (DAC, 2000)

Monitor-Based Formal Specification of PCI. - Kanna Shimizu; David L. Dill; Alan J. Hu (FMCAD, 2000)

Symbolic Simulation with Approximate Values. - Chris Wilson; David L. Dill; Randal E. Bryant (FMCAD, 2000)

Model checking Java programs. - David L. Dill (FMSP, 2000)

Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. - Shankar G. Govindaraju; David L. Dill (ICCAD, 2000)

Model checking Java programs (abstract only). - David L. Dill (ISSTA, 2000)

Java Model Checking. - David Y. W. Park; Ulrich Stern; Jens U. Skakkebæk; David L. Dill (ASE, 2000)

Automatic checking of aggregation abstractions through stateenumeration. - Seungjoon Park; Satyaki Das; David L. Dill (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol. - Kanna Shimizu; David L. Dill; Ching-Tsun Chou (CHARME, 2001)

A simple method for extracting models for protocol code. - David Lie; Andy Chou; Dawson R. Engler; David L. Dill (ISCA, 2001)

Successive Approximation of Abstract Transition Relations. - Satyaki Das; David L. Dill (LICS, 2001)

A Decision Procedure for an Extensional Theory of Arrays. - Aaron Stump; Clark W. Barrett; David L. Dill; Jeremy R. Levitt (LICS, 2001)

Parallelizing the Murj Verifier. - Ulrich Stern; David L. Dill (Formal Methods Syst. Des., 2001)

Faster Proof Checking in the Edinburgh Logical Framework. - Aaron Stump; David L. Dill (CADE, 2002)

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. - Clark W. Barrett; David L. Dill; Aaron Stump (CAV, 2002)

CVC: A Cooperating Validity Checker. - Aaron Stump; Clark W. Barrett; David L. Dill (CAV, 2002)

Formal verification methods: getting around the brick wall. - David L. Dill; Nate James; Shishpal Rawat; Gérard Berry; Limor Fix; Harry Foster; Rajeev K. Ranjan 001; Gunnar Stålmarck; Curt Widdoes (DAC, 2002)

Deriving a simulation input generator and a coverage metric from a formal specification. - Kanna Shimizu; David L. Dill (DAC, 2002)

Counter-Example Based Predicate Discovery in Predicate Abstraction. - Satyaki Das; David L. Dill (FMCAD, 2002)

Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. - Vijay Ganesh 001; Sergey Berezin; David L. Dill (FMCAD, 2002)

A Generalization of Shostak's Method for Combining Decision Procedures. - Clark W. Barrett; David L. Dill; Aaron Stump (FroCoS, 2002)

CMC: A Pragmatic Approach to Model Checking Real Code. - Madanlal Musuvathi; David Y. W. Park; Andy Chou; Dawson R. Engler; David L. Dill (OSDI, 2002)

Model checking system software with CMC. - Madanlal Musuvathi; Andy Chou; David L. Dill; Dawson R. Engler (ACM SIGOPS European Workshop, 2002)

Using Formal Specifications for Functional Validation of Hardware Designs. - Kanna Shimizu; David L. Dill (IEEE Des. Test Comput., 2002)

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. - Aaron Stump; Clark W. Barrett; David L. Dill (LFM, 2002)

Formal Verification of Out-of-Order Execution with Incremental Flushing. - Robert B. Jones; Jens U. Skakkebæk; David L. Dill (Formal Methods Syst. Des., 2002)

Strengthening Invariants by Symbolic Consistency Testing. - Husam Abu-Haimed; Sergey Berezin; David L. Dill (CAV, 2003)

Semi-formal Verification of Memory Systems by Symbolic Simulation. - Husam Abu-Haimed; Sergey Berezin; David L. Dill (CHARME, 2003)

Evolution as Design Engineer. - David L. Dill; Patrick Lincoln (CMSB, 2003)

Event Correlation: Language and Semantics. - César Sánchez 001; Sriram Sankaranarayanan 001; Henny Sipma; Ting Zhang 001; David L. Dill; Zohar Manna (EMSOFT, 2003)

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. - Sergey Berezin; Vijay Ganesh 001; David L. Dill (TACAS, 2003)

Voting and technology: who gets to count your vote? - David L. Dill; Bruce Schneier; Barbara Simons (Commun. ACM, 2003)

Using Interface Refinement to Integrate Formal Verification into the Design Cycle. - Jacob Chang; Sergey Berezin; David L. Dill (CAV, 2004)

A Partitioning Methodology for BDD-Based Verification. - Debashis Sahoo; Subramanian K. Iyer; Jawahar Jain; Christian Stangier; Amit Narayan; David L. Dill; E. Allen Emerson (FMCAD, 2004)

The battle of accountable voting systems. - David L. Dill (MEMOCODE, 2004)

Evaluation of voting systems. - Poorvi L. Vora; Ben Adida; Ren Bucholz; David Chaum; David L. Dill; David R. Jefferson; Douglas W. Jones; William Lattin; Aviel D. Rubin; Michael Ian Shamos; Moti Yung (Commun. ACM, 2004)

A Practical Approach to Partial Functions in CVC Lite. - Sergey Berezin; Clark W. Barrett; Igor Shikanian; Marsha Chechik; Arie Gurfinkel; David L. Dill (D/PDPAR@IJCAR, 2004)

Guest Editors' Introduction: E-Voting Security. - David L. Dill; Aviel D. Rubin (IEEE Secur. Priv., 2004)

A New Reachability Algorithm for Symmetric Multi-processor Architecture. - Debashis Sahoo; Jawahar Jain; Subramanian K. Iyer; David L. Dill (ATVA, 2005)

Predictive Reachability Using a Sample-Based Approach. - Debashis Sahoo; Jawahar Jain; Subramanian K. Iyer; David L. Dill; E. Allen Emerson (CHARME, 2005)

Multi-threaded reachability. - Debashis Sahoo; Jawahar Jain; Subramanian K. Iyer; David L. Dill; E. Allen Emerson (DAC, 2005)

The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways. - David L. Dill; Merrill Knapp; Pamela Gage; Carolyn L. Talcott; Keith Laderoute; Patrick Lincoln (Systems Biology and Regulatory Genomics, 2005)

An Incremental Heap Canonicalization Algorithm. - Madanlal Musuvathi; David L. Dill (SPIN, 2005)

I Think I Voted: E-Voting vs. Democracy. - David L. Dill (CAV, 2006)

A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. - Husam Abu-Haimed; David L. Dill; Sergey Berezin (FMCAD, 2006)

Multiple Representations of Biological Processes. - Carolyn L. Talcott; David L. Dill (Trans. Comp. Sys. Biology, 2006)

A Decision Procedure for Bit-Vectors and Arrays. - Vijay Ganesh 001; David L. Dill (CAV, 2007)

Formal Verification and Biology. - David L. Dill (ATVA, 2008)

Automatic Formal Verification of Block Cipher Implementations. - Eric Whitman Smith; David L. Dill (FMCAD, 2008)

A Retrospective on Murphi. - David L. Dill (25 Years of Model Checking, 2008)

Point/counterpoint: The U.S. should ban paperless electronic voting machines. - David L. Dill; Daniel Castro (Commun. ACM, 2008)

EXE: Automatically Generating Inputs of Death. - Cristian Cadar; Vijay Ganesh 001; Peter M. Pawlowski; David L. Dill; Dawson R. Engler (ACM Trans. Inf. Syst. Secur., 2008)

Towards program optimization through automated analysis of numerical precision. - Michael D. Linderman; Matthew Ho; David L. Dill; Teresa H. Meng; Garry P. Nolan (CGO, 2010)

MiDReG: A method of mining developmentally regulated genes using Boolean implications. - Debashis Sahoo; Jun Seita; Deepta Bhattacharya; Matthew A. Inlay; Irving L. Weissman; Sylvia K. Plevritis; David L. Dill (Proc. Natl. Acad. Sci. USA, 2010)

Applying a Reusable Election Threat Model at the County Level. - Eric Lazarus; David L. Dill; Jeremy Epstein (EVT/WOTE, 2011)

Are Cells Asynchronous Circuits? - (Invited Talk). - David L. Dill (VMCAI, 2011)

Model Checking Cell Biology. - David L. Dill (CAV, 2012)

Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach. - Weiruo Zhang; Ritesh Kolte; David L. Dill (BMC Syst. Biol., 2015)

Deciphering cancer biology using boolean methods. - Subarna Sinha; David L. Dill (HLDVT, 2016)

CauloBrowser: A systems biology resource for Caulobacter crescentus. - Keren Lasker; Jared M. Schrader; Yifei Men; Tyler Marshik; David L. Dill; Harley H. McAdams; Lucy Shapiro (Nucleic Acids Res., 2016)

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (CAV (1), 2017)

Developing Bug-Free Machine Learning Systems With Formal Mathematics. - Daniel Selsam; Percy Liang; David L. Dill (ICML, 2017)

Towards Proving the Adversarial Robustness of Deep Neural Networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (FVAV@iFM, 2017)

Ground-Truth Adversarial Examples. - Nicholas Carlini; Guy Katz; Clark W. Barrett; David L. Dill (CoRR, 2017)

The Marabou Framework for Verification and Analysis of Deep Neural Networks. - Guy Katz; Derek A. Huang; Duligur Ibeling; Kyle Julian; Christopher Lazarus; Rachel Lim; Parth Shah 003; Shantanu Thakoor; Haoze Wu 001; Aleksandar Zeljic; David L. Dill; Mykel J. Kochenderfer; et al. (CAV (1), 2019)

Learning a SAT Solver from Single-Bit Supervision. - Daniel Selsam; Matthew Lamm; Benedikt Bünz; Percy Liang; Leonardo de Moura 001; David L. Dill (ICLR (Poster), 2019)

The Move Prover. - Jingyi Emma Zhong; Kevin Cheang; Shaz Qadeer; Wolfgang Grieskamp; Sam Blackshear; Junkil Park; Yoni Zohar; Clark W. Barrett; David L. Dill (CAV (1), 2020)

Resources: A Safe Language Abstraction for Money. - Sam Blackshear; David L. Dill; Shaz Qadeer; Clark W. Barrett; John C. Mitchell; Oded Padon; Yoni Zohar (CoRR, 2020)

Example dataset of stLFR linked reads to run Aquila_stLFR. - Yichen Henry Liu; Griffin L. Grubbs; Lu Zhang; Xiaodong Fang; David L. Dill; Arend Sidow; Xin Zhou (Zenodo, 2021)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. - David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Meng Xu; Jingyi Emma Zhong (TACAS (1), 2022)

Reluplex: a calculus for reasoning about deep neural networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (Formal Methods Syst. Des., 2022)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

ClassInvGen: Class Invariant Synthesis using Large Language Models. - Chuyue Sun; Viraj Agashe; Saikat Chakraborty; Jubi Taneja; Clark W. Barrett; David L. Dill; Xiaokang Qiu; Shuvendu K. Lahiri (CoRR, 2025)