Home
Research
Publications
Hardware and Protocol Verification
Asynchronous Circuits
Software
CVC Lite
CVC
Talks

Selected Papers from Verification Group

[Abs]: Abstract, [Bib]: BibTex entry, [PS]: Postscript

Systems Biology

  • [Abs] [Bib] [PDF] Carolyn Talcott and David L. Dill Multiple Representations of Biological Processes Transactions on Computational Systems Biology, 2006.

  • [Abs] [Bib] [PDF] [PS] David L. Dill, Merrill A. Knapp, Pamela Gage, Carolyn Talcott, Keith Laderoute and Patrick Lincoln The Pathalyzer: a Tool for Analysis of Signal Transduction Pathways The First Annual Recomb Satellite Workshop on Systems Biology, 2005

    Hardware, Software, and Protocol Verification

  • [Abs] [Bib] [PS] [PDF] Vijay Ganesh and David L. Dill. A Decision Procedure for Bit-Vectors and Arrays. In the Proceedings of Computer Aided Verification (CAV), Berlin, Germany, July 7-11, 2007.

  • [Abs] [Bib] [PDF] Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David L. Dill and Dawson Engler. EXE: Automatically Generating Inputs of Death. In the Proceedings of ACM Conference on Computer and Communications Security, Virginia, USA, Oct 30 - Nov 3, 2006.

  • [Abs] [Bib] [PS] [PDF] Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer, David L. Dill and E. Allen Emerson. Multi-threaded Reachability. In DAC'05

  • [Abs] [Bib] [PS] [PDF] Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill and E. Allen Emerson. A Partitioning Methodology for BDD-Based Verification. In Formal Methods in Computer-Aided Design, 5th International Conference, Austin, USA, November 14-17, 2004

  • [Abs] [Bib] [PS] Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill. A Practical Approach to Partial Functions in CVC Lite. In proceedings of PDPAR'04, July 2004.

  • [Abs] [Bib] [PS] Clark Barrett and Sergey Berezin. CVC Lite: A New Implementation of the Cooperating Validity Checker. In Proceedings of CAV'04, July 2004

  • [Abs] [Bib] [PS] Jacob Chang, Sergey Berezin, and David L. Dill. Using Interface Refinement to Integrate Formal Verification into the Design Cycle. In Proceedings of CAV'04, July 2004

  • [Abs] [Bib] [PS] [PDF] Debashis Sahoo, Subramanian K. Iyer, Jawahar Jain, Christian Stangier, Amit Narayan, David L. Dill and E. Allen Emerson. A Partitioning Methodology for BDD-Based Verification. In Proceedings of the 13th IEEE/ACM International Workshop on Logic & Synthesis, pp. 192-199, Temecula, USA, June 2-4, 2004.

  • [Abs] [Bib] [PS][PDF] Satyaki Das. "Predicate Abstraction", Ph.D. Thesis., Department of Electrical Engineering, Stanford University, Dec 2003.

  • [Abs] [Bib] [PS][PDF] Madanlal Musuvathi. "CMC: A Model Checker for Network Protocol Implementations", Ph.D. Thesis, Department of Computer Science, Stanford University, Dec 2003.

  • [Abs] [Bib] [PS] Clark Barrett and Sergey Berezin. "A Proof-Producing Boolean Search Engine." In Proceedings of PDPAR 2003 Workshop, Miami, Florida, USA, July, 2003.

  • [Abs] [Bib] [PS] Husam Abu-Haimed, Sergey Berezin, and David L. Dill. "Strengthening Invariants by Symbolic Consistency Testing." To appear in Proceedings of CAV'03, July 2003.

  • [Abs] [Bib] [PS] Sergey Berezin, Vijay Ganesh, and David L. Dill. "Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic." In Proceedings of TACAS 2003, Warsaw, Poland, April, 2003.

  • [Abs] [Bib] [PS] [PDF] Madanlal Musuvathi, David Park, Andy Chou, Dawson Engler, David L Dill. "CMC: A Pragmatic Approach to Model Checking Real Code", In Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (OSDI), Boston, Massachusetts, USA, December, 2002.

  • [Abs] [Bib] [PS] Vijay Ganesh, Sergey Berezin, and David L. Dill. "Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods", In Proceedings of FMCAD 2002, Portland, Oregon, USA, November, 2002.

  • [Abs] [Bib] [PS] [PPT] Satyaki Das and David L. Dill. "Counter-Example Based Predicate Discovery in Predicate Abstraction", In Proceedings of FMCAD 2002, Portland, Oregon, USA, November, 2002.

  • [Abs] [Bib] [PS][PDF] Kanna Shimizu. "Writing, Verifying, and Exploiting Formal Specifications for Hardware Designs", Ph.D. Thesis, Department of Electrical Engineering, Stanford University, August 2002.

  • [Abs] [Bib] [PS] [PDF] Aaron Stump, Clark W. Barrett, and David L. Dill. "CVC: a Cooperating Validity Checker," In Proceedings of CAV 2002, Copenhagen, Denmark, July 2002.

    [Abs] [Bib] [PS] Clark W. Barrett, David L. Dill, and Aaron Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In Ed Brinksma and Kim Guldstrand Larsen, editors, 14th International Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 236-249. Springer-Verlag, 2002. Copenhagen, Denmark.

  • [Abs] [Bib] [PS] [PDF] Aaron Stump and David L. Dill. "Faster Proof Checking in the Edinburgh Logical Framework," In Proceedings of CADE 2002, Copenhagen, Denmark, July 2002.

  • [Abs] [Bib] [PS] [PDF] [PPT] Kanna Shimizu and David L. Dill. "Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification", In Proceedings of DAC 2002, New Orleans, LA, June 2002.

  • [Abs] [Bib] [PS] [PDF] [PPT] Kanna Shimizu, David L. Dill, and Ching-Tsun Chou. "A Specification Methodology by a Collection of Compact Properties as Applied to the Intel(C) Itanium(TM) Processor Bus Protocol," In Proceedings of CHARME 2001, Livingston, Scotland, September 2001.

  • [Abs] [Bib] [PS] Satyaki Das and David L. Dill "Successive Approximation of Abstract Transition Relations," In Proc. of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, June 2001.

  • [Abs] [Bib] [PS] [PDF] Aaron Stump, Clark W. Barrett, David L. Dill, and Jeremy Levitt "A Decision Procedure for an Extensional Theory of Arrays," In Proc. of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, June 2001.

  • [Abs] [Bib] [PS] [PDF] [PPT] Kanna Shimizu, David L. Dill, and Alan J. Hu. "Monitor-Based Formal Specification of PCI," In Proc. of the Third International Conference on Formal Methods in Computer-Aided Design, Austin, Texas, November 2000.

  • [Abs] [Bib] [PS] Chris Wilson, David L. Dill, and Randal E. Bryant. "Symbolic Simulation with Approximate Values," In Proc. of the Third International Conference on Formal Methods in Computer-Aided Design, Austin, Texas, November 2000.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju, and David L. Dill. "Counterexample-guided Choice of Projections in Approximate Symbolic Model Checking," Proceedings of ICCAD-2000, November 2000.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju. "Approximate Symbolic Model Checking Using Overlapping Projections," Ph.D. Thesis, Department of Electrical Engineering, Stanford University, August 2000.

  • [Abs] [Bib] [PS] Chris Wilson and David L. Dill. "Reliable Verification using Symbolic Simulation with Scalar Values," 37th Design Automation Conference, June 2000.

  • [Abs] [Bib] [PS] David Y.W. Park, Ulrich Stern, Jens U. Skakkebæk, and David L. Dill. "Java Model Checking," In Proc. of the First International Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland, June 2000.

  • [Abs] [Bib] [PS] [PPT] Clark W. Barrett, David L. Dill and Aaron Stump. "A Framework for Cooperating Decision Procedures," CADE'00, LNCS, June 2000.

  • [Abs] [Bib] [PS] Satyaki Das, David L. Dill, and Seungjoon Park. "Experience with Predicate Abstraction," 11th International Conference on Computer Aided Verification, July 1999.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju, and David L. Dill. "Aproximate Symbolic Model Checking Using Overlapping Projections," First International Workshop on Symbolic Model Checking (SMC99) at Federated Logic Conference (FLOC), July 1999.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju, David L. Dill and Jules P. Bergmann. "Improved Approximate Reachability using Auxiliary State Variables," Proceedings of DAC99, June 1999.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju, David L. Dill. "Verification by Approximate Forward and Backward Reachability," Proceedings of ICCAD98, November 1998.

  • [Abs] [Bib] [PS] Jeffrey X. Su, David L. Dill, and Jens U. Skakkebæk, "Formally Verifying Data and Control with Weak Reachability Invariants", FMCAD98, 1998.

  • [Abs] [Bib] [PS] Robert B. Jones, Jens U. Skakkebæk, and David L. Dill. "Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution", to appear in FMCAD '98.

  • [Abs] [Bib] [PS] David Y.W. Park, Jens U. Skakkebæk, and David L. Dill. "Static Analysis to Identify Invariants in RSML Specifications", to appear in Formal Techniques in Real-Time and Fault Tolerant Systems, Lyngby, Denmark, September 1998.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "Verifying Systems with Replicated Components in Murphi," to appear in Formal Methods in System Design.

  • [Abs] [Bib] [PS] Jens U. Skakkebæk, Robert B. Jones, and David L. Dill. "Formal Verification of Out-of-Order Execution Using Incremental Flushing," 10th International Conference on Computer Aided Verification, June 1998.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "Using Magnetic Disk instead of Main Memory in the Murphi Verifier," 10th International Conference on Computer Aided Verification, June 1998.

  • [Abs] [Bib] [PS] Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. "A Decision Procedure for Bit-Vector Arithmetic," 35th Design Automation Conference, June 1998.

  • [Abs] [Bib] [PS] Shankar G. Govindaraju, David L. Dill, Alan J. Hu, and Mark A. Horowitz. "Approximate Reachability with BDDs using Overlapping Projections," 35th Design Automation Conference, June 1998.

  • [Abs] [Bib] [PS] C. Han Yang and David L. Dill. "Validation with Guided Search of the State Space," 35th Design Automation Conference, June 1998.

  • [Abs] [Bib] [PS] David Y.W. Park, Jens U. Skakkebæk, Mats P.E. Heimdahl, Barbara J. Czerny, and David L. Dill. "Checking Properties of Safety Critical Specifications Using Efficient Decision Procedures," FMSP'98: Second Workshop on Formal Methods in Software Practice, March 1998.

  • [Abs] [Bib] [PS] John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern. "Finite-State Analysis of SSL 3.0," 7th USENIX Security Symposium, January 1998.

  • [Abs] [Bib] [PS] Seungjoon Park and David L. Dill. "Verification of Cache Coherence Protocols By Aggregation of Distributed Transactions." Theory of Computing Systems, vol 31(4), pp. 355-376, 1998.

  • [Abs] [Bib] [PS] Seungjoon Park, Satyaki Das, and David L. Dill. "Automatic Checking of Aggregation Abstractions Through State Enumeration," IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV), pp. 207-222, November 1997.

  • [Abs] [Bib] Seungjoon Park. "Practical Verification of Cache Coherence Algorithms With an Automatic Theorem-Prover," 2nd International Workshop on Verification of Infinite State Systems: Infinity, July 1997.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "Parallelizing the Murphi Verifier," 9th International Conference on Computer Aided Verification, June 1997.

  • [Abs] [Bib] [PS] John C. Mitchell, Mark Mitchell, and Ulrich Stern. "Automated analysis of cryptographic protocols using Murphi," IEEE Symposium on Security and Privacy, May 1997.

  • [Abs] [Bib] [PS] C. Norris Ip. "State Reduction Methods for Automatic Formal Verification," Ph.D. Thesis, Department of Computer Science, Stanford University, December 1996.

  • [Abs] [Bib] [PS] Jeremy Levitt, Ph.D. Thesis, Department of Computer Science, Stanford University, 1996.

  • [Abs] [Bib] [PS] Clark W. Barrett, David L. Dill, Jeremy R. Levitt. "Validity Checking for Combinations of Theories with Equality," FMCAD'96, November 1996.

  • [Abs] [Bib] [PS] Robert B. Jones, Carl-Johan Seger, and David L. Dill. "Self-consistency checking," FMCAD'96, November 1996.

  • [Abs] [Bib] [PS] Jeffrey X. Su, David L. Dill and Clark Barrett. "Automatic Generation of Invariants in Processor Verification," FMCAD'96, November 1996.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "Better Verification Through Symmetry," Formal Methods in System Design, vol. 9(1/2), August 1996.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "A New Scheme for Memory-Efficient Probabilistic Verification," FORTE/PSTV'96, October 1996.

  • [Abs] [Bib] [PS] David L. Dill. "The Murphi verification system," International Conference on Computer-Aided Verification, LNCS 1102, July 1996.

  • [Abs] [Bib] [PS] Seungjoon Park and David L. Dill. "Protocol Verification by Aggregation of Distributed Transactions," International Conference on Computer-Aided Verification, pp. 300-310, LNCS 1102, July 1996.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "Verifying Systems with Replicated Components in Murphi," International Conference on Computer-Aided Verification, July 1996.

  • [Abs] [Bib] [PS] Seungjoon Park and David L. Dill. "Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions," 8th ACM Symposium on Parallel Algorithms and Architectures (SPAA), pp. 288-296, June 1996.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "State Reduction Using Reversible Rules," 33rd Design Automation Conference, Las Vegas, June 1996.

  • [Abs] [Bib] [PS] Seungjoon Park. "Computer Assisted Analysis of Multiprocessor Memory Systems," Ph.D. Thesis, Computer Systems Laboratory Technical Report CSL-TR-96-696, Stanford University, June 1996.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "Combining State Space Caching and Hash Compaction," Methoden des Entwurfs und der Verifikation digitaler Systeme:4. GI/ITG/GME Workshop Proceedings, Kreischa, March 1996.

  • [Abs] [Bib] [PS] Alan John Hu. "Efficient Techniques for Formal Verification Using Binary Decision Diagrams," Ph.D. Thesis, Stanford University, December 1995.

  • [Abs] [Bib] [PS] Robert B. Jones, David L. Dill, and Jerry R. Burch. "Efficient Validity Checking for Processor Verification," International Conference on Computer-Aided Design, November 1995.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "Improved probabilistic verification by hash compaction," Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, October 1995.

  • [Abs] [Bib] [PS] Elizabeth Susan Wolf. "Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution," Ph.D. Thesis, Stanford University, September 1995.

  • [Abs] [Bib] [PS] Seungjoon Park and David L. Dill. "An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)," 7th ACM Symposium on Parallel Algorithms and Architectures, pp. 34-41, July 1995.

  • [Abs] [Bib] [PS] Howard Wong-Toi and David L. Dill. "Verification of real-time systems by successive over and under approximation" International Conference on Computer-Aided Verification, July 1995.

  • [Abs] [Bib] [PS] Richard C. Ho, C. Han Yang, Mark Horowitz, and David L. Dill. "Architecture Validation for Processors," 22nd Annual International Symposium on Computer Architecture, June 1995.

  • [Abs] [Bib] [PS] Ulrich Stern and David L. Dill. "Automatic verification of the SCI cache coherence protocol," Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.

  • [Abs] [Bib] [PS] Jerry R. Burch and David L. Dill. "Automatic Verification of Pipelined Microprocessor Control," International Conference on Computer-Aided Verification, LNCS 818, Springer-Verlag, June 1994.

  • [Abs] [Bib] [PS] Alan J. Hu, Gary York, and David L. Dill. "New Techniques for Efficient Verification with Implicitly Conjoined BDDs," 31st Design Automation Conference, June 1994.

  • [Abs] [Bib] [PS] Jerry R. Burch, David L. Dill, Elizabeth Wolf, and Giovanni De Micheli. "Modeling Hierarchical Combinational Circuits," International Conference on Computer-Aided Design, November 1993.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "Efficient Verification of Symmetric Concurrent Systems," IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 230-234, IEEE Computer Society, October 1993.

  • [Abs] [Bib] [PS] Alan J. Hu and David L. Dill. "Efficient Verification with BDDs Using Implicitly Conjoined Invariants," International Conference on Computer-Aided Verification, pp. 3-14, LNCS 697, Springer-Verlag, June 1993.

  • [Abs] [Bib] [PS] Alan J. Hu and David L. Dill. "Reducing BDD Size by Exploiting Functional Dependencies," 30th Design Automation Conference, pp. 266-271, June 1993.

  • [Abs] [Bib] [PS] C. Norris Ip and David L. Dill. "Better Verification through Symmetry," International Conference on Computer Hardware Description Languages, pp. 87-100, April 1993.

  • [Abs] [Bib] [PS] David L. Dill and Seungjoon Park and Andreas G. Nowatzyk. "Formal Specification of Abstract Memory Models," Research on Integrated Systems: Proceedings of the 1993 Symposium, Gaetano Borriello and Carl Ebeling, Eds. pp. 38-52, MIT Press, March 1993.

  • [Abs] [Bib] [PS] David L. Dill and Andreas J. Drexler and Alan J. Hu and C. Han Yang. "Protocol Verification as a Hardware Design Aid," IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522-525, October 1992.

  • [Abs] [Bib] [PS] Alan J. Hu and David L. Dill and Andreas J. Drexler and C. Han Yang. "Higher-Level Specification and Verification With BDDs," Fourth Workshop on Computer-Aided Verification, Montreal, June 1992.

    Asynchronous Circuits

  • [Abs] [Bib] [PS] Supratik Chakraborty, Kenneth Y. Yun and David L. Dill, "Practical Timing Analysis of Asynchronous Systems using Time Separation of Events", 1998 IEEE Custom Integrated Circuits Conference, pp. 455-458, May 1998.

  • [Abs] [Bib] [PS] Supratik Chakraborty, Kenneth Y. Yun and David L. Dill, "Practical Timing Analysis of Asynchronous Systems using Time Separation of Events", Proceedings of the Fifth ACM/IEEE International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU), pp. 209-217, December 1997.

  • [Abs] [Bib] [PS] Supratik Chakraborty and David L. Dill, "Approximate Algorithms for Time Separation of Events", Proceedings of ICCAD97, pp. 190-194, November 1997.

  • [Abs] [Bib] [PS] Supratik Chakraborty and David L. Dill, "More Accurate Polynomial-Time Min-Max Timing Simulation," Proceedings of the Third International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 112-123, April 1997.

  • [Abs] [Bib] [PS] Supratik Chakraborty, David L. Dill, Kenneth Y. Yun and Kun-Yung Chang, "Timing Analysis for Extended Burst-Mode Circuits," Proccedings of the Third International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 101-111, April 1997.

  • [PS] Kenneth Y. Yun and David L. Dill, "A High-Performance Asynchronous SCSI Controller," International Conference on Computer Design: VLSI and Computers and Processors, October 1995.

  • [PS] Kenneth Y. Yun and David L. Dill, "Unifying Synchronous/Asynchronous State Machine Synthesis", ICCAD93, November, 1993.

  • [PS] Steven M. Nowick and Mark E. Dean and David L. Dill and Mark Horowitz, "The Design of a High-Performance Cache Controller: a Case Study in Asynchronous Synthesis", Hawaii International Conference on Systems Science, 1993.

  • [PS] Kenneth Y. Yun, David L. Dill and Steven M. Nowick, "Practical generalizations of asynchronous state machines", EDAC93, February, 1993.

  • [PS] Steven M. Nowick and David L. Dill, "Exact Two-Level Minimization of Hazard-Free Logic with Multiple-Input Changes", ICCAD92, November, 1992.

  • [PS] Kenneth Y. Yun and David L. Dill. "Automatic synthesis of 3D asynchronous state machines", ICCAD92, November, 1992.

  • [PS] Steven M. Nowick, Kenneth Y. Yun and David L. Dill, "Practical asynchronous controller design", ICCD92, October, 1992.

  • [PS] Kenneth Y. Yun, David L. Dill and Steven M. Nowick, "Synthesis of 3D asynchronous state machines", ICCD92, October, 1992.