% our_group.bib
% Aaron Stump, 3/17/99
%
% This file contains references to publications of our group.

@InProceedings{PSD98,
  author =       {D. Park and J. Skakkeb{\ae}k and D. Dill},
  title =        {Static Analysis to Identify Invariants in {RSML} Specifications},
  booktitle =    {Formal Techniques in Real-Time and Fault Tolerant Systems},
  year =         1998
}

@inproceedings{SDS98,
author = "J. Su and D. Dill and J. Skakkeb{\ae}k",
title = "Formally Verifying Data and Control with Weak Reachability Invariants",
booktitle= "Formal Methods In Computer-Aided Design",
year=1998}

@inproceedings{SJD98,
author = "J. Skakkeb{\ae}k and R. Jones and D. Dill",
title = "Formal Verification of Out-of-Order Execution Using Incremental Flushing",
booktitle= "10th International Conference on Computer-Aided Verification",
year=1998}

@inproceedings{BDL96,
author="C. Barrett and D. Dill and J. Levitt",
title="Validity Checking for Combinations of Theories with Equality",
booktitle="Formal Methods In Computer-Aided Design",
Editor="M. Srivas and A. Camilleri",
Publisher="Springer-Verlag",
Year=1996,
pages="187-201"}

@inproceedings{BDS00,
author= "C. Barrett and D. Dill and A. Stump",
title={{A Framework for Cooperating Decision Procedures}},
booktitle="17th International Conference on Automated Deduction",
Editor="D. McAllester",
Publisher="Springer-Verlag",
pages="79-97",
year =         2000
}

@article{SDGB00,
author= "A. Stump and D. Dill and J. Giesl and C. Barrett",
title={{On a Very Simple Abstract Higher-Order Congruence Closure Algorithm}},
journal="In preparation",
note="Available from http://verify.stanford.edu/\~\,stump/",
year="2000"}

@inproceedings{SBDL01,
author= "A. Stump and C. Barrett and D. Dill and J. Levitt",
title={{A Decision Procedure for an Extensional Theory of Arrays}},
booktitle="16th IEEE Symposium on Logic in Computer Science",
Publisher="IEEE Computer Society",
pages="29-37",
year = 2001
}

@article{SBDF02,
author= "A. Stump and C. Barrett and D. Dill and C. Flanagan",
title={{Proof production in decision procedures}},
journal="In revision",
year=2002}

@inproceedings{BDS02,
author= "C. Barrett and D. Dill and A. Stump",
title={{Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT}},
booktitle="14th International Conference on Computer-Aided Verification",
editors="K. Larsen and E. Brinksma",
pages="236--249",
publisher="Springer",
year="2002"}

@inproceedings{SBD02,
author= "A. Stump and C. Barrett and D. Dill",
title={{CVC: a Cooperating Validity Checker}},
booktitle="14th International Conference on Computer-Aided Verification",
editors="K. Larsen and E. Brinksma",
pages={500--504},
year="2002"}

@inproceedings{SD02a,
author= "A. Stump and D. Dill",
title={{Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF}},
booktitle="3rd International Workshop on Logical Frameworks and Meta-Languages",
editors="F. Pfenning",
year="2002"}

@inproceedings{SD02,
author= "A. Stump and D. Dill",
title={{Faster Proof Checking in the Edinburgh Logical Framework}},
booktitle="18th International Conference on Automated Deduction",
pages={392--407},
editors="A. Voronkov",
year="2002"}

@inproceedings{BDS02a,
author= "C. Barrett and D. Dill and A. Stump",
title = {{A Generalization of Shostak's Method for Combining Decision Procedures}},
booktitle="4th International Workshop on Frontiers of Combining Systems (FroCos)",
year= "2002"}

@phdthesis{B02,
author = "C. Barrett",
title = {{Checking Validity of Quantifier-free Formulas in Combinations of First-Order Theories}},
year="2002",
note="In preparation",
school={Stanford University}}

@phdthesis{S02,
author = "A. Stump",
title = {{Checking Validities and Proofs with CVC and flea}},
year="2002",
note="available from http://www.cs.wustl.edu/\~\,stump/",
school={Stanford University}}

@InProceedings{AMSV02,
  author =       {A. Appel and N. Michael and A. Stump and R. Virga},
  title =        {A Trustworthy Proof Checker},
  booktitle =    {Joint session of the FLoC '02 VERIFY and FCS workshops},
  year =         2002
}

@InProceedings{mpc02,
  author = "M. Musuvathi and D. Park and A. Chou and D. Engler and D. Dill",
   year = "2002",
   month = dec,
   title = "{CMC: A Pragmatic Approach to Model Checking Real Code}",
   booktitle = "5th Symposium on Operating Systems Design and Implementation"
}

@inproceedings{DD2002,
author = "Satyaki Das and David L. Dill",
title = "Counter-Example Based Predicate Discovery in Predicate Abstraction",
booktitle = "Formal Methods in Computer-Aided Design",
year = "2002",
month = "November",
publisher = "Springer-Verlag",
location = "Portland, Oregon"
}

@inproceedings{BD94,
author="Jerry R. Burch and David L. Dill",
title="Automatic Verification of Pipelined Microprocessor Control",
booktitle="Conference on Computer-Aided Verification",
editor="David L. Dill",
Series="Lecture Notes in Computer Science",
Volume="818",
Publisher="Springer-Verlag",
year="1994",
Pages="68--80"}