@article{Abate2019,
  title = "Automated formal synthesis of provably safe digital controllers for continuous plants",
  author = "Abate, Alessandro and Bessa, Iury and Cordeiro, Lucas and David, Cristina and Kesseli, Pascal and Kroening, Daniel and Polgreen, Elizabeth",
  year = "2019",
  issn = "1432-0525",
  journal = "Acta Informatica",
  month = "Dec",
  doi = "10.1007/s00236-019-00359-1",
}
@article{DBLP:journals/corr/abs-1712-07388,
  title = "Kayak: Safe Semantic Refactoring to Java Streams",
  author = "Cristina David and Pascal Kesseli and Daniel Kroening",
  year = "2017",
  journal = "CoRR",
  url = "http://arxiv.org/abs/1712.07388",
  volume = "abs/1712.07388",
}
@inproceedings{our-work.POPL:2013,
  title = "Abstract Conflict Driven Learning",
  author = "V. D'Silva and L. Haller and D. Kroening",
  year = "2013",
  booktitle = "Proc.~of the Symposium on Principles of Programming Languages",
  publisher = "ACM",
}
@inproceedings{abstract-syntax.VMCAI:2013,
  title = "Abstraction of Syntax",
  author = "V. D'Silva and D. Kroening",
  year = "2013",
  booktitle = "Proc.~of the conference on Verification, Model Checking and Abstract Interpretation",
  publisher = "Springer-Verlag",
}
@inproceedings{our-work.VMCAI:2013,
  title = "An Abstract Interpretation of {DPLL(T)}",
  author = "M. Brain and V. D'Silva and L. Haller and A. Griggio and D. Kroening",
  year = "2013",
  booktitle = "Proc.~of the conference on Verification, Model Checking and Abstract Interpretation",
}
@inproceedings{dhkt.tacas.2012,
  title = "Numeric Bounds Analysis with Conflict-Driven Learning",
  author = "Vijay D'Silva and Leopold Haller and Daniel Kroening and Michael Tautschnig",
  year = "2012",
  booktitle = "TACAS",
  url = "https://www.cs.ox.ac.uk/people/leopold.haller/papers/tacas2012.pdf",
}
@inproceedings{our-work.SAS:2012,
  title = "Satisfiability Solvers are Static Analysers",
  author = "V. D'Silva and L. Haller and D. Kroening",
  year = "2012",
  booktitle = "Proc.~of Static Analysis Symposium",
  pages = "317-333",
  publisher = "Springer",
}
@inproceedings{kroening_weissenbacher_hvc_09,
  title = "An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions",
  author = "Daniel Kroening and Georg Weissenbacher",
  year = "2010",
  booktitle = "Proceedings of the 5th Haifa Verification Conference",
  editor = "Kedar Namjoshi and Andreas Zeller",
  location = "Haifa, Israel",
  note = "This work was also presented at the  <a href="http://www.iist.unu.edu/index.php/seminars-and-colloquia-2010">UNU IIST seminar in Macau</a> <a href="http://www.georg.weissenbacher.name/slides/macau2010.pdf">(click here for slides)</a> in January 2010.",
  publisher = "Springer",
  series = "LNCS",
}
@inproceedings{dkpwvmcai,
  title = "Interpolant Strength",
  author = "Vijay D'Silva and Daniel Kroening and  Mitra Purandare and Georg Weissenbacher",
  year = "2010",
  booktitle = "Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)",
  month = "January",
  note = "Extended version available as <a href="http://www.inf.ethz.ch/research/disstechreps/techreports/show?serial=652&lang=en">technical report</a>. <a href="http://www.georg.weissenbacher.name/slides/vmcai2010.pdf">Download slides.</a>",
  pages = "129-145",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  url = "http://dx.doi.org/10.1007/978-3-642-11319-2_12",
  volume = "5944",
  doi = "10.1007/978-3-642-11319-2_12",
}
@conference{dsilva_kroening_date09,
  title = "Fixed Points in Multi-Cycle Path Detection",
  author = "Vijay D'Silva and Daniel Kroening",
  year = "2009",
  booktitle = "Proceedings of the Conference on Design Automation and Test in Europe (DATE)",
  editor = "Bashir Al-Hashimi",
  location = "Nice, France",
  month = "April",
  publisher = "IEEE",
}
@article{kroeningweissenbacher_fac09,
  title = "Verification and Falsification of Programs with Loops Using Predicate Abstraction",
  author = "Daniel Kroening and Georg Weissenbacher",
  year = "2009",
  journal = "Formal Aspects of Computing",
  publisher = "Springer",
  url = "http://dx.doi.org/10.1007/s00165-009-0110-2",
  doi = "10.1007/s00165-009-0110-2",
}
@unpublished{dsilva_RRR08,
  title = "Restructuring Resolution Refutations for Interpolation",
  author = "Vijay D'Silva and Daniel Kroening and  Mitra Purandare and Georg Weissenbacher",
  year = "2008",
  month = "October",
  url = "http://www.inf.ethz.ch/personal/vdsilva/publications/dkpw_restructuring_resolution_refutations.pdf",
}
@conference{dsilva_purandare_kroening_VMCAI08,
  title = "Approximation Refinement for Interpolation-Based Model Checking",
  author = "Vijay D'Silva and  Mitra Purandare and Daniel Kroening",
  year = "2008",
  address = "Heidelberg, Germany",
  booktitle = "Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)",
  copyright = "2008",
  editor = "Francesco Logozzo and Doron Peled and Lenore D. Zuck",
  isbn = "978-3-540-78162-2",
  issn = "0302-9743",
  month = "January",
  pages = "68--82",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  url = "http://www.springerlink.com/content/0vx4605k3w51u873/",
  volume = "4905",
  doi = "10.1007/978-3-540-78163-9",
}
@article{zkc2008,
  title = "Computing Binary Combinatorial {Gray} Codes via Exhaustive Search with {SAT}-Solvers",
  author = "Zinovik, Igor and Kroening, Daniel and Chebiryak, Yury",
  year = "2008",
  journal = "IEEE Transactions on Information Theory",
  month = "April",
  note = "To appear.",
}
@article{dkw2008,
  title = "A Survey of Automated Techniques for Formal Software Verification",
  author = "Vijay D'Silva and Daniel Kroening and Georg Weissenbacher",
  year = "2008",
  journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)",
  month = "July",
  number = "7",
  pages = "1165-1178",
  publisher = "IEEE",
  url = "http://dx.doi.org/10.1109/TCAD.2008.923410",
  volume = "27",
  doi = "10.1109/TCAD.2008.923410",
}
@inproceedings{bks2008-scoot,
  title = "Scoot: A Tool for the Analysis of {SystemC} Models",
  author = "Blanc, Nicolas and Kroening, Daniel and Sharygina, Natasha",
  year = "2008",
  booktitle = "Proceedings of TACAS 2008",
  note = "To appear.",
  publisher = "Springer",
}
@inproceedings{spk2008-vmcai,
  title = "Approximation Refinement for Interpolation-Based Model Checking",
  author = "D'Silva, Vijay and Purandare, Mitra and Kroening, Daniel",
  year = "2008",
  booktitle = "Proceedings of VMCAI 2008",
  pages = "68--82",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4905",
}
@article{jksc2007-tcad,
  title = "Word Level Predicate Abstraction and Refinement for Verifying {RTL} {Verilog}",
  author = "Jain, Himanshu and Kroening, Daniel and Sharygina, Natasha and Clarke, Edmund",
  year = "2008",
  journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)",
  month = "February",
  pages = "366--379",
  publisher = "IEEE",
  volume = "27",
}
@book{bkww2008,
  title = "Digitaltechnik",
  author = "Biere, Armin and Kroening, Daniel and Weissenbacher, Georg and Wintersteiger, Christoph",
  year = "2008",
  month = "March",
  publisher = "Springer",
  url = "http://www.digitaltechnik.org",
}
@book{ks2008,
  title = "Decision Procedures -- an Algorithmic Point of View",
  author = "Kroening, Daniel and Strichman, Ofer",
  year = "2008",
  note = "To appear",
  publisher = "Springer",
  series = "EATCS",
}
@inproceedings{ks2007-iccad,
  title = "Formal Verification at Higher Levels of Abstraction",
  author = "Kroening, Daniel and Seshia, Sanjit A.",
  year = "2007",
  booktitle = "Proceedings of ICCAD 2007",
  note = "Tutorial",
  pages = "572--578",
  publisher = "IEEE",
}
@inproceedings{bkw2007-hvc,
  title = "A Complete Bounded Model Checking Algorithm for Pushdown Systems",
  author = "Basler, Gerard and Kroening, Daniel and Weissenbacher, Georg",
  year = "2007",
  booktitle = "Proceedings of HVC 2007",
  isbn = "978-3-540-77964-3",
  pages = "202--217",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4899",
}
@inproceedings{bgk2007,
  title = "Verifying {C++} with {STL} Containers via Predicate Abstraction",
  author = "Blanc, Nicolas and Groce, Alex and Kroening, Daniel",
  year = "2007",
  booktitle = "22nd IEEE International Conference on Automated Software Engineering (ASE)",
  isbn = "978-1-59593-882-4",
  pages = "521--524",
  publisher = "IEEE",
}
@inproceedings{wbwk2007,
  title = "Model Checking Concurrent {Linux} Device Drivers",
  author = "Witkowski, Thomas and Blanc, Nicolas and Weissenbacher, Georg and Kroening, Daniel",
  year = "2007",
  booktitle = "22nd IEEE International Conference on Automated Software Engineering (ASE)",
  isbn = "978-1-59593-882-4",
  pages = "501--504",
  publisher = "IEEE",
  url = "http://doi.acm.org/10.1145/1321631.1321719",
  doi = "10.1145/1321631.1321719",
}
@incollection{ckr2007,
  title = "Static Analysis to Enhance the Power of Model Checking for Concurrent Software",
  author = "Clarke, Edmund and Kroening, Daniel and Reps, Thomas",
  year = "2007",
  booktitle = "Department of Defense Sponsored Information Security Research",
  isbn = "0-471-78756-6",
  month = "July",
  pages = "349--360",
  publisher = "Wiley",
}
@inproceedings{kw2007,
  title = "Lifting Propositional Interpolants to the Word-Level",
  author = "Kroening, Daniel and Weissenbacher, Georg",
  year = "2007",
  booktitle = "Proceedings of FMCAD",
  note = "(also presented in the <a href="http://tresor.epfl.ch/dokuwiki/seminars/2008">TRESOR seminar at EPFL<a>, June 2008)",
  pages = "85--89",
  publisher = "IEEE",
  url = "http://doi.ieeecomputersociety.org/10.1109/FMCAD.2007.31",
}
@article{cks2007-tcs,
  title = "Verification of {Boolean} Programs with Unbounded Thread Creation",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2007",
  journal = "Theoretical Computer Science (TCS)",
  pages = "227--242",
  publisher = "Elsevier",
  volume = "388",
}
@incollection{sh2007-ws,
  title = "Model Checking with Abstraction for Web Services",
  author = "Sharygina, Natasha and Kroening, Daniel",
  year = "2007",
  booktitle = "Test and Analysis of Web Services",
  editor = "Luciano Baresi and Elisabetta DiNitto",
  isbn = "3540729119",
  pages = "121--145",
  publisher = "Springer",
}
@inproceedings{bkw2007-spin,
  title = "{SAT}-based Summarisation for {B}oolean Programs",
  author = "Basler, Gerard and Kroening, Daniel and Weissenbacher, Georg",
  year = "2007",
  booktitle = "Proceedings of SPIN 2007",
  note = "<a href="http://www.georg.weissenbacher.name/slides/spin2007.pdf">Click here for slides.</a>",
  number = "4595",
  pages = "131--148",
  series = "Lecture Notes in Computer Science",
  url = "http://www.springerlink.com/content/x7h7526tu6702917",
}
@inproceedings{zkc2007-ab,
  title = "An Algebraic Algorithm for the Identification of {Glass} Networks with Periodic Orbits along Cyclic Attractors",
  author = "Zinovik, Igor and Kroening, Daniel and Chebiryak, Yury",
  year = "2007",
  booktitle = "Proceedings of Algebraic Biology (AB)",
  pages = "140--154",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4545",
}
@inproceedings{jbskw2007,
  title = "A First Step Towards a Unified Proof Checker for {QBF}",
  author = "Jussila, Toni and Biere, Armin and Sinz, Carsten and Kroening, Daniel and Wintersteiger, Christoph",
  year = "2007",
  booktitle = "Proceedings of SAT 2007",
  isbn = "978-3-540-72787-3",
  pages = "201--214",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4501",
}
@inproceedings{jksc2007,
  title = "{VCEGAR}: Verilog CounterExample Guided Abstraction Refinement",
  author = "Jain, Himanshu and Kroening, Daniel and Sharygina, Natasha and Clarke, Edmund",
  year = "2007",
  booktitle = "Proceedings of TACAS 2007",
  pages = "583--586",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4424",
}
@inproceedings{ks2007-date,
  title = "Image Computation and Predicate Refinement for {RTL} {Verilog} using Word Level Proofs",
  author = "Kroening, Daniel and Sharygina, Natasha",
  year = "2007",
  booktitle = "Proceedings of DATE 2007",
  pages = "1325--1330",
}
@inproceedings{bkossb2007-tacas,
  title = "Deciding Bit-Vector Arithmetic with Abstraction",
  author = "Bryant, Randal E. and Kroening, Daniel and Ouaknine, Joel and Seshia, Sanjit A. and Strichman, Ofer and Brady, Bryan",
  year = "2007",
  booktitle = "Proceedings of TACAS 2007",
  pages = "358--372",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4424",
}
@inproceedings{BEGKR2006,
  title = "{ExpliSAT}: Guiding {SAT}-Based Software Verification with Explicit States",
  author = "Sharon Barner and Cindy Eisner and Ziv Glazberg and Daniel Kroening and Ishai Rabinovitz",
  year = "2007",
  booktitle = "Proceedings of HVC 2006",
  pages = "138--154",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4383",
}
@article{cjk2006,
  title = "Verification of {SpecC} using Predicate Abstraction",
  author = "Clarke, Edmund and Jain, Himanshu and Kroening, Daniel",
  year = "2007",
  journal = "Formal Methods in System Design (FMSD)",
  month = "February",
  number = "1",
  pages = "5--28",
  volume = "30",
}
@inproceedings{cks2006-fmcad,
  title = "Over-Approximating {Boolean} Programs with Unbounded Thread Creation",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2006",
  booktitle = "Proceedings of FMCAD 2006",
  isbn = "0-7695-2707-8",
  pages = "53--59",
  publisher = "IEEE",
}
@inproceedings{cks2006-cogent,
  title = "Accurate Theorem Proving for Program Verification",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2006",
  booktitle = "Proceedings of ISoLA 2004",
  pages = "96--114",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "4313",
}
@inproceedings{kw2006-cav,
  title = "Counterexamples with Loops for Predicate Abstraction",
  author = "Kroening, Daniel and Weissenbacher, Georg",
  year = "2006",
  booktitle = "Proceedings of CAV 2006",
  isbn = "3-540-37406-X",
  pages = "152--165",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  url = "http://dx.doi.org/10.1007/11817963_16",
  volume = "4144",
  doi = "10.1007/11817963_16",
}
@inproceedings{ks2006-tacas,
  title = "Approximating Predicate Images for Bit-Vector Logic",
  author = "Kroening, Daniel and Sharygina, Natasha",
  year = "2006",
  booktitle = "Proceedings of TACAS 2006",
  pages = "242--256",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "3920",
}
@inproceedings{BMC-K2005,
  title = "Computing Over-Approximations with Bounded Model Checking",
  author = "Kroening, Daniel",
  year = "2006",
  booktitle = "Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005)",
  month = "January",
  pages = "79--92",
  publisher = "Elsevier",
  series = "ENTCS",
  volume = "144",
}
@article{gcks05,
  title = "Error Explanation with Distance Metrics",
  author = "Groce, Alex and Chaki, Sagar and Kroening, Daniel and Strichman, Ofer",
  year = "2006",
  journal = "Software Tools for Technology Transfer (STTT)",
  month = "June",
  pages = "229--247",
  publisher = "Springer",
  volume = "8",
}
@article{BJKLP05,
  title = "Putting it all together - Formal Verification of the {VAMP}",
  author = "Beyer, Sven and Jacobi, Christian and Kroening, Daniel and Leinenbach, Dirk and Paul, Wolfgang J.",
  year = "2006",
  journal = "Software Tools for Technology Transfer (STTT), Special Issue on Recent Advances in Hardware Verification",
  month = "August",
  number = "4-5",
  pages = "411--430",
  publisher = "Springer",
  volume = "8",
}
@inproceedings{KS2005,
  title = "Formal Verification of {SystemC} by Automatic Hardware/Software Partitioning",
  author = "Kroening, Daniel and Sharygina, Natasha",
  year = "2005",
  booktitle = "Proceedings of MEMOCODE 2005",
  pages = "101--110",
  publisher = "IEEE",
}
@inproceedings{CKS05,
  title = "Symbolic model checking for asynchronous {Boolean} programs",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2005",
  booktitle = "Proceedings of SPIN 2005",
  editor = "P. Godefroid",
  number = "3639",
  pages = "75--90",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
}
@inproceedings{cks2005,
  title = "Cogent: Accurate theorem proving for program verification",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2005",
  booktitle = "Proceedings of CAV 2005",
  editor = "Etessami, Kousha and Rajamani, Sriram K.",
  isbn = "3-540-27231-3",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "3576",
}
@inproceedings{jksc2005,
  title = "Word Level Predicate Abstraction and Refinement for Verifying {RTL} {Verilog}",
  author = "Jain, Himanshu and Kroening, Daniel and Sharygina, Natasha and Clarke, Edmund",
  year = "2005",
  booktitle = "Proceedings of DAC 2005",
  isbn = "1-59593-058-2",
  pages = "445--450",
}
@inproceedings{cksy2005,
  title = "{SATABS}: {SAT}-based Predicate Abstraction for {ANSI-C}",
  author = "Clarke, Edmund and Kroening, Daniel and Sharygina, Natasha and Yorav, Karen",
  year = "2005",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005)",
  isbn = "3-540-25333-5",
  pages = "570--574",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "3440",
}
@article{ckos2005,
  title = "Computational Challenges in Bounded Model Checking",
  author = "Clarke, Edmund and Kroening, Daniel and Ouaknine, Joel and Strichman, Ofer",
  year = "2005",
  journal = "Software Tools for Technology Transfer (STTT)",
  month = "April",
  number = "2",
  pages = "174--183",
  publisher = "Springer",
  volume = "7",
}
@inproceedings{gk2004-bmc,
  title = "Making the Most of {BMC} Counterexamples",
  author = "Groce, Alex and Kroening, Daniel",
  year = "2005",
  booktitle = "Proceedings of BMC 2004",
  pages = "67--81",
  publisher = "Elsevier",
  series = "ENTCS",
  volume = "119",
}
@article{cksy2004,
  title = "Predicate Abstraction of {ANSI--C} Programs using {SAT}",
  author = "Clarke, Edmund and Kroening, Daniel and Sharygina, Natasha and Yorav, Karen",
  year = "2004",
  journal = "Formal Methods in System Design (FMSD)",
  month = "September--November",
  pages = "105--127",
  volume = "25",
}
@inproceedings{gk2004-icfem,
  title = "Counterexample Guided Abstraction Refinement via Program Execution",
  author = "Groce, Alex and Kroening, Daniel",
  year = "2004",
  booktitle = "Proceedings of ICFEM 2004",
  month = "November",
  number = "3308",
  pages = "224--238",
  publisher = "Springer",
  series = "LNCS",
}
@inproceedings{kc2004,
  title = "Checking Consistency of {C} and {Verilog} using Predicate Abstraction and Induction",
  author = "Kroening, Daniel and Clarke, Edmund",
  year = "2004",
  booktitle = "Proceedings of ICCAD",
  month = "November",
  pages = "66--72",
  publisher = "IEEE",
}
@inproceedings{koss2004-cav,
  title = "Abstraction-based Satisfiability Solving of {Presburger} Arithmetic",
  author = "Kroening, Daniel and Ouaknine, Joel and Seshia, Sanjit and Strichman, Ofer",
  year = "2004",
  booktitle = "Proceedings of CAV 2004",
  editor = "Rajeev Alur and Doron A. Peled",
  isbn = "3-540-22342-8",
  month = "July",
  number = "3114",
  pages = "308--320",
  series = "LNCS",
}
@inproceedings{gkl2004,
  title = "Understanding Counterexamples with explain",
  author = "Groce, Alex and Kroening, Daniel and Lerda, Flavio",
  year = "2004",
  booktitle = "Proceedings of CAV 2004",
  editor = "Rajeev Alur and Doron A. Peled",
  isbn = "3-540-22342-8",
  month = "July",
  number = "3114",
  pages = "453--456",
  series = "LNCS",
}
@inproceedings{cjk2004,
  title = "Verification of {SpecC} and {Verilog} using Predicate Abstraction",
  author = "Jain, Himanshu and Clarke, Edmund and Kroening, Daniel",
  year = "2004",
  booktitle = "Proceedings of MEMOCODE 2004",
  isbn = "0-7803-8509-8",
  pages = "7--16",
  publisher = "IEEE",
}
@inproceedings{cck2004,
  title = "A {SAT}-Based Algorithm for Reparameterization in Symbolic Simulation",
  author = "Chauhan, Pankaj and Clarke, Edmund and Kroening, Daniel",
  year = "2004",
  booktitle = "Proceedings of DAC 2004",
  isbn = "1-58113-828-8",
  pages = "524--529",
  publisher = "ACM Press",
}
@inproceedings{kkm2004,
  title = "Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures",
  author = "Morris, Jennifer and Kroening, Daniel and Koopman, Philip",
  year = "2004",
  booktitle = "Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004)",
  pages = "349--358",
  publisher = "IEEE",
}
@inproceedings{ckl2004,
  title = "A Tool for Checking {ANSI-C} Programs",
  author = "Clarke, Edmund and Kroening, Daniel and Lerda, Flavio",
  year = "2004",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)",
  editor = "Kurt Jensen and Andreas Podelski",
  isbn = "3-540-21299-X",
  pages = "168--176",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "2988",
}
@inproceedings{ckso04,
  title = "Completeness and Complexity of Bounded Model Checking",
  author = "Clarke, Edmund and Kroening, Daniel and Strichman, Ofer and Ouaknine, Joel",
  year = "2004",
  booktitle = "5th International Conference on Verification, Model Checking, and Abstract Interpretation",
  isbn = "3-540-20803-8",
  pages = "85--96",
  series = "Lecture Notes in Computer Science",
  volume = "2937",
}
@inproceedings{ckyclock03,
  title = "Specifying and Verifying Systems with Multiple Clocks",
  author = "Clarke, Edmund and Kroening, Daniel and Yorav, Karen",
  year = "2003",
  booktitle = "Proc.\ of the 2003 International Conference on Computer Design (ICCD)",
  month = "October",
  pages = "48--55",
  publisher = "IEEE",
}
@inproceedings{bjklp03,
  title = "Instantiating uninterpreted functional units and memory system: functional verification of the {VAMP} processor",
  author = "Beyer, Sven and Jacobi, Christian and Kroening, Daniel and Leinenbach, Dirk and Paul, Wolfgang",
  year = "2003",
  booktitle = "Proc.\ of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
  month = "October",
  pages = "51--65",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "2860",
}
@inproceedings{CKY03,
  title = "Behavioral Consistency of {C} and {Verilog} Programs Using Bounded Model Checking",
  author = "Kroening, Daniel and Clarke, Edmund and Yorav, Karen",
  year = "2003",
  booktitle = "Proceedings of DAC 2003",
  isbn = "1-58113-688-9",
  pages = "368--371",
  publisher = "ACM Press",
}
@inproceedings{CK03,
  title = "Hardware Verification using {ANSI-C} Programs as a Reference",
  author = "Clarke, Edmund and Kroening, Daniel",
  year = "2003",
  booktitle = "Proceedings of ASP-DAC 2003",
  isbn = "0-7803-7659-5",
  month = "January",
  pages = "308--311",
  publisher = "IEEE Computer Society Press",
}
@inproceedings{KS03,
  title = "Efficient Computation of Recurrence Diameters",
  author = "Kroening, Daniel and Strichman, Ofer",
  year = "2003",
  booktitle = "4th International Conference on Verification, Model Checking, and Abstract Interpretation",
  editor = "Zuck, L. and Attie, P. and Cortesi, A. and Mukhopadhyay, S.",
  month = "January",
  pages = "298--309",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = "2575",
}
@inproceedings{kp01,
  title = "Automated Pipeline Design",
  author = "Kroening, Daniel and Paul, Wolfgang",
  year = "2001",
  booktitle = "Proc. of 38th {ACM}/{IEEE} Design Automation Conference ({DAC} 2001)",
  pages = "810--815",
  publisher = "ACM Press",
}
@inproceedings{99MPK,
  title = "Proving the Correctness of Processors with Delayed Branch using Delayed {PC}",
  author = "Mueller, Silvia M. and Paul, Wolfgang and Kroening, Daniel",
  year = "2000",
  booktitle = "Numbers, Information and Complexity",
  editor = "Althoefer, I. and Cai, N. and Dueck, G. and Khachatrian, L. and Pinsker, M. and Sarkozy, A. and Wegener, I. and Zhang Z.",
  pages = "579--588",
  publisher = "Kluwer",
}
@inproceedings{KPM00,
  title = "Proving the Correctness of Pipelined Micro-Architectures",
  author = "Kroening, Daniel and Paul, Wolfgang and Mueller, Silvia M.",
  year = "2000",
  booktitle = "Proc. of ITG/GI/GMM-Workshop ''Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen''",
  editor = "Waldschmidt, Klaus and Grimm, Christoph",
  pages = "89--98",
  publisher = "VDE Verlag",
}
@inproceedings{99SLDGK,
  title = "The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs.",
  author = "Mueller, Silvia M. and Leister, Holger and Dell, Peter and Gerteis, Nikolaus and Kroening, Daniel",
  year = "1999",
  booktitle = "In Proc.\ 15th GI/ITG conference 'Architektur von Rechensystemen' ARCS'99",
  pages = "65--73",
}