Hardware Verification: Publications

Click here to download all publications in a single bibtex file

@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{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{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{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{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{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{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{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",
}