biblio.bib

@article{toplas07,
  author    = {Xavier Rival and Laurent Mauborgne},
  title     = {The trace partitioning abstract domain},
  journal   = {{ACM} TOPLAS},
  volume    = {29},
  number    = {5},
  year      = {2007}
}


@inproceedings{ndsmt,
  author = {Cotton, Scott},
  title = {Natural Domain {SMT}: A Preliminary Assessment},
  booktitle = {FORMATS},
  year = {2010},
  pages = {77--91},
  numpages = {15},
  publisher = {Springer}
} 

@inproceedings{sas13,
  author    = {Martin Brain and Vijay D'Silva and Alberto Griggio and Leopold Haller and Daniel Kroening},
  title     =  {Interpolation-Based Verification of Floating-Point Programs with Abstract {CDCL}},
  booktitle = {SAS},
  pages  =   {412--432},
  year    =   {2013}
}

@inproceedings{sriram,
  author    = {Sriram Sankaranarayanan and Michael Col{\'{o}}n and Henny B. Sipma and Zohar Manna},
  title     = {Efficient Strongly Relational Polyhedral Analysis},
  booktitle = {VMCAI},
  pages   =   {111--125},
  year    =   {2006}
}

@inproceedings{pldi15,
  author    = {Gagandeep Singh and Markus P{\"{u}}schel and Martin T. Vechev},
  title     = {Making numerical program analysis fast},
  booktitle = {PLDI},
  pages     = {303--313},
  year      = {2015}
}



@article{eugoldberg07,
  author    = {Eugene Goldberg and Yakov Novikov},
  title     = {BerkMin: {A} fast and robust {Sat}-solver},
  journal   = {Discrete Applied Mathematics},
  volume    = {155},
  number    = {12},
  pages     = {1549--1561},
  year      = {2007}
}

@Inbook{cp09,
author= {Korovin, Konstantin and Tsiskaridze, Nestan and Voronkov, Andrei},
title= {Conflict Resolution},
bookTitle= {CP},
year= {2009},
publisher= {Springer Berlin Heidelberg},
pages= {509--523},
}

@inproceedings{dpll,
  author = {Mcmillan, Kenneth L. and Kuehlmann, Andreas and Sagiv, Mooly},
  title = {Generalizing {DPLL} to Richer Logics},
  booktitle = {CAV},
  year = {2009},
  pages = {462--476},
  publisher = {Springer}
} 


@inproceedings{SMPP,
  author = {Harris, William R. and Sankaranarayanan, Sriram and Ivan\v{c}i\'{c},
    Franjo and Gupta, Aarti},
  title = {Program Analysis via Satisfiability Modulo Path Programs},
  booktitle = {POPL},
  year = {2010},
  pages = {71--82},
  publisher = {ACM}
} 

@inproceedings{DBLP:conf/esop/MineBR16,
  author    = {Antoine Min{\'{e}} and
               Jason Breck and
               Thomas W. Reps},
  title     = {An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants
               in Numeric Programs},
  booktitle = {ESOP},
  pages     = {560--588},
  year      = {2016},
series    = {LNCS},
  volume    = {9632},
  publisher = {Springer},
}

@inproceedings{DBLP:conf/vmcai/PelleauMTB13,
  author    = {Marie Pelleau and
               Antoine Min{\'{e}} and
               Charlotte Truchet and
               Fr{\'{e}}d{\'{e}}ric Benhamou},
  title     = {A Constraint Solver Based on Abstract Domains},
  booktitle = {VMCAI},
  pages     = {434--454},
  year      = {2013},
  series    = {LNCS},
  volume    = {7737},
  publisher = {Springer},
}

@inproceedings{BJKS15,
  author    = {Martin Brain and 
               Saurabh Joshi and 
               Daniel Kroening and
               Peter Schrammel},
  title     = {{Safety Verification and Refutation by  k-Invariants and k-Induction}},
  booktitle = {SAS},
  pages     = {145-161},
  year      = {2015},
  series    = LNCS,
  volume    = {9291},
  publisher = {Springer},
}

@inproceedings{GS07b,
  author = {Thomas M. Gawlitza and Helmut Seidl},
  title = {Precise Relational Invariants Through Strategy Iteration},
  booktitle = {CSL},
  publisher = {Springer},
  series = {LNCS},
  volume = {4646},
  pages = {23-40},
  year = {2007},
}

@inproceedings{chaff,
  title={Chaff: Engineering an efficient {SAT} solver},
  author={Moskewicz, Matthew W and Madigan, Conor F and Zhao, Ying and Zhang,
    Lintao and Malik, Sharad},
  booktitle={Proceedings of the 38th annual Design Automation Conference},
  pages={530--535},
  year={2001},
  organization={ACM}
}

@inproceedings{apron,
  author    = {Bertrand Jeannet and
               Antoine Min{\'{e}}},
  title     = {Apron: {A} Library of Numerical Abstract Domains for Static Analysis},
  booktitle = {CAV},
  pages     = {661--667},
  year      = {2009}
  }

@inproceedings{uip,
  author    = {Lintao Zhang and Conor F. Madigan and Matthew W. Moskewicz and Sharad Malik},
  title     = {Efficient Conflict Driven Learning in Boolean Satisfiability Solver},
  booktitle = {ICCAD},
  pages =  {279--285},
  year = {2001}
}


@article{se2011,
  author    = {Julien Bertrane and
               Patrick Cousot and
               Radhia Cousot and
               J{\'{e}}r{\^{o}}me Feret and
               Laurent Mauborgne and
               Antoine Min{\'{e}} and
               Xavier Rival},
  title     = {Static analysis by abstract interpretation of embedded critical software},
  journal   = {{ACM} {SIGSOFT} Software Engineering Notes},
  volume    = {36},
  number    = {1},
  pages     = {1--8},
  year      = {2011}
}

@inproceedings{mtk2016,
  author    = {Rajdeep Mukherjee and
               Michael Tautschnig and
               Daniel Kroening},
  title     = {v2c -- {A} Verilog to {C} Translator},
  booktitle = {TACAS},
  pages     = {580--586},
  year      = {2016}
}

@inproceedings{2ls,
  author    = {Peter Schrammel and Daniel Kroening},
  title     = {{2LS} for Program Analysis},
  booktitle = {TACAS},
  pages     = {905--907},
  year      = {2016}
}



@inproceedings{mskm2016,
  author    = {Rajdeep Mukherjee and
               Peter Schrammel and
               Daniel Kroening and
               Tom Melham},
  title     = {Unbounded safety verification for hardware using software analyzers},
  booktitle = {DATE},
  pages     = {1152--1155},
  year      = {2016}
}

@inproceedings{mkm2015,
  author    = {Rajdeep Mukherjee and
               Daniel Kroening and
               Tom Melham},
  title     = {Hardware Verification Using Software Analyzers},
  booktitle = {ISVLSI},
  pages     = {7--12},
  year      = {2015}
}

@inproceedings{tacas12,
  author    = {Vijay D'Silva and
               Leopold Haller and
               Daniel Kroening and
               Michael Tautschnig},
  title     = {Numeric Bounds Analysis with Conflict-Driven Learning},
  booktitle = {TACAS},
  pages     = {48--63},
  year      = {2012},
}

@inproceedings{sas12,
  author    = {Vijay D'Silva and
               
               Daniel Kroening and 
               Leopold Haller},
  title     = {Satisfiability Solvers Are Static Analysers},
  booktitle = {SAS},
  pages     = {317--333},
  year      = {2012}
}

@inproceedings{sas01,
author="Giacobazzi, Roberto
and Quintarelli, Elisa",
title="Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking",
bookTitle="SAS",
year="2001",
pages="356--373"
}

@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 = "DAC",
  pages = "368--371",
}

@book{soc-keating,
  title = "The Simple Art of SoC Design",
  author = "M. Keating",
  year = "2011",
  publisher = "Springer",
  isbn = "978-1-4419-8585-9"
}

@inproceedings{CC77,
  author = {Patrick Cousot and Radhia Cousot},
  title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
  booktitle = {POPL},
  year = {1977},
  pages = {238-252},
}

@inproceedings{DBLP:conf/iccd/YangS01,
  author    = {Jin Yang and
               Carl{-}Johan H. Seger},
  title     = {Introduction to Generalized Symbolic Trajectory Evaluation},
  booktitle = { International Conference on Computer Design (ICCD) },
  pages     = {360--367},
  publisher = { IEEE },
  year      = {2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/osdi/CadarDE08,
  author    = {Cristian Cadar and
               Daniel Dunbar and
               Dawson R. Engler},
  title     = {{KLEE:} Unassisted and Automatic Generation of High-Coverage Tests
               for Complex Systems Programs},
  booktitle = {OSDI},
  publisher = {USENIX},
  pages     = {209--224},
  year      = {2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}



@book{SVA,
	title = "A Practical Introduction to PSL",
	author = "Cindy Eisner and Dana Fisman",
	year = "2006",
	publisher = "Springer",
	isbn =  "978-0-387-36123-9"
}

@book{cdcl,
	title = "Handbook of Satisfiability",
	author = "Biere, A. and Heule, M. and Van Maaren, H. and Walsh, T.",
	year = "2009",
	publisher = "IOS press",
	isbn = "978-1-58603-929-5"
}

@inproceedings{DBLP:conf/lpar/AndrausLS08,
  author    = {Zaher S. Andraus and
               Mark H. Liffiton and
               Karem A. Sakallah},
  title     = {{Reveal}: {A} Formal Verification Tool for {Verilog} Designs},
  booktitle = {LPAR},
  pages     = {343--352},
  year      = {2008},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  series    = {LNCS},
  Volume    = {5330},
  publisher = {Springer},
}

@article{DBLP:journals/corr/abs-cs-0701193,
  author    = {Bruno Blanchet and
               Patrick Cousot and
               Radhia Cousot and
               J{\'{e}}r{\^{o}}me Feret and
               Laurent Mauborgne and
               Antoine Min{\'{e}} and
               David Monniaux and
               Xavier Rival},
  title     = {A Static Analyzer for Large Safety-Critical Software},
  journal   = {CoRR},
  volume    = {abs/cs/0701193},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/pldi/BlanchetCCFMMMR03,
  author    = {Bruno Blanchet and
               Patrick Cousot and
               Radhia Cousot and
               J{\'{e}}r{\^{o}}me Feret and
               Laurent Mauborgne and
               Antoine Min{\'{e}} and
               David Monniaux and
               Xavier Rival},
  title     = {A static analyzer for large safety-critical software},
  pages     = {196--207},
  year      = {2003},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {{ACM}},
  isbn      = {1-58113-662-5},
}

@inproceedings{DBLP:conf/popl/BallR02,
  author    = {Thomas Ball and
               Sriram K. Rajamani},
  title     = {The {SLAM} project: debugging system software via static analysis},
  booktitle = {POPL},
  pages     = {1--3},
  year      = {2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/sttt/BeyerHJM07,
  author    = {Dirk Beyer and
               Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar},
  title     = {The software model checker \textsc{Blast}},
  journal   = {{STTT}},
  volume    = {9},
  number    = {5-6},
  pages     = {505--525},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@misc{slec,
note={\url{http://calypto.com/en/products/slec/}}}

@inproceedings{DBLP:conf/mtv/SunkariCVM07,
  author    = {Sasidhar Sunkari and
               Supratik Chakraborty and
               Vivekananda M. Vedula and
               Kailasnath Maneparambil},
  title     = {A Scalable Symbolic Simulator for {Verilog} {RTL}},
  booktitle = {MTV},
  pages     = {51--59},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/ac/BiereCCSZ03,
  author    = {Armin Biere and
               Alessandro Cimatti and
               Edmund M. Clarke and
               Ofer Strichman and
               Yunshan Zhu},
  title     = {Bounded model checking},
  journal   = {Advances in Computers},
  volume    = {58},
  year      = {2003},
  pages     = {117-148},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{cbmc,
note={\url{http://www.cprover.org/cbmc/}}}

@misc{astree,
note={\url{https://www.absint.com/astree/index.htm}}}

@inproceedings{cbmc.tacas:2004,
  AUTHOR    = { Clarke, Edmund and Kroening, Daniel and Lerda, Flavio},
  TITLE     = { A Tool for Checking {ANSI-C} Programs },
  BOOKTITLE = { TACAS },
  YEAR      = { 2004 },
  PUBLISHER = { Springer },
  series    = { LNCS },
  PAGES     = { 168--176 }
}

@inproceedings{DBLP:conf/iccd/YangS01,
  author    = {Jin Yang and
               Carl{-}Johan H. Seger},
  title     = {Introduction to Generalized Symbolic Trajectory Evaluation},
  booktitle = { International Conference on Computer Design (ICCD) },
  pages     = {360--367},
  publisher = { IEEE },
  year      = {2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/mtv/SunkariCVM07,
  author    = {Sasidhar Sunkari and
               Supratik Chakraborty and
               Vivekananda M. Vedula and
               Kailasnath Maneparambil},
  title     = {A Scalable Symbolic Simulator for {Verilog} {RTL}},
  booktitle = {MTV},
  pages     = {51--59},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/osdi/CadarDE08,
  author    = {Cristian Cadar and
               Daniel Dunbar and
               Dawson R. Engler},
  title     = {{KLEE:} Unassisted and Automatic Generation of High-Coverage Tests
               for Complex Systems Programs},
  booktitle = {OSDI},
  publisher = {USENIX},
  pages     = {209--224},
  year      = {2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@misc{AIG,
note={\url{http://fmv.jku.at/aiger/FORMAT-20070427.pdf}}}

@misc{PSL,
note={\url{http://www.eda.org/vfv/docs/PSL-v1.1.pdf}}}

@misc{ebmc,
note={\url{http://www.cprover.org/ebmc/}}}


@article{DBLP:journals/todaes/LiuV14,
  author    = {Lingyi Liu and
               Shobha Vasudevan},
  title     = {Scaling Input Stimulus Generation through Hybrid Static and Dynamic
               Analysis of {RTL}},
  journal   = {ACM TODAES},
  volume    = {20},
  number    = {1},
  pages     = {4:1--4:33},
  year      = {2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{King:1976:SEP:360248.360252,
 author = {King, James C.},
 title = {Symbolic Execution and Program Testing},
 journal = {Commun. ACM},
 issue_date = {July 1976},
 volume = {19},
 number = {7},
 year = {1976},
 pages = {385--394},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@misc{synopsys,
note={\url{http://www.synopsys.com/Tools/Verification/FunctionalVerification/Pages/HECTOR.aspx}}}

@misc{cadence,
note={\url{http://www.cadence.com/products/fv/Pages/default.aspx}}}

@inproceedings{DBLP:conf/emsoft/Cousot07,
  author    = {Patrick Cousot},
  title     = {Proving the absence of run-time errors in safety-critical avionics
               code},
  booktitle = {EMSOFT},
  pages     = {7--9},
  year      = {2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/vlsid/MukherjeeDPM13,
  author    = {Rajdeep Mukherjee and
               Pallab Dasgupta and
               Ajit Pal and
               Subhankar Mukherjee},
  title     = {Formal Verification of Hardware/Software Power Management Strategies},
  booktitle = {{VLSI}},
  year      = {2013},
  pages     = {326--331},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{co-ver,
 author = {Li, Juncao and Xie, Fei and Ball, Thomas and Levin, Vladimir},
 title = {Efficient Reachability Analysis of {B{\"u}chi} Pushdown Systems for Hardware/Software Co-verification},
 booktitle = {{CAV}},
 year = {2010},
 pages = {339--353},
 publisher = {Springer},
}

@inproceedings{Clarke:2003:HVU:1119772.1119831,
 author = {Clarke, Edmund and Kroening, Daniel},
 title = {Hardware Verification Using {ANSI-C} Programs As a Reference},
 booktitle = {Proceedings of the 2003 Asia and South Pacific Design Automation Conference},
 series = {ASP-DAC},
 year = {2003},
 pages = {308--311},
 publisher = {ACM},
}

@book{decision_procedures,
  author = { Kroening, Daniel and Strichman, Ofer },
  title  = { Decision Procedures },
  publisher = { Springer },
  year = { 2008 },
}

@inproceedings{DBLP:conf/dac/JainKSC05,
  author    = {Himanshu Jain and
               Daniel Kroening and
               Natasha Sharygina and
               Edmund M. Clarke},
  title     = {Word level predicate abstraction and refinement for verifying {RTL}
               {Verilog}},
  booktitle = {DAC},
  pages     = {445--450},
  year      = {2005},
  publisher = {{ACM}},
}

@inproceedings{DBLP:conf/vstte/ClarkeGJV05,
  author    = {Edmund M. Clarke and
               Anubhav Gupta and
               Himanshu Jain and
               Helmut Veith},
  title     = {Model Checking: Back and Forth between Hardware and Software},
  booktitle = {VSTTE},
  series    = {LNCS},
  pages     = {251--255},
  volume    = {4171},
  publisher = {Springer},
  year      = {2008},
}

@misc{opencores,
	note={\url{http://opencores.org/}}}

@misc{minisat,
note={\url{http://minisat.se/}}}

@misc{verilator,
 note={\url{http://www.veripool.org/projects/verilator/wiki/Manual-verilator}}}

@inproceedings{DBLP:conf/rsp/Greaves00,
  author    = {David J. Greaves},
  title     = {A {Verilog} to {C} Compiler},
  booktitle = {RSP},
  pages     = {122--127},
  publisher = {{IEEE} Computer Society},
  year      = {2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/esop/BrainDKS14,
  author    = {Martin Brain and
               Cristina David and
               Daniel Kroening and
               Peter Schrammel},
  title     = {Model and Proof Generation for Heap-Manipulating Programs},
  booktitle = {ESOP},
  pages     = {432--452},
  year      = {2014},
  series    = {LNCS},
  volume    = {8410},
  publisher = {Springer},
}

@inproceedings{DBLP:conf/cav/Bjesse08,
  author    = {Per Bjesse},
  title     = {A Practical Approach to Word Level Model Checking of Industrial Netlists},
  booktitle = { Computer Aided Verification (CAV) },
  pages     = {446--458},
  publisher = {Springer},
  series    = { LNCS },
  volume    = { 5123 },
  year      = {2008}
}

@article{DBLP:journals/fmsd/BrainDGHK14,
  author    = {Martin Brain and
               Vijay D'Silva and
               Alberto Griggio and
               Leopold Haller and
               Daniel Kroening},
  title     = {Deciding floating-point logic with abstract conflict driven clause
               learning},
  journal   = {Formal Methods in System Design},
  volume    = {45},
  number    = {2},
  pages     = {213--245},
  year      = {2014},
}

@inproceedings{dhk2013-popl,
  AUTHOR    = { D'Silva, Vijay
                and Haller, Leopold
                and Kroening, Daniel },
  TITLE     = { Abstract Conflict Driven Learning },
  BOOKTITLE = { Principles of Programming Languages (POPL) },
  YEAR      = { 2013 },
  PUBLISHER = { ACM },
  PAGES     = { 143--154 },
  ISBN      = { 978-1-4503-1832-7 },
}

@inproceedings{KS2005,
  AUTHOR    = { Kroening, Daniel
                and Sharygina, Natasha },
  TITLE     = { Formal Verification of {SystemC} by Automatic Hardware/Software Partitioning },
  BOOKTITLE = { MEMO\-CODE 2005 },
  YEAR      = { 2005 },
  PUBLISHER = { IEEE },
  PAGES     = { 101--110 },
}

@article{cjk2006,
  AUTHOR    = { Clarke, Edmund
                and Jain, Himanshu
                and Kroening, Daniel },
  TITLE     = { Verification of {SpecC} using Predicate Abstraction },
  YEAR      = { 2007 },
  PAGES     = { 5--28 },
  JOURNAL   = { Formal Methods in System Design (FMSD) },
  VOLUME    = { 30 },
  MONTH     = { February },
  NUMBER    = { 1 },
}

@article{bk2010-todaes,
  AUTHOR    = { Blanc, Nicolas
                and Kroening, Daniel },
  TITLE     = { Race Analysis for {SystemC} using {Model} {Checking} },
  YEAR      = { 2010 },
  PUBLISHER = { ACM },
  JOURNAL   = { ACM Transactions on Design Automation of Electronic Systems (TODAES) },
  VOLUME    = { 15 },
  MONTH     = { May },
  NUMBER    = { 3 },
}

@article{DBLP:journals/tcad/CimattiNR13,
  author    = {Alessandro Cimatti and
               Iman Narasamdya and
               Marco Roveri},
  title     = {Software Model Checking {SystemC}},
  journal   = {IEEE TCAD},
  volume    = {32},
  number    = {5},
  pages     = {774--787},
  year      = {2013},
}