default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDavid L. Dill
Person information
- affiliation: Stanford University, Department of Computer Science, CA, USA
- award (2004): EFF Pioneer Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[j33]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): 32 (2023)- 2022
- [j32]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): 87-116 (2022) - [c136]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: 125-143 - [c135]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: 183-200 - [i7]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 abs/2205.08095 (2022) - 2021
- [i6]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 abs/2110.08362 (2021) - 2020
- [c134]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: 137-150 - [i5]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 abs/2004.05106 (2020)
2010 – 2019
- 2019
- [c133]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: 443-452 - [c132]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 - 2018
- [i4]Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill:
Learning a SAT Solver from Single-Bit Supervision. CoRR abs/1802.03685 (2018) - 2017
- [c131]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: 97-117 - [c130]Daniel Selsam, Percy Liang, David L. Dill:
Developing Bug-Free Machine Learning Systems With Formal Mathematics. ICML 2017: 3047-3056 - [c129]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: 19-26 - [i3]Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs/1702.01135 (2017) - [i2]Daniel Selsam, Percy Liang, David L. Dill:
Developing Bug-Free Machine Learning Systems With Formal Mathematics. CoRR abs/1706.08605 (2017) - [i1]Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill:
Ground-Truth Adversarial Examples. CoRR abs/1709.10207 (2017) - 2016
- [j31]Keren Lasker, Jared M. Schrader, Yifei Men, Tyler Marshik, David L. Dill, Harley H. McAdams, Lucy Shapiro:
CauloBrowser: A systems biology resource for Caulobacter crescentus. Nucleic Acids Res. 44(Database-Issue): 640-645 (2016) - [c128]Subarna Sinha, David L. Dill:
Deciphering cancer biology using boolean methods. HLDVT 2016: 150-154 - 2015
- [j30]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: 66 (2015) - 2012
- [c127]David L. Dill:
Model Checking Cell Biology. CAV 2012: 2 - 2011
- [c126]Eric Lazarus, David L. Dill, Jeremy Epstein:
Applying a Reusable Election Threat Model at the County Level. EVT/WOTE 2011 - [c125]David L. Dill:
Are Cells Asynchronous Circuits? - (Invited Talk). VMCAI 2011: 1 - 2010
- [j29]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): 5732-5737 (2010) - [c124]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: 230-237
2000 – 2009
- 2008
- [j28]David L. Dill, Daniel Castro:
Point/counterpoint: The U.S. should ban paperless electronic voting machines. Commun. ACM 51(10): 29-33 (2008) - [j27]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): 10:1-10:38 (2008) - [c123]David L. Dill:
Formal Verification and Biology. ATVA 2008: 3 - [c122]Eric Whitman Smith, David L. Dill:
Automatic Formal Verification of Block Cipher Implementations. FMCAD 2008: 1-7 - [c121]David L. Dill:
A Retrospective on Murphi. 25 Years of Model Checking 2008: 77-88 - [e2]David L. Dill, Tadayoshi Kohno:
2008 USENIX/ACCURATE Electronic Voting Workshop, EVT 2008, July 28-29, 2008, San Jose, CA, USA, Proceedings. USENIX Association 2008 [contents] - 2007
- [c120]Vijay Ganesh, David L. Dill:
A Decision Procedure for Bit-Vectors and Arrays. CAV 2007: 519-531 - 2006
- [j26]Carolyn L. Talcott, David L. Dill:
Multiple Representations of Biological Processes. Trans. Comp. Sys. Biology 6: 221-245 (2006) - [c119]David L. Dill:
I Think I Voted: E-Voting vs. Democracy. CAV 2006: 2 - [c118]Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler:
EXE: automatically generating inputs of death. CCS 2006: 322-335 - [c117]Husam Abu-Haimed, David L. Dill, Sergey Berezin:
A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. FMCAD 2006: 145-152 - 2005
- [c116]Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill:
A New Reachability Algorithm for Symmetric Multi-processor Architecture. ATVA 2005: 26-38 - [c115]Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson:
Predictive Reachability Using a Sample-Based Approach. CHARME 2005: 388-392 - [c114]Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson:
Multi-threaded reachability. DAC 2005: 467-470 - [c113]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: 11-22 - [c112]Madanlal Musuvathi, David L. Dill:
An Incremental Heap Canonicalization Algorithm. SPIN 2005: 28-42 - 2004
- [j25]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): 144 (2004) - [j24]David L. Dill, Aviel D. Rubin:
Guest Editors' Introduction: E-Voting Security. IEEE Secur. Priv. 2(1): 22-23 (2004) - [c111]Jacob Chang, Sergey Berezin, David L. Dill:
Using Interface Refinement to Integrate Formal Verification into the Design Cycle. CAV 2004: 122-134 - [c110]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: 399-413 - [c109]David L. Dill:
The battle of accountable voting systems. MEMOCODE 2004: 105 - [c108]Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill:
A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR 2004: 13-23 - 2003
- [j23]David L. Dill, Bruce Schneier, Barbara Simons:
Voting and technology: who gets to count your vote? Commun. ACM 46(8): 29-31 (2003) - [c107]Husam Abu-Haimed, Sergey Berezin, David L. Dill:
Strengthening Invariants by Symbolic Consistency Testing. CAV 2003: 407-419 - [c106]Husam Abu-Haimed, Sergey Berezin, David L. Dill:
Semi-formal Verification of Memory Systems by Symbolic Simulation. CHARME 2003: 158-163 - [c105]David L. Dill, Patrick Lincoln:
Evolution as Design Engineer. CMSB 2003: 202-206 - [c104]César Sánchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, Zohar Manna:
Event Correlation: Language and Semantics. EMSOFT 2003: 323-339 - [c103]Sergey Berezin, Vijay Ganesh, David L. Dill:
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. TACAS 2003: 521-536 - 2002
- [j22]Kanna Shimizu, David L. Dill:
Using Formal Specifications for Functional Validation of Hardware Designs. IEEE Des. Test Comput. 19(4): 96-106 (2002) - [j21]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): 139-158 (2002) - [c102]Aaron Stump, David L. Dill:
Faster Proof Checking in the Edinburgh Logical Framework. CADE 2002: 392-407 - [c101]Clark W. Barrett, David L. Dill, Aaron Stump:
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV 2002: 236-249 - [c100]Aaron Stump, Clark W. Barrett, David L. Dill:
CVC: A Cooperating Validity Checker. CAV 2002: 500-504 - [c99]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: 576-577 - [c98]Kanna Shimizu, David L. Dill:
Deriving a simulation input generator and a coverage metric from a formal specification. DAC 2002: 801-806 - [c97]Satyaki Das, David L. Dill:
Counter-Example Based Predicate Discovery in Predicate Abstraction. FMCAD 2002: 19-32 - [c96]Vijay Ganesh, Sergey Berezin, David L. Dill:
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. FMCAD 2002: 171-186 - [c95]Clark W. Barrett, David L. Dill, Aaron Stump:
A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS 2002: 132-146 - [c94]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 - [c93]Madanlal Musuvathi, Andy Chou, David L. Dill, Dawson R. Engler:
Model checking system software with CMC. ACM SIGOPS European Workshop 2002: 219-222 - [c92]Aaron Stump, Clark W. Barrett, David L. Dill:
Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM 2002: 29-41 - 2001
- [j20]Ulrich Stern, David L. Dill:
Parallelizing the Murj Verifier. Formal Methods Syst. Des. 18(2): 117-129 (2001) - [c91]Kanna Shimizu, David L. Dill, Ching-Tsun Chou:
A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol. CHARME 2001: 340-354 - [c90]David Lie, Andy Chou, Dawson R. Engler, David L. Dill:
A simple method for extracting models for protocol code. ISCA 2001: 192-203 - [c89]Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37 - [c88]Satyaki Das, David L. Dill:
Successive Approximation of Abstract Transition Relations. LICS 2001: 51-58 - 2000
- [j19]Seungjoon Park, Satyaki Das, David L. Dill:
Automatic checking of aggregation abstractions through stateenumeration. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 19(10): 1202-1210 (2000) - [c87]Clark W. Barrett, David L. Dill, Aaron Stump:
A Framework for Cooperating Decision Procedures. CADE 2000: 79-98 - [c86]Chris Wilson, David L. Dill:
Reliable verification using symbolic simulation with scalar values. DAC 2000: 124-129 - [c85]Kanna Shimizu, David L. Dill, Alan J. Hu:
Monitor-Based Formal Specification of PCI. FMCAD 2000: 335-353 - [c84]Chris Wilson, David L. Dill, Randal E. Bryant:
Symbolic Simulation with Approximate Values. FMCAD 2000: 470-485 - [c83]David L. Dill:
Model checking Java programs. FMSP 2000: 1 - [c82]Shankar G. Govindaraju, David L. Dill:
Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. ICCAD 2000: 115-119 - [c81]David L. Dill:
Model checking Java programs (abstract only). ISSTA 2000: 179 - [c80]David Y. W. Park, Ulrich Stern, Jens U. Skakkebæk, David L. Dill:
Java Model Checking. ASE 2000: 253-256
1990 – 1999
- 1999
- [j18]C. Norris Ip, David L. Dill:
Verifying Systems with Replicated Components in Mur[b.phiv]. Formal Methods Syst. Des. 14(3): 273-310 (1999) - [j17]Seungjoon Park, David L. Dill:
An Executable Specification and Verifier for Relaxed Memory Order. IEEE Trans. Computers 48(2): 227-235 (1999) - [j16]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): 101-117 (1999) - [j15]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): 118-132 (1999) - [j14]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): 1061-1076 (1999) - [c79]David L. Dill:
Alternative Approaches to Hardware Verification (abstract). CAV 1999: 1 - [c78]Satyaki Das, David L. Dill, Seungjoon Park:
Experience with Predicate Abstraction. CAV 1999: 160-171 - [c77]Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann:
Improved Approximate Reachability Using Auxiliary State Variables. DAC 1999: 312-316 - [c76]Ellen Sentovich, David L. Dill, Serdar Tasiran:
Formal verification meets simulation (tutorial abstract). ICCAD 1999: 221 - [c75]Shankar G. Govindaraju, David L. Dill:
Approximate Symbolic Model Checking using Overlapping Projections. SMC@FLoC 1999: 23-33 - 1998
- [j13]Seungjoon Park, David L. Dill:
Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions. Theory Comput. Syst. 31(4): 355-376 (1998) - [j12]Kenneth Y. Yun, Bill Lin, David L. Dill, Srinivas Devadas:
BDD-based synthesis of extended burst-mode controllers. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 17(9): 782-792 (1998) - [c74]Jens U. Skakkebæk, Robert B. Jones, David L. Dill:
Formal Verification of Out-of-Order Execution Using Incremental Flushing. CAV 1998: 98-109 - [c73]Ulrich Stern, David L. Dill:
Using Magnatic Disk Instead of Main Memory in the Murphi Verifier. CAV 1998: 172-183 - [c72]Supratik Chakraborty, Kenneth Y. Yun, David L. Dill:
Practical timing analysis of asynchronous circuits using time separation of events. CICC 1998: 455-458 - [c71]David L. Dill:
What's Between Simulation and Formal Verification? (Extended Abstract). DAC 1998: 328-329 - [c70]Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz:
Approximate Reachability with BDDs Using Overlapping Projections. DAC 1998: 451-456 - [c69]Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for Bit-Vector Arithmetic. DAC 1998: 522-527 - [c68]C. Han Yang, David L. Dill:
Validation with Guided Search of the State Space. DAC 1998: 599-604 - [c67]Robert B. Jones, Jens U. Skakkebæk, David L. Dill:
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. FMCAD 1998: 2-17 - [c66]Jeffrey X. Su, David L. Dill, Jens U. Skakkebæk:
Formally Verifying Data and Control with Weak Reachability Invariants. FMCAD 1998: 387-402 - [c65]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: 34-43 - [c64]David Y. W. Park, Jens U. Skakkebæk, David L. Dill:
Static Analysis to Identify Invariants in RSML Specifications. FTRTFT 1998: 133-142 - [c63]Shankar G. Govindaraju, David L. Dill:
Verification by approximate forward and backward reachability. ICCAD 1998: 366-370 - 1997
- [c62]Supratik Chakraborty, David L. Dill, Kun-Yung Chang, Kenneth Y. Yun:
Timing Analysis of Extended Burst-Mode Circuits. ASYNC 1997: 101-111 - [c61]Supratik Chakraborty, David L. Dill:
More Accurate Polynomial-Time Min-Max Timing Simulation. ASYNC 1997: 112- - [c60]Ulrich Stern, David L. Dill:
Parallelizing the Murphi Verifier. CAV 1997: 256-278 - [c59]Seungjoon Park, Satyaki Das, David L. Dill:
Automatic Checking of Aggregation Abstractions Through State Enumeration. FORTE 1997: 207-222 - [c58]Supratik Chakraborty, David L. Dill:
Approximate algorithms for time separation of events. ICCAD 1997: 190-194 - 1996
- [j11]Jonathan P. Bowen, Ricky W. Butler, David L. Dill, Robert L. Glass, David Gries, Anthony Hall, Michael G. Hinchey, C. Michael Holloway, Daniel Jackson, Cliff B. Jones, Michael J. Lutz, David Lorge Parnas, John M. Rushby, Jeannette M. Wing, Pamela Zave:
An Invitation to Formal Methods. Computer 29(4): 16-30 (1996) - [j10]C. Norris Ip, David L. Dill:
Better Verification Through Symmetry. Formal Methods Syst. Des. 9(1/2): 41-75 (1996) - [c57]C. Norris Ip, David L. Dill:
Verifying Systems with Replicated Components in Murphi. CAV 1996: 147-158 - [c56]Seungjoon Park, David L. Dill:
Protocol Verification by Aggregation of Distributed Transactions. CAV 1996: 300-310 - [c55]David L. Dill:
The Murphi Verification System. CAV 1996: 390-393 - [c54]C. Norris Ip, David L. Dill:
State Reduction Using Reversible Rules. DAC 1996: 564-567 - [c53]Robert B. Jones, Carl-Johan H. Seger, David L. Dill:
Self-Consistency Checking. FMCAD 1996: 159-171 - [c52]Clark W. Barrett, David L. Dill, Jeremy R. Levitt:
Validity Checking for Combinations of Theories with Equality. FMCAD 1996: 187-201 - [c51]Jeffrey X. Su, David L. Dill, Clark W. Barrett:
Automatic Generation of Invariants in Processor Verification. FMCAD 1996: 377-388 - [c50]