David L. Dill

Publication Activity (10 Years)

Years Active: 1986-2023
Publications (10 Years): 19

Top Venues

CoRR

CAV (1)

TACAS (1)

ICML

Publications

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67 (3) (2023)
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. 60 (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR (2022)
David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Jingyi Emma Zhong
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. TACAS (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR (2022)
David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Jingyi Emma Zhong
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. CoRR (2021)
Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
Resources: A Safe Language Abstraction for Money. CoRR (2020)
Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill
The Move Prover. CAV (1) (2020)
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
The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV (1) (2019)
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
Learning a SAT Solver from Single-Bit Supervision. ICLR (Poster) (2019)
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
Learning a SAT Solver from Single-Bit Supervision. CoRR (2018)
Daniel Selsam, Percy Liang, David L. Dill
Developing Bug-Free Machine Learning Systems With Formal Mathematics. ICML (2017)
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM (2017)
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR (2017)
Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill
Ground-Truth Adversarial Examples. CoRR (2017)
Daniel Selsam, Percy Liang, David L. Dill
Developing Bug-Free Machine Learning Systems With Formal Mathematics. CoRR (2017)
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) (2017)
Keren Lasker, Jared M. Schrader, Yifei Men, Tyler Marshik, David L. Dill, Harley H. McAdams, Lucy Shapiro
. Nucleic Acids Res. 44 (Database-Issue) (2016)
Subarna Sinha, David L. Dill
Deciphering cancer biology using boolean methods. HLDVT (2016)
Weiruo Zhang, Ritesh Kolte, David L. Dill
Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach. BMC Syst. Biol. 9 (2015)
David L. Dill
Model Checking Cell Biology. CAV (2012)
Eric Lazarus, David L. Dill, Jeremy Epstein
Applying a Reusable Election Threat Model at the County Level. EVT/WOTE (2011)
David L. Dill
Are Cells Asynchronous Circuits? - (Invited Talk). VMCAI (2011)
Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Meng, Garry P. Nolan
Towards program optimization through automated analysis of numerical precision. CGO (2010)
Debashis Sahoo, Jun Seita, Deepta Bhattacharya, Matthew A. Inlay, Irving L. Weissman, Sylvia K. Plevritis, David L. Dill
MiDReG: A method of mining developmentally regulated genes using Boolean implications. Proc. Natl. Acad. Sci. USA 107 (13) (2010)
David L. Dill
. 25 Years of Model Checking (2008)
Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler
EXE: Automatically Generating Inputs of Death. ACM Trans. Inf. Syst. Secur. 12 (2) (2008)
David L. Dill
Formal Verification and Biology. ATVA (2008)
Eric Whitman Smith, David L. Dill
Automatic Formal Verification of Block Cipher Implementations. FMCAD (2008)
David L. Dill, Daniel Castro
Point/counterpoint: The U.S. should ban paperless electronic voting machines. Commun. ACM 51 (10) (2008)
Vijay Ganesh, David L. Dill
A Decision Procedure for Bit-Vectors and Arrays. CAV (2007)
Husam Abu-Haimed, David L. Dill, Sergey Berezin
A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. FMCAD (2006)
David L. Dill
I Think I Voted: E-Voting vs. Democracy. CAV (2006)
Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler
EXE: automatically generating inputs of death. CCS (2006)
Carolyn L. Talcott, David L. Dill
Multiple Representations of Biological Processes. Trans. Comp. Sys. Biology 6 (2006)
Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill
A Practical Approach to Partial Functions in CVC Lite. Electron. Notes Theor. Comput. Sci. 125 (3) (2005)
Madanlal Musuvathi, David L. Dill
An Incremental Heap Canonicalization Algorithm. SPIN (2005)
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
Multi-threaded reachability. DAC (2005)
David L. Dill, Merrill Knapp, Pamela Gage, Carolyn L. Talcott, Keith Laderoute, Patrick Lincoln
The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways. Systems Biology and Regulatory Genomics (2005)
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill
A New Reachability Algorithm for Symmetric Multi-processor Architecture. ATVA (2005)
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
Predictive Reachability Using a Sample-Based Approach. CHARME (2005)
Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson
A Partitioning Methodology for BDD-Based Verification. FMCAD (2004)
Jacob Chang, Sergey Berezin, David L. Dill
Using Interface Refinement to Integrate Formal Verification into the Design Cycle. CAV (2004)
David L. Dill
The battle of accountable voting systems. MEMOCODE (2004)
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
Evaluation of voting systems. Commun. ACM 47 (11) (2004)
David L. Dill, Aviel D. Rubin
Guest Editors' Introduction: E-Voting Security. IEEE Secur. Priv. 2 (1) (2004)
David L. Dill, Patrick Lincoln
Evolution as Design Engineer. CMSB (2003)
Husam Abu-Haimed, Sergey Berezin, David L. Dill
Semi-formal Verification of Memory Systems by Symbolic Simulation. CHARME (2003)
Sergey Berezin, Vijay Ganesh, David L. Dill
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. TACAS (2003)
César Sánchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, Zohar Manna
Event Correlation: Language and Semantics. EMSOFT (2003)
David L. Dill, Bruce Schneier, Barbara Simons
Voting and technology: who gets to count your vote? Commun. ACM 46 (8) (2003)
Husam Abu-Haimed, Sergey Berezin, David L. Dill
Strengthening Invariants by Symbolic Consistency Testing. CAV (2003)
David L. Dill, Nate James, Shishpal Rawat, Gérard Berry, Limor Fix, Harry Foster, Rajeev K. Ranjan, Gunnar Stålmarck, Curt Widdoes
Formal verification methods: getting around the brick wall. DAC (2002)
Clark W. Barrett, David L. Dill, Aaron Stump
A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS (2002)
Satyaki Das, David L. Dill
Counter-Example Based Predicate Discovery in Predicate Abstraction. FMCAD (2002)
Aaron Stump, Clark W. Barrett, David L. Dill
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. Electron. Notes Theor. Comput. Sci. 70 (2) (2002)
Robert B. Jones, Jens U. Skakkebæk, David L. Dill
Formal Verification of Out-of-Order Execution with Incremental Flushing. Formal Methods Syst. Des. 20 (2) (2002)
Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, David L. Dill
CMC: A Pragmatic Approach to Model Checking Real Code. OSDI (2002)
Clark W. Barrett, David L. Dill, Aaron Stump
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV (2002)
Vijay Ganesh, Sergey Berezin, David L. Dill
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. FMCAD (2002)
Kanna Shimizu, David L. Dill
Deriving a simulation input generator and a coverage metric from a formal specification. DAC (2002)
Madanlal Musuvathi, Andy Chou, David L. Dill, Dawson R. Engler
Model checking system software with CMC. ACM SIGOPS European Workshop (2002)
Aaron Stump, Clark W. Barrett, David L. Dill
CVC: A Cooperating Validity Checker. CAV (2002)
Aaron Stump, David L. Dill
Faster Proof Checking in the Edinburgh Logical Framework. CADE (2002)
Kanna Shimizu, David L. Dill
Using Formal Specifications for Functional Validation of Hardware Designs. IEEE Des. Test Comput. 19 (4) (2002)
David Lie, Andy Chou, Dawson R. Engler, David L. Dill
A simple method for extracting models for protocol code. ISCA (2001)
Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt
A Decision Procedure for an Extensional Theory of Arrays. LICS (2001)
Ulrich Stern, David L. Dill
Parallelizing the Murj Verifier. Formal Methods Syst. Des. 18 (2) (2001)
Kanna Shimizu, David L. Dill, Ching-Tsun Chou
Processor Bus Protocol. CHARME (2001)
Satyaki Das, David L. Dill
Successive Approximation of Abstract Transition Relations. LICS (2001)
Kanna Shimizu, David L. Dill, Alan J. Hu
Monitor-Based Formal Specification of PCI. FMCAD (2000)
Shankar G. Govindaraju, David L. Dill
Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. ICCAD (2000)
Seungjoon Park, Satyaki Das, David L. Dill
Automatic checking of aggregation abstractions through stateenumeration. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 19 (10) (2000)
Chris Wilson, David L. Dill
Reliable verification using symbolic simulation with scalar values. DAC (2000)
David L. Dill
Model checking Java programs. FMSP (2000)
David L. Dill
Model checking Java programs (abstract only). ISSTA (2000)
Clark W. Barrett, David L. Dill, Aaron Stump
A Framework for Cooperating Decision Procedures. CADE (2000)
Chris Wilson, David L. Dill, Randal E. Bryant
Symbolic Simulation with Approximate Values. FMCAD (2000)
David Y. W. Park, Ulrich Stern, Jens U. Skakkebæk, David L. Dill
Java Model Checking. ASE (2000)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
Timing analysis of asynchronous systems using time separation of events. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18 (8) (1999)
Ellen Sentovich, David L. Dill, Serdar Tasiran
Formal verification meets simulation (tutorial abstract). ICCAD (1999)
Kenneth Y. Yun, David L. Dill
Automatic synthesis of extended burst-mode circuits. I.(Specification and hazard-free implementations). IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18 (2) (1999)
Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann
Improved Approximate Reachability Using Auxiliary State Variables. DAC (1999)
C. Norris Ip, David L. Dill
Verifying Systems with Replicated Components in Mur[b.phiv]. Formal Methods Syst. Des. 14 (3) (1999)
Shankar G. Govindaraju, David L. Dill
Approximate Symbolic Model Checking using Overlapping Projections. Electron. Notes Theor. Comput. Sci. 23 (2) (1999)
Satyaki Das, David L. Dill, Seungjoon Park
Experience with Predicate Abstraction. CAV (1999)
David L. Dill
Alternative Approaches to Hardware Verification (abstract). CAV (1999)
Kenneth Y. Yun, David L. Dill
Automatic synthesis of extended burst-mode circuits. II. (Automaticsynthesis). IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18 (2) (1999)
Seungjoon Park, David L. Dill
An Executable Specification and Verifier for Relaxed Memory Order. IEEE Trans. Computers 48 (2) (1999)
David Y. W. Park, Jens U. Skakkebæk, David L. Dill
Static Analysis to Identify Invariants in RSML Specifications. FTRTFT (1998)
Seungjoon Park, David L. Dill
Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions. Theory Comput. Syst. 31 (4) (1998)
Clark W. Barrett, David L. Dill, Jeremy R. Levitt
A Decision Procedure for Bit-Vector Arithmetic. DAC (1998)
Ulrich Stern, David L. Dill
Verifier. CAV (1998)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
Practical timing analysis of asynchronous circuits using time separation of events. CICC (1998)
Shankar G. Govindaraju, David L. Dill
Verification by approximate forward and backward reachability. ICCAD (1998)
C. Han Yang, David L. Dill
Validation with Guided Search of the State Space. DAC (1998)
David L. Dill
What's Between Simulation and Formal Verification? (Extended Abstract). DAC (1998)
Robert B. Jones, Jens U. Skakkebæk, David L. Dill
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. FMCAD (1998)
Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz
Approximate Reachability with BDDs Using Overlapping Projections. DAC (1998)
David Y. W. Park, Jens U. Skakkebæk, Mats Per Erik Heimdahl, Barbara J. Czerny, David L. Dill
Checking properties of safety critical specifications using efficient decision procedures. FMSP (1998)

David L. Dill.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David L. Dill