Daniel Kroening : Publications
Click here to download all publications in a single bibtex file
@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{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",
}
@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",
}
@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",
}
@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",
}
@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.",
}
@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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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{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",
}
@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{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{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{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{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",
}