David L. Dill - RankMe

183 papers A* 50A 19B 19C 13Misc 1Journal 42Unranked 37

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. TACAS (2) Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2025	—	`conf`	ClassInvGen: Class Invariant Synthesis Using Large Language Models. SAIV Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025	J	`jnl`	ClassInvGen: Class Invariant Synthesis using Large Language Models. CoRR Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark W. Barrett, David L. Dill, Xiaokang Qiu, Shuvendu K. Lahiri
2025	J	`jnl`	VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. CoRR Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu K. Lahiri, Shan Lu, David L. Dill, Clark W. Barrett
2023	J	`jnl`	Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	—	`conf`	Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. TACAS (1) David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Jingyi Emma Zhong
2022	A	`conf`	Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Reasoning About Vectors using an SMT Theory of Sequences. CoRR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2021	J	`jnl`	Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. CoRR David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Jingyi Emma Zhong
2020	J	`jnl`	Resources: A Safe Language Abstraction for Money. CoRR Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
2020	—	`conf`	The Move Prover. CAV (1) Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill
2019	—	`conf`	Learning a SAT Solver from Single-Bit Supervision. ICLR (Poster) Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
2019	—	`conf`	The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV (1) 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
2018	J	`jnl`	Learning a SAT Solver from Single-Bit Supervision. CoRR Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill
2017	A*	`conf`	Developing Bug-Free Machine Learning Systems With Formal Mathematics. ICML Daniel Selsam, Percy Liang, David L. Dill
2017	J	`jnl`	Developing Bug-Free Machine Learning Systems With Formal Mathematics. CoRR Daniel Selsam, Percy Liang, David L. Dill
2017	J	`jnl`	Ground-Truth Adversarial Examples. CoRR Nicholas Carlini, Guy Katz, Clark W. Barrett, David L. Dill
2017	—	`conf`	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV (1) Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2017	J	`jnl`	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2017	—	`conf`	Towards Proving the Adversarial Robustness of Deep Neural Networks. FVAV@iFM Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer
2016	J	`jnl`	CauloBrowser: A systems biology resource for Nucleic Acids Res. Keren Lasker, Jared M. Schrader, Yifei Men, Tyler Marshik, David L. Dill, Harley H. McAdams, Lucy Shapiro
2016	—	`conf`	Deciphering cancer biology using boolean methods. HLDVT Subarna Sinha, David L. Dill
2015	J	`jnl`	Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach. BMC Syst. Biol. Weiruo Zhang, Ritesh Kolte, David L. Dill
2012	A*	`conf`	Model Checking Cell Biology. CAV David L. Dill
2011	—	`conf`	Applying a Reusable Election Threat Model at the County Level. EVT/WOTE Eric Lazarus, David L. Dill, Jeremy Epstein
2011	B	`conf`	Are Cells Asynchronous Circuits? - (Invited Talk). VMCAI David L. Dill
2010	J	`jnl`	MiDReG: A method of mining developmentally regulated genes using Boolean implications. Proc. Natl. Acad. Sci. USA Debashis Sahoo, Jun Seita, Deepta Bhattacharya, Matthew A. Inlay, Irving L. Weissman, Sylvia K. Plevritis, David L. Dill
2010	A	`conf`	Towards program optimization through automated analysis of numerical precision. CGO Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Meng, Garry P. Nolan
2008	—	`ed.`	2008 USENIX/ACCURATE Electronic Voting Workshop, EVT 2008, July 28-29, 2008, San Jose, CA, USA, Proceedings EVT David L. Dill, Tadayoshi Kohno
2008	—	`conf`	A Retrospective on Mur 25 Years of Model Checking David L. Dill
2008	B	`conf`	Automatic Formal Verification of Block Cipher Implementations. FMCAD Eric Whitman Smith, David L. Dill
2008	J	`jnl`	EXE: Automatically Generating Inputs of Death. ACM Trans. Inf. Syst. Secur. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler
2008	B	`conf`	Formal Verification and Biology. ATVA David L. Dill
2008	J	`jnl`	Point/counterpoint: The U.S. should ban paperless electronic voting machines. Commun. ACM David L. Dill, Daniel Castro
2007	A*	`conf`	A Decision Procedure for Bit-Vectors and Arrays. CAV Vijay Ganesh, David L. Dill
2006	B	`conf`	A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. FMCAD Husam Abu-Haimed, David L. Dill, Sergey Berezin
2006	A*	`conf`	EXE: automatically generating inputs of death. CCS Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler
2006	A*	`conf`	I Think I Voted: E-Voting vs. Democracy. CAV David L. Dill
2006	J	`jnl`	Multiple Representations of Biological Processes. Trans. Comp. Sys. Biology Carolyn L. Talcott, David L. Dill
2005	B	`conf`	A New Reachability Algorithm for Symmetric Multi-processor Architecture. ATVA Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill
2005	—	`conf`	An Incremental Heap Canonicalization Algorithm. SPIN Madanlal Musuvathi, David L. Dill
2005	A*	`conf`	Multi-threaded reachability. DAC Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
2005	—	`conf`	Predictive Reachability Using a Sample-Based Approach. CHARME Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill, E. Allen Emerson
2005	—	`conf`	The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways. Systems Biology and Regulatory Genomics David L. Dill, Merrill Knapp, Pamela Gage, Carolyn L. Talcott, Keith Laderoute, Patrick Lincoln
2004	B	`conf`	A Partitioning Methodology for BDD-Based Verification. FMCAD Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill, E. Allen Emerson
2004	—	`conf`	A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill
2004	J	`jnl`	Evaluation of voting systems. Commun. ACM 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
2004	J	`jnl`	Guest Editors' Introduction: E-Voting Security. IEEE Secur. Priv. David L. Dill, Aviel D. Rubin
2004	C	`conf`	The battle of accountable voting systems. MEMOCODE David L. Dill
2004	A*	`conf`	Using Interface Refinement to Integrate Formal Verification into the Design Cycle. CAV Jacob Chang, Sergey Berezin, David L. Dill
2003	A	`conf`	An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. TACAS Sergey Berezin, Vijay Ganesh, David L. Dill
2003	Misc	`conf`	Event Correlation: Language and Semantics. EMSOFT César Sánchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, Zohar Manna
2003	—	`conf`	Evolution as Design Engineer. CMSB David L. Dill, Patrick Lincoln
2003	—	`conf`	Semi-formal Verification of Memory Systems by Symbolic Simulation. CHARME Husam Abu-Haimed, Sergey Berezin, David L. Dill
2003	A*	`conf`	Strengthening Invariants by Symbolic Consistency Testing. CAV Husam Abu-Haimed, Sergey Berezin, David L. Dill
2003	J	`jnl`	Voting and technology: who gets to count your vote? Commun. ACM David L. Dill, Bruce Schneier, Barbara Simons
2002	—	`conf`	A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS Clark W. Barrett, David L. Dill, Aaron Stump
2002	A*	`conf`	CMC: A Pragmatic Approach to Model Checking Real Code. OSDI Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, David L. Dill
2002	A*	`conf`	CVC: A Cooperating Validity Checker. CAV Aaron Stump, Clark W. Barrett, David L. Dill
2002	A*	`conf`	Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV Clark W. Barrett, David L. Dill, Aaron Stump
2002	B	`conf`	Counter-Example Based Predicate Discovery in Predicate Abstraction. FMCAD Satyaki Das, David L. Dill
2002	B	`conf`	Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. FMCAD Vijay Ganesh, Sergey Berezin, David L. Dill
2002	A*	`conf`	Deriving a simulation input generator and a coverage metric from a formal specification. DAC Kanna Shimizu, David L. Dill
2002	A	`conf`	Faster Proof Checking in the Edinburgh Logical Framework. CADE Aaron Stump, David L. Dill
2002	J	`jnl`	Formal Verification of Out-of-Order Execution with Incremental Flushing. Formal Methods Syst. Des. Robert B. Jones, Jens U. Skakkebæk, David L. Dill
2002	A*	`conf`	Formal verification methods: getting around the brick wall. DAC David L. Dill, Nate James, Shishpal Rawat, Gérard Berry, Limor Fix, Harry Foster, Rajeev K. Ranjan, Gunnar Stålmarck, Curt Widdoes
2002	—	`conf`	Model checking system software with CMC. ACM SIGOPS European Workshop Madanlal Musuvathi, Andy Chou, David L. Dill, Dawson R. Engler
2002	—	`conf`	Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. LFM Aaron Stump, Clark W. Barrett, David L. Dill
2002	J	`jnl`	Using Formal Specifications for Functional Validation of Hardware Designs. IEEE Des. Test Comput. Kanna Shimizu, David L. Dill
2001	A*	`conf`	A Decision Procedure for an Extensional Theory of Arrays. LICS Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt
2001	—	`conf`	A Specification Methodology by a Collection of Compact Properties as Applied to the Intel CHARME Kanna Shimizu, David L. Dill, Ching-Tsun Chou
2001	A*	`conf`	A simple method for extracting models for protocol code. ISCA David Lie, Andy Chou, Dawson R. Engler, David L. Dill
2001	J	`jnl`	Parallelizing the Murj Verifier. Formal Methods Syst. Des. Ulrich Stern, David L. Dill
2001	A*	`conf`	Successive Approximation of Abstract Transition Relations. LICS Satyaki Das, David L. Dill
2000	A	`conf`	A Framework for Cooperating Decision Procedures. CADE Clark W. Barrett, David L. Dill, Aaron Stump
2000	J	`jnl`	Automatic checking of aggregation abstractions through stateenumeration. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Seungjoon Park, Satyaki Das, David L. Dill
2000	A	`conf`	Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking. ICCAD Shankar G. Govindaraju, David L. Dill
2000	A*	`conf`	Java Model Checking. ASE David Y. W. Park, Ulrich Stern, Jens U. Skakkebæk, David L. Dill
2000	A	`conf`	Model checking Java programs (abstract only). ISSTA David L. Dill
2000	—	`conf`	Model checking Java programs. FMSP David L. Dill
2000	B	`conf`	Monitor-Based Formal Specification of PCI. FMCAD Kanna Shimizu, David L. Dill, Alan J. Hu
2000	A*	`conf`	Reliable verification using symbolic simulation with scalar values. DAC Chris Wilson, David L. Dill
2000	B	`conf`	Symbolic Simulation with Approximate Values. FMCAD Chris Wilson, David L. Dill, Randal E. Bryant
1999	A*	`conf`	Alternative Approaches to Hardware Verification (abstract). CAV David L. Dill
1999	J	`jnl`	An Executable Specification and Verifier for Relaxed Memory Order. IEEE Trans. Computers Seungjoon Park, David L. Dill
1999	—	`conf`	Approximate Symbolic Model Checking using Overlapping Projections. SMC@FLoC Shankar G. Govindaraju, David L. Dill
1999	J	`jnl`	Automatic synthesis of extended burst-mode circuits. I.(Specification and hazard-free implementations). IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Kenneth Y. Yun, David L. Dill
1999	J	`jnl`	Automatic synthesis of extended burst-mode circuits. II. (Automaticsynthesis). IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Kenneth Y. Yun, David L. Dill
1999	A*	`conf`	Experience with Predicate Abstraction. CAV Satyaki Das, David L. Dill, Seungjoon Park
1999	A	`conf`	Formal verification meets simulation (tutorial abstract). ICCAD Ellen Sentovich, David L. Dill, Serdar Tasiran
1999	A*	`conf`	Improved Approximate Reachability Using Auxiliary State Variables. DAC Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann
1999	J	`jnl`	Timing analysis of asynchronous systems using time separation of events. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
1999	J	`jnl`	Verifying Systems with Replicated Components in Mur[b.phiv]. Formal Methods Syst. Des. C. Norris Ip, David L. Dill
1998	A*	`conf`	A Decision Procedure for Bit-Vector Arithmetic. DAC Clark W. Barrett, David L. Dill, Jeremy R. Levitt
1998	A*	`conf`	Approximate Reachability with BDDs Using Overlapping Projections. DAC Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz
1998	J	`jnl`	BDD-based synthesis of extended burst-mode controllers. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Kenneth Y. Yun, Bill Lin, David L. Dill, Srinivas Devadas
1998	—	`conf`	Checking properties of safety critical specifications using efficient decision procedures. FMSP David Y. W. Park, Jens U. Skakkebæk, Mats Per Erik Heimdahl, Barbara J. Czerny, David L. Dill
1998	A*	`conf`	Formal Verification of Out-of-Order Execution Using Incremental Flushing. CAV Jens U. Skakkebæk, Robert B. Jones, David L. Dill
1998	B	`conf`	Formally Verifying Data and Control with Weak Reachability Invariants. FMCAD Jeffrey X. Su, David L. Dill, Jens U. Skakkebæk
1998	—	`conf`	Practical timing analysis of asynchronous circuits using time separation of events. CICC Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
1998	B	`conf`	Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. FMCAD Robert B. Jones, Jens U. Skakkebæk, David L. Dill
1998	—	`conf`	Static Analysis to Identify Invariants in RSML Specifications. FTRTFT David Y. W. Park, Jens U. Skakkebæk, David L. Dill
1998	A*	`conf`	Using Magnatic Disk Instead of Main Memory in the Mur CAV Ulrich Stern, David L. Dill
1998	A*	`conf`	Validation with Guided Search of the State Space. DAC C. Han Yang, David L. Dill
1998	A	`conf`	Verification by approximate forward and backward reachability. ICCAD Shankar G. Govindaraju, David L. Dill
1998	J	`jnl`	Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions. Theory Comput. Syst. Seungjoon Park, David L. Dill
1998	A*	`conf`	What's Between Simulation and Formal Verification? (Extended Abstract). DAC David L. Dill
1997	A	`conf`	Approximate algorithms for time separation of events. ICCAD Supratik Chakraborty, David L. Dill
1997	C	`conf`	Automatic Checking of Aggregation Abstractions Through State Enumeration. FORTE Seungjoon Park, Satyaki Das, David L. Dill
1997	—	`conf`	More Accurate Polynomial-Time Min-Max Timing Simulation. ASYNC Supratik Chakraborty, David L. Dill
1997	A*	`conf`	Parallelizing the Mur CAV Ulrich Stern, David L. Dill
1997	—	`conf`	Timing Analysis of Extended Burst-Mode Circuits. ASYNC Supratik Chakraborty, David L. Dill, Kun-Yung Chang, Kenneth Y. Yun
1996	C	`conf`	A New Scheme for Memory-Efficient Probabilistic Verification. FORTE Ulrich Stern, David L. Dill
1996	J	`jnl`	An Invitation to Formal Methods. Computer 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
1996	B	`conf`	Automatic Generation of Invariants in Processor Verification. FMCAD Jeffrey X. Su, David L. Dill, Clark W. Barrett
1996	J	`jnl`	Better Verification Through Symmetry. Formal Methods Syst. Des. C. Norris Ip, David L. Dill
1996	A*	`conf`	Protocol Verification by Aggregation of Distributed Transactions. CAV Seungjoon Park, David L. Dill
1996	B	`conf`	Self-Consistency Checking. FMCAD Robert B. Jones, Carl-Johan H. Seger, David L. Dill
1996	A*	`conf`	State Reduction Using Reversible Rules. DAC C. Norris Ip, David L. Dill
1996	A*	`conf`	The Mur CAV David L. Dill
1996	B	`conf`	Validity Checking for Combinations of Theories with Equality. FMCAD Clark W. Barrett, David L. Dill, Jeremy R. Levitt
1996	B	`conf`	Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. SPAA Seungjoon Park, David L. Dill
1996	A*	`conf`	Verifying Systems with Replicated Components in Mur CAV C. Norris Ip, David L. Dill
1995	C	`conf`	A high-performance asynchronous SCSI controller. ICCD Kenneth Y. Yun, David L. Dill
1995	B	`conf`	An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order). SPAA Seungjoon Park, David L. Dill
1995	A*	`conf`	Architecture Validation for Processors. ISCA Richard C. Ho, C. Han Yang, Mark Horowitz, David L. Dill
1995	—	`conf`	Automatic verification of the SCI cache coherence protocol. CHARME Ulrich Stern, David L. Dill
1995	A	`conf`	Efficient validity checking for processor verification. ICCAD Robert B. Jones, David L. Dill, Jerry R. Burch
1995	J	`jnl`	Exact two-level minimization of hazard-free logic with multiple-input changes. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Steven M. Nowick, David L. Dill
1995	—	`conf`	Improved probabilistic verification by hash compaction. CHARME Ulrich Stern, David L. Dill
1995	A*	`conf`	Verification of Real-Time Systems by Successive Over and Under Approximation. CAV David L. Dill, Howard Wong-Toi
1994	J	`jnl`	A Theory of Timed Automata. Theor. Comput. Sci. Rajeev Alur, David L. Dill
1994	A*	`conf`	Automatic verification of Pipelined Microprocessor Control. CAV Jerry R. Burch, David L. Dill
1994	A*	`ed.`	Computer Aided Verification, 6th International Conference, CAV '94, Stanford, California, USA, June 21-23, 1994, Proceedings CAV David L. Dill
1994	B	`conf`	Hierarchical Models of Synchronous Circuits (Abstract). CONCUR David L. Dill
1994	A*	`conf`	New Techniques for Efficient Verification with Implicitly Conjoined BDDs. DAC Alan J. Hu, Gary York, David L. Dill
1994	A	`conf`	Performance-driven synthesis of asynchronous controllers. ICCAD Kenneth Y. Yun, Bill Lin, David L. Dill, Srinivas Devadas
1994	J	`jnl`	Self-timed logic using Current-Sensing Completion Detection (CSCD). J. VLSI Signal Process. Mark E. Dean, David L. Dill, Mark Horowitz
1994	J	`jnl`	Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill
1993	A*	`conf`	Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs. DAC Polly Siegel, Giovanni De Micheli, David L. Dill
1993	—	`conf`	Better Verification Through Symmetry. CHDL C. Norris Ip, David L. Dill
1993	C	`conf`	Efficient Verification of Symmetric Concurrent Systems. ICCD C. Norris Ip, David L. Dill
1993	A*	`conf`	Efficient Verification with BDDs using Implicitly Conjoined Invariants. CAV Alan J. Hu, David L. Dill
1993	J	`jnl`	Model-Checking in Dense Real-time Inf. Comput. Rajeev Alur, Costas Courcoubetis, David L. Dill
1993	A	`conf`	Modeling hierarchical combinational circuits. ICCAD Jerry R. Burch, David L. Dill, Elizabeth Wolf, Giovanni De Micheli
1993	A*	`conf`	Reducing BDD Size by Exploiting Functional Dependencies. DAC Alan J. Hu, David L. Dill
1993	J	`jnl`	The design of a high-performance cache controller: a case study in asynchronous synthesis. Integr. Steven M. Nowick, Mark E. Dean, David L. Dill, Mark Horowitz
1993	A	`conf`	Unifying synchronous/asynchronous state machine synthesis. ICCAD Kenneth Y. Yun, David L. Dill
1992	C	`conf`	Algorithms for Interface Timing Verification. ICCD Kenneth L. McMillan, David L. Dill
1992	A	`conf`	An implementation of three algorithms for timing verification based on automata emptiness. RTSS Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, Howard Wong-Toi
1992	A	`conf`	Automatic synthesis of 3D asynchronous state machines. ICCAD Kenneth Y. Yun, David L. Dill
1992	A	`conf`	Exact two-level minimization of hazard-free logic with multiple-input changes. ICCAD Steven M. Nowick, David L. Dill
1992	A*	`conf`	Higher-Level Specification and Verification with BDDs. CAV Alan J. Hu, David L. Dill, Andreas J. Drexler, C. Han Yang
1992	B	`conf`	Minimization of Timed Transition Systems. CONCUR Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David L. Dill, Howard Wong-Toi
1992	C	`conf`	Practical Asynchronous Controller Design. ICCD Steven M. Nowick, Kenneth Y. Yun, David L. Dill
1992	C	`conf`	Protocol Verification as a Hardware Design Aid. ICCD David L. Dill, Andreas J. Drexler, Alan J. Hu, C. Han Yang
1992	J	`jnl`	Specification and Automatic Verification of Self-Timed Queues. Formal Methods Syst. Des. David L. Dill, Steven M. Nowick, Robert F. Sproull
1992	J	`jnl`	Symbolic Model Checking: 10^20 States and Beyond Inf. Comput. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1992	C	`conf`	Synthesis of 3D Asynchronous State Machines. ICCD Kenneth Y. Yun, David L. Dill, Steven M. Nowick
1992	A*	`conf`	Verification with Real-Time COSPAN. CAV Costas Courcoubetis, David L. Dill, Magda Chatzaki, Panagiotis Tzounakis
1991	A	`conf`	Automatic Synthesis of Locally-Clocked Asynchronous State Machines. ICCAD Steven M. Nowick, David L. Dill
1991	A*	`conf`	Checking for Language Inclusion Using Simulation Preorders. CAV David L. Dill, Alan J. Hu, Howard Wong-Toi
1991	A*	`conf`	Model-Checking for Probabilistic Real-Time Systems (Extended Abstract). ICALP Rajeev Alur, Costas Courcoubetis, David L. Dill
1991	C	`conf`	Self-Timed Logic Using Current-Sensing Completion Detection (CSCD). ICCD Mark E. Dean, David L. Dill, Mark Horowitz
1991	C	`conf`	Synthesis of Asynchronous State Machines Using A Local Clock. ICCD Steven M. Nowick, David L. Dill
1991	—	`conf`	The Theory of Timed Automata. REX Workshop Rajeev Alur, David L. Dill
1991	—	`conf`	Verifying Automata Specifications of Probabilistic Real-time Systems. REX Workshop Rajeev Alur, Costas Courcoubetis, David L. Dill
1990	A*	`conf`	Automata For Modeling Real-Time Systems. ICALP Rajeev Alur, David L. Dill
1990	C	`conf`	Formal verification of cache systems using refinement relations. ICCD Paul Loewenstein, David L. Dill
1990	A*	`conf`	Model-Checking for Real-Time Systems LICS Rajeev Alur, Costas Courcoubetis, David L. Dill
1990	A*	`conf`	Sequential Circuit Verification Using Symbolic Model Checking. DAC Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill
1990	A*	`conf`	Symbolic Model Checking: 10^20 States and Beyond LICS Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang
1990	A*	`conf`	Synthesizing Processes and Schedulers from Temporal Specifications. CAV Howard Wong-Toi, David L. Dill
1990	—	`conf`	Synthesizing Processes and Schedulers from Temporal Specifications. CAV (DIMACS/AMS volume) Howard Wong-Toi, David L. Dill
1990	—	`conf`	Verification of Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. CAV (DIMACS/AMS volume) Paul Loewenstein, David L. Dill
1990	A*	`conf`	Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. CAV Paul Loewenstein, David L. Dill
1989	C	`conf`	Automatic verification of speed-independent circuits with Petri net specifications. ICCD David L. Dill, Steven M. Nowick, Robert F. Sproull
1989	—	`conf`	Complete Trace Structures. Hardware Specification, Verification and Synthesis David L. Dill
1989	A	`conf`	Practicality of state-machine verification of speed-independent circuits. ICCAD Steven M. Nowick, David L. Dill
1989	—	`conf`	Timing Assumptions and Verification of Finite-State Concurrent Systems. Automatic Verification Methods for Finite State Systems David L. Dill
1989	—	`book`	Trace theory for automatic hierarchical verification of speed-independent circuits. David L. Dill
1986	J	`jnl`	Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Trans. Computers Michael C. Browne, Edmund M. Clarke, David L. Dill, Bud Mishra