| 2026 | TACAS | VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. | Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | 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 |
| 2020 | CAV | The Move Prover. | Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill |
| 2019 | CAV | 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, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, Clark W. Barrett |
| 2019 | ICLR | Learning a SAT Solver from Single-Bit Supervision. | Daniel Selsam, Matthew Lamm, Benedikt Bnz, Percy Liang, Leonardo de Moura, David L. Dill |
| 2017 | CAV | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. | Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer |
| 2017 | ICML | Developing Bug-Free Machine Learning Systems With Formal Mathematics. | Daniel Selsam, Percy Liang, David L. Dill |
| 2012 | CAV | Model Checking Cell Biology. | David L. Dill |
| 2011 | VMCAI | Are Cells Asynchronous Circuits? - (Invited Talk). | David L. Dill |
| 2010 | CGO | Towards program optimization through automated analysis of numerical precision. | Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Meng, Garry P. Nolan |
| 2008 | ATVA | Formal Verification and Biology. | David L. Dill |
| 2008 | FMCAD | Automatic Formal Verification of Block Cipher Implementations. | Eric Whitman Smith, David L. Dill |
| 2007 | CAV | A Decision Procedure for Bit-Vectors and Arrays. | Vijay Ganesh, David L. Dill |
| 2006 | CAV | I Think I Voted: E-Voting vs. Democracy. | David L. Dill |
| 2006 | CCS | EXE: automatically generating inputs of death. | Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler |
| 2006 | FMCAD | A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. | Husam Abu-Haimed, David L. Dill, Sergey Berezin |
| 2005 | ATVA | A New Reachability Algorithm for Symmetric Multi-processor Architecture. | Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill |
| 2005 | DAC | Multi-threaded reachability. | Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson |
| 2005 | RECOMB | The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways. | David L. Dill, Merrill Knapp, Pamela Gage, Carolyn L. Talcott, Keith Laderoute, Patrick Lincoln |
| 2004 | CAV | Using Interface Refinement to Integrate Formal Verification into the Design Cycle. | Jacob Chang, Sergey Berezin, David L. Dill |
| 2004 | FMCAD | A Partitioning Methodology for BDD-Based Verification. | Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson |
| 2004 | MEMOCODE | The battle of accountable voting systems. | David L. Dill |
| 2003 | CAV | Strengthening Invariants by Symbolic Consistency Testing. | Husam Abu-Haimed, Sergey Berezin, David L. Dill |
| 2003 | EMSOFT | Event Correlation: Language and Semantics. | Csar Snchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, Zohar Manna |
| 2003 | TACAS | An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. | Sergey Berezin, Vijay Ganesh, David L. Dill |
| 2002 | CADE | Faster Proof Checking in the Edinburgh Logical Framework. | Aaron Stump, David L. Dill |
| 2002 | CAV | Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 2002 | CAV | CVC: A Cooperating Validity Checker. | Aaron Stump, Clark W. Barrett, David L. Dill |
| 2002 | DAC | Formal verification methods: getting around the brick wall. | David L. Dill, Nate James, Shishpal Rawat, Grard Berry, Limor Fix, Harry Foster, Rajeev K. Ranjan, Gunnar Stlmarck, Curt Widdoes |
| 2002 | DAC | Deriving a simulation input generator and a coverage metric from a formal specification. | Kanna Shimizu, David L. Dill |
| 2002 | FMCAD | Counter-Example Based Predicate Discovery in Predicate Abstraction. | Satyaki Das, David L. Dill |
| 2002 | FMCAD | Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. | Vijay Ganesh, Sergey Berezin, David L. Dill |
| 2002 | OSDI | CMC: A Pragmatic Approach to Model Checking Real Code. | Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, David L. Dill |
| 2001 | ISCA | A simple method for extracting models for protocol code. | David Lie, Andy Chou, Dawson R. Engler, David L. Dill |
| 2001 | LICS | Successive Approximation of Abstract Transition Relations. | Satyaki Das, David L. Dill |
| 2001 | LICS | A Decision Procedure for an Extensional Theory of Arrays. | Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 2000 | CADE | A Framework for Cooperating Decision Procedures. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 2000 | DAC | Reliable verification using symbolic simulation with scalar values. | Chris Wilson, David L. Dill |
| 2000 | FMCAD | Monitor-Based Formal Specification of PCI. | Kanna Shimizu, David L. Dill, Alan J. Hu |
| 2000 | FMCAD | Symbolic Simulation with Approximate Values. | Chris Wilson, David L. Dill, Randal E. Bryant |
| 2000 | ICCAD | Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. | Shankar G. Govindaraju, David L. Dill |
| 2000 | ISSTA | Model checking Java programs (abstract only). | David L. Dill |
| 1999 | CAV | Experience with Predicate Abstraction. | Satyaki Das, David L. Dill, Seungjoon Park |
| 1999 | CAV | Alternative Approaches to Hardware Verification (abstract). | David L. Dill |
| 1999 | DAC | Improved Approximate Reachability Using Auxiliary State Variables. | Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann |
| 1999 | ICCAD | Formal verification meets simulation (tutorial abstract). | Ellen Sentovich, David L. Dill, Serdar Tasiran |
| 1998 | CAV | Formal Verification of Out-of-Order Execution Using Incremental Flushing. | Jens U. Skakkebk, Robert B. Jones, David L. Dill |
| 1998 | CAV | Using Magnatic Disk Instead of Main Memory in the Mur | Ulrich Stern, David L. Dill |
| 1998 | DAC | A Decision Procedure for Bit-Vector Arithmetic. | Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 1998 | DAC | What's Between Simulation and Formal Verification? (Extended Abstract). | David L. Dill |
| 1998 | DAC | Approximate Reachability with BDDs Using Overlapping Projections. | Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz |
| 1998 | DAC | Validation with Guided Search of the State Space. | C. Han Yang, David L. Dill |
| 1998 | FMCAD | Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. | Robert B. Jones, Jens U. Skakkebk, David L. Dill |
| 1998 | FMCAD | Formally Verifying Data and Control with Weak Reachability Invariants. | Jeffrey X. Su, David L. Dill, Jens U. Skakkebk |
| 1998 | ICCAD | Verification by approximate forward and backward reachability. | Shankar G. Govindaraju, David L. Dill |
| 1997 | CAV | Parallelizing the Mur | Ulrich Stern, David L. Dill |
| 1997 | FORTE | Automatic Checking of Aggregation Abstractions Through State Enumeration. | Seungjoon Park, Satyaki Das, David L. Dill |
| 1997 | ICCAD | Approximate algorithms for time separation of events. | Supratik Chakraborty, David L. Dill |
| 1996 | CAV | The Mur | David L. Dill |
| 1996 | CAV | Verifying Systems with Replicated Components in Mur | C. Norris Ip, David L. Dill |
| 1996 | CAV | Protocol Verification by Aggregation of Distributed Transactions. | Seungjoon Park, David L. Dill |
| 1996 | DAC | State Reduction Using Reversible Rules. | C. Norris Ip, David L. Dill |
| 1996 | FMCAD | Validity Checking for Combinations of Theories with Equality. | Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 1996 | FMCAD | Self-Consistency Checking. | Robert B. Jones, Carl-Johan H. Seger, David L. Dill |
| 1996 | FMCAD | Automatic Generation of Invariants in Processor Verification. | Jeffrey X. Su, David L. Dill, Clark W. Barrett |
| 1996 | FORTE | A New Scheme for Memory-Efficient Probabilistic Verification. | Ulrich Stern, David L. Dill |
| 1996 | SPAA | Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. | Seungjoon Park, David L. Dill |
| 1995 | CAV | Verification of Real-Time Systems by Successive Over and Under Approximation. | David L. Dill, Howard Wong-Toi |
| 1995 | ICCAD | Efficient validity checking for processor verification. | Robert B. Jones, David L. Dill, Jerry R. Burch |
| 1995 | ICCD | A high-performance asynchronous SCSI controller. | Kenneth Y. Yun, David L. Dill |
| 1995 | ISCA | Architecture Validation for Processors. | Richard C. Ho, C. Han Yang, Mark Horowitz, David L. Dill |
| 1995 | SPAA | An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order). | Seungjoon Park, David L. Dill |
| 1994 | CAV | Automatic verification of Pipelined Microprocessor Control. | Jerry R. Burch, David L. Dill |
| 1994 | CONCUR | Hierarchical Models of Synchronous Circuits (Abstract). | David L. Dill |
| 1994 | DAC | New Techniques for Efficient Verification with Implicitly Conjoined BDDs. | Alan J. Hu, Gary York, David L. Dill |
| 1994 | ICCAD | Performance-driven synthesis of asynchronous controllers. | Kenneth Y. Yun, Bill Lin, David L. Dill, Srinivas Devadas |
| 1993 | CAV | Efficient Verification with BDDs using Implicitly Conjoined Invariants. | Alan J. Hu, David L. Dill |
| 1993 | DAC | Reducing BDD Size by Exploiting Functional Dependencies. | Alan J. Hu, David L. Dill |
| 1993 | DAC | Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs. | Polly Siegel, Giovanni De Micheli, David L. Dill |
| 1993 | ICCAD | Modeling hierarchical combinational circuits. | Jerry R. Burch, David L. Dill, Elizabeth Wolf, Giovanni De Micheli |
| 1993 | ICCAD | Unifying synchronous/asynchronous state machine synthesis. | Kenneth Y. Yun, David L. Dill |
| 1993 | ICCD | Efficient Verification of Symmetric Concurrent Systems. | C. Norris Ip, David L. Dill |
| 1992 | CAV | Verification with Real-Time COSPAN. | Costas Courcoubetis, David L. Dill, Magda Chatzaki, Panagiotis Tzounakis |
| 1992 | CAV | Higher-Level Specification and Verification with BDDs. | Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang |
| 1992 | CONCUR | Minimization of Timed Transition Systems. | Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David L. Dill, Howard Wong-Toi |
| 1992 | ICCAD | Exact two-level minimization of hazard-free logic with multiple-input changes. | Steven M. Nowick, David L. Dill |
| 1992 | ICCAD | Automatic synthesis of 3D asynchronous state machines. | Kenneth Y. Yun, David L. Dill |
| 1992 | ICCD | Protocol Verification as a Hardware Design Aid. | David L. Dill, Andreas J. Drexler, Alan J. Hu, C. Han Yang |
| 1992 | ICCD | Algorithms for Interface Timing Verification. | Kenneth L. McMillan, David L. Dill |
| 1992 | ICCD | Practical Asynchronous Controller Design. | Steven M. Nowick, Kenneth Y. Yun, David L. Dill |
| 1992 | ICCD | Synthesis of 3D Asynchronous State Machines. | Kenneth Y. Yun, David L. Dill, Steven M. Nowick |
| 1992 | RTSS | An implementation of three algorithms for timing verification based on automata emptiness. | Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, Howard Wong-Toi |
| 1991 | CAV | Checking for Language Inclusion Using Simulation Preorders. | David L. Dill, Alan J. Hu, Howard Wong-Toi |
| 1991 | ICALP | Model-Checking for Probabilistic Real-Time Systems (Extended Abstract). | Rajeev Alur, Costas Courcoubetis, David L. Dill |
| 1991 | ICCAD | Automatic Synthesis of Locally-Clocked Asynchronous State Machines. | Steven M. Nowick, David L. Dill |
| 1991 | ICCD | Self-Timed Logic Using Current-Sensing Completion Detection (CSCD). | Mark E. Dean, David L. Dill, Mark Horowitz |
| 1991 | ICCD | Synthesis of Asynchronous State Machines Using A Local Clock. | Steven M. Nowick, David L. Dill |
| 1990 | CAV | Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. | Paul Loewenstein, David L. Dill |
| 1990 | CAV | Synthesizing Processes and Schedulers from Temporal Specifications. | Howard Wong-Toi, David L. Dill |
| 1990 | DAC | Sequential Circuit Verification Using Symbolic Model Checking. | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill |
| 1990 | ICALP | Automata For Modeling Real-Time Systems. | Rajeev Alur, David L. Dill |
| 1990 | ICCD | Formal verification of cache systems using refinement relations. | Paul Loewenstein, David L. Dill |
| 1990 | LICS | Model-Checking for Real-Time Systems | Rajeev Alur, Costas Courcoubetis, David L. Dill |
| 1990 | LICS | Symbolic Model Checking: 10^20 States and Beyond | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang |
| 1989 | ICCAD | Practicality of state-machine verification of speed-independent circuits. | Steven M. Nowick, David L. Dill |
| 1989 | ICCD | Automatic verification of speed-independent circuits with Petri net specifications. | David L. Dill, Steven M. Nowick, Robert F. Sproull |