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]Ulrich Stern, David L. Dill:
A New Scheme for Memory-Efficient Probabilistic Verification. FORTE 1996: 333-348 - [c49]Seungjoon Park, David L. Dill:
Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. SPAA 1996: 288-296 - 1995
- [j9]Steven M. Nowick, David L. Dill:
Exact two-level minimization of hazard-free logic with multiple-input changes. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 14(8): 986-997 (1995) - [c48]David L. Dill, Howard Wong-Toi:
Verification of Real-Time Systems by Successive Over and Under Approximation. CAV 1995: 409-422 - [c47]Ulrich Stern, David L. Dill:
Automatic verification of the SCI cache coherence protocol. CHARME 1995: 21-34 - [c46]Ulrich Stern, David L. Dill:
Improved probabilistic verification by hash compaction. CHARME 1995: 206-224 - [c45]Robert B. Jones, David L. Dill, Jerry R. Burch:
Efficient validity checking for processor verification. ICCAD 1995: 2-6 - [c44]Kenneth Y. Yun, David L. Dill:
A high-performance asynchronous SCSI controller. ICCD 1995: 44-49 - [c43]Richard C. Ho, C. Han Yang, Mark Horowitz, David L. Dill:
Architecture Validation for Processors. ISCA 1995: 404-413 - [c42]Seungjoon Park, David L. Dill:
An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order). SPAA 1995: 34-41 - 1994
- [j8]Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill:
Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4): 401-424 (1994) - [j7]Rajeev Alur, David L. Dill:
A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183-235 (1994) - [j6]Mark E. Dean, David L. Dill, Mark Horowitz:
Self-timed logic using Current-Sensing Completion Detection (CSCD). J. VLSI Signal Process. 7(1-2): 7-16 (1994) - [c41]Jerry R. Burch, David L. Dill:
Automatic verification of Pipelined Microprocessor Control. CAV 1994: 68-80 - [c40]David L. Dill:
Hierarchical Models of Synchronous Circuits (Abstract). CONCUR 1994: 161 - [c39]Alan J. Hu, Gary York, David L. Dill:
New Techniques for Efficient Verification with Implicitly Conjoined BDDs. DAC 1994: 276-282 - [c38]Kenneth Y. Yun, Bill Lin, David L. Dill, Srinivas Devadas:
Performance-driven synthesis of asynchronous controllers. ICCAD 1994: 550-557 - [e1]David L. Dill:
Computer Aided Verification, 6th International Conference, CAV '94, Stanford, California, USA, June 21-23, 1994, Proceedings. Lecture Notes in Computer Science 818, Springer 1994, ISBN 3-540-58179-0 [contents] - 1993
- [j5]Rajeev Alur, Costas Courcoubetis, David L. Dill:
Model-Checking in Dense Real-time. Inf. Comput. 104(1): 2-34 (1993) - [j4]Steven M. Nowick, Mark E. Dean, David L. Dill, Mark Horowitz:
The design of a high-performance cache controller: a case study in asynchronous synthesis. Integr. 15(3): 241-262 (1993) - [c37]Alan J. Hu, David L. Dill:
Efficient Verification with BDDs using Implicitly Conjoined Invariants. CAV 1993: 3-14 - [c36]C. Norris Ip, David L. Dill:
Better Verification Through Symmetry. CHDL 1993: 97-111 - [c35]Polly Siegel, Giovanni De Micheli, David L. Dill:
Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs. DAC 1993: 61-67 - [c34]Alan J. Hu, David L. Dill:
Reducing BDD Size by Exploiting Functional Dependencies. DAC 1993: 266-271 - [c33]Kenneth Y. Yun, David L. Dill:
Unifying synchronous/asynchronous state machine synthesis. ICCAD 1993: 255-260 - [c32]Jerry R. Burch, David L. Dill, Elizabeth Wolf, Giovanni De Micheli:
Modeling hierarchical combinational circuits. ICCAD 1993: 612-617 - [c31]C. Norris Ip, David L. Dill:
Efficient Verification of Symmetric Concurrent Systems. ICCD 1993: 230-234 - 1992
- [j3]David L. Dill, Steven M. Nowick, Robert F. Sproull:
Specification and Automatic Verification of Self-Timed Queues. Formal Methods Syst. Des. 1(1): 29-60 (1992) - [j2]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang:
Symbolic Model Checking: 10^20 States and Beyond. Inf. Comput. 98(2): 142-170 (1992) - [c30]Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang:
Higher-Level Specification and Verification with BDDs. CAV 1992: 82-95 - [c29]Costas Courcoubetis, David L. Dill, Magda Chatzaki, Panagiotis Tzounakis:
Verification with Real-Time COSPAN. CAV 1992: 274-287 - [c28]Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David L. Dill, Howard Wong-Toi:
Minimization of Timed Transition Systems. CONCUR 1992: 340-354 - [c27]Kenneth Y. Yun, David L. Dill:
Automatic synthesis of 3D asynchronous state machines. ICCAD 1992: 576-580 - [c26]Steven M. Nowick, David L. Dill:
Exact two-level minimization of hazard-free logic with multiple-input changes. ICCAD 1992: 626-630 - [c25]Kenneth L. McMillan, David L. Dill:
Algorithms for Interface Timing Verification. ICCD 1992: 48-51 - [c24]Steven M. Nowick, Kenneth Y. Yun, David L. Dill:
Practical Asynchronous Controller Design. ICCD 1992: 341-345 - [c23]Kenneth Y. Yun, David L. Dill, Steven M. Nowick:
Synthesis of 3D Asynchronous State Machines. ICCD 1992: 346-350 - [c22]David L. Dill, Andreas J. Drexler, Alan J. Hu, C. Han Yang:
Protocol Verification as a Hardware Design Aid. ICCD 1992: 522-525 - [c21]Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, Howard Wong-Toi:
An implementation of three algorithms for timing verification based on automata emptiness. RTSS 1992: 157-166 - 1991
- [c20]David L. Dill, Alan J. Hu, Howard Wong-Toi:
Checking for Language Inclusion Using Simulation Preorders. CAV 1991: 255-265 - [c19]Rajeev Alur, Costas Courcoubetis, David L. Dill:
Model-Checking for Probabilistic Real-Time Systems (Extended Abstract). ICALP 1991: 115-126 - [c18]Steven M. Nowick, David L. Dill:
Automatic Synthesis of Locally-Clocked Asynchronous State Machines. ICCAD 1991: 318-321 - [c17]Mark E. Dean, David L. Dill, Mark Horowitz:
Self-Timed Logic Using Current-Sensing Completion Detection (CSCD). ICCD 1991: 187-191 - [c16]Steven M. Nowick, David L. Dill:
Synthesis of Asynchronous State Machines Using A Local Clock. ICCD 1991: 192-197 - [c15]Rajeev Alur, Costas Courcoubetis, David L. Dill:
Verifying Automata Specifications of Probabilistic Real-time Systems. REX Workshop 1991: 28-44 - [c14]Rajeev Alur, David L. Dill:
The Theory of Timed Automata. REX Workshop 1991: 45-73 - 1990
- [c13]Howard Wong-Toi, David L. Dill:
Synthesizing Processes and Schedulers from Temporal Specifications. CAV 1990: 272-281 - [c12]Paul Loewenstein, David L. Dill:
Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. CAV 1990: 302-311 - [c11]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill:
Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51 - [c10]Howard Wong-Toi, David L. Dill:
Synthesizing Processes and Schedulers from Temporal Specifications. CAV (DIMACS/AMS volume) 1990: 177-186 - [c9]Paul Loewenstein, David L. Dill:
Verification of Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. CAV (DIMACS/AMS volume) 1990: 187-206 - [c8]Rajeev Alur, David L. Dill:
Automata For Modeling Real-Time Systems. ICALP 1990: 322-335 - [c7]Paul Loewenstein, David L. Dill:
Formal verification of cache systems using refinement relations. ICCD 1990: 228-233 - [c6]Rajeev Alur, Costas Courcoubetis, David L. Dill:
Model-Checking for Real-Time Systems. LICS 1990: 414-425 - [c5]Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang:
Symbolic Model Checking: 10^20 States and Beyond. LICS 1990: 428-439
1980 – 1989
- 1989
- [b1]David L. Dill:
Trace theory for automatic hierarchical verification of speed-independent circuits. ACM distinguished dissertations, MIT Press 1989, ISBN 978-0-262-04101-0, pp. 1-163 - [c4]David L. Dill:
Timing Assumptions and Verification of Finite-State Concurrent Systems. Automatic Verification Methods for Finite State Systems 1989: 197-212 - [c3]Steven M. Nowick, David L. Dill:
Practicality of state-machine verification of speed-independent circuits. ICCAD 1989: 266-269 - [c2]David L. Dill, Steven M. Nowick, Robert F. Sproull:
Automatic verification of speed-independent circuits with Petri net specifications. ICCD 1989: 212-216 - [c1]David L. Dill:
Complete Trace Structures. Hardware Specification, Verification and Synthesis 1989: 224-243 - 1986
- [j1]Michael C. Browne, Edmund M. Clarke, David L. Dill, Bud Mishra:
Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Trans. Computers 35(12): 1035-1044 (1986)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-06-28 23:43 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
