main.bib

@inproceedings{wagner2017spin,
  author={Lucas Wagner and others},
  title={{SIMPAL}: A Compositional Reasoning Framework for Imperative Programs},
  booktitle={{SPIN}},
  year=2017,
}

@inproceedings{fifarek2017nfm,
  author = {Aaron W. Fifarek and others},
  title = {{SpeAR} v2.0: Formalized Past {LTL} Specification and Analysis of Requirements},
  booktitle = {{NFM}},
  year = {2017},
}

@inproceedings{QFCS15:backes,
 author={Backes, John and others},
 title={Requirements Analysis of a Quad-Redundant Flight Control System},
 year={2015},
 booktitle={{NFM}}
}

@inproceedings{hilt2013,
  author    = {Anitha Murugesan and others},
  title     = {Compositional Verification of a Medical Device System},
  booktitle = {{HILT}},
  year      = {2013}
}

@misc{jasper_gold,
    title = {{Cadence JasperGold Formal Verification Platform}},
    howpublished = {\url{https://www.cadence.com/}}
}

@misc{Synopsys_VC_formal,
    title = {{Synopsys VC Formal Platform}},
    howpublished = {\url{https://www.synopsys.com}}
}

@misc{hanna2015formal,
  title={Formal verification coverage metrics for circuit design properties},
  author={Hanna, Z.E. and others},
  url={https://www.google.com/patents/US20150135150},
  year={2015},
  publisher={Google Patents}
}


@inproceedings{Beyer:2016,
 author = {Beyer, Dirk and others},
 title = {Correctness Witnesses: Exchanging Verification Results Between Verifiers},
 booktitle = {FSE},
 year = {2016},
 pages = {326--337},
 numpages = {12}
}

@inproceedings{champion2016cav,
  author={Champion, Adrien and others},
  title={The {Kind} 2 Model Checker},
  booktitle={{CAV}},
  year={2016}
}

@ARTICLE{halbwachs1991ieee,
   AUTHOR={N. Halbwachs and others},
   TITLE={The synchronous dataflow programming language {Lustre}},
   JOURNAL={{IEEE}},
   YEAR={1991}
}

@inproceedings{kahsai2011pdmc,
  author    = {Temesghen Kahsai and
               Cesare Tinelli},
  title     = {PKind: {A} parallel k-induction based model checker},
  booktitle = {{PDMC}},
  year      = {2011}
}

@inproceedings{kahsai2011nfm,
  author    = {Temesghen Kahsai and
               Yeting Ge and
               Cesare Tinelli},
  title     = {Instantiation-Based Invariant Discovery},
  booktitle = {{NFM}},
  year      = {2011}
}

@inproceedings{kahsai2012nfm,
 author = {Temesghen Kahsai and others},
 title = {Incremental Verification with Mode Variable Invariants in State Machines},
 booktitle = {NFM},
 year = {2012}
}

@inproceedings{een2011fmcad,
  author    = {Niklas E{\'{e}}n and others},
  title     = {Efficient implementation of property directed reachability},
  booktitle = {{FMCAD}},
  year      = {2011}
}

@inproceedings{cimatti2014tacas,
  author    = {Alessandro Cimatti and others},
  title     = {{IC3} Modulo Theories via Implicit Predicate Abstraction},
  booktitle = {{TACAS}},
  year      = {2014}
}

@inproceedings{Ghass17Cov,
  title={Proof-based Coverage Metrics for Formal Verification},
  author={Ghassabani, Elaheh and others},
  booktitle = {{ASE}},
  year= {2017}
}

@inproceedings{ghassabani2016fse,
  author    = {Elaheh Ghassabani and others},
  title     = {Efficient generation of inductive validity cores for safety properties},
  booktitle = {FSE},
  year      = {2016}
}

@inproceedings{Ghass17AllIVCs,
  title={Efficient Generation of All Minimal Inductive Validity Cores},
  author={Ghassabani, E and others},
  booktitle = {FMCAD},
  year= {2017}
}


@inproceedings{whalen2006issta,
  author = {Whalen, Michael W. and others},
  title = {Coverage Metrics for Requirements-based Testing},
  booktitle = {ISSTA},
  year = {2006}
}

@article{miller2010cacm,
 author = {Miller, Steven P. and others},
 title = {Software model checking takes off},
 journal = {Commun. ACM},
 year = {2010}
}

@manual{DO178C,
  title =        {Software Considerations in Airborne Systems and Equipment
                  Certification},
  author =       {{RTCA DO-178C}},
  publisher =    {RTCA},
  year =         2011
}

@inproceedings{cofer2012nfm,
 author = {Cofer, Darren and others},
 title = {Compositional Verification of Architectural Models},
 booktitle = {NFM},
 year = {2012}
}

@inproceedings{beyer2015boosting,
  title={Boosting k-induction with continuously-refined invariants},
  author={Beyer, Dirk and others},
  booktitle={CAV},
  year={2015}
}

@inproceedings{brain2015safety,
  title={Safety verification and refutation by k-invariants and k-induction},
  author={Brain, Martin and others},
  booktitle={SAS},
  year={2015}
}

@incollection{rocha2017model,
  title={Model checking embedded {C} software using k-induction and invariants},
  author={Rocha, Herbert and others},
  booktitle={SBESC},
  year={2015}
}

@inproceedings{beyer2016smt,
  title={{SMT}-based software model checking: An experimental comparison of four algorithms},
  author={Beyer, Dirk and Dangl, Matthias},
  booktitle={VSTTE},
  year={2016}
}

@misc{Zustre,
    title={Zustre product home page},
    author={T. Kahsai and H. Bourbouh},
    howpublished = {\url{https://github.com/coco-team/zustre}}
}

@InProceedings{GPDR,
author="Hoder, K.
and Bj{\o}rner, N.",
title="Generalized Property Directed Reachability",
booktitle="SAT 2012",
year="2012",
address="Berlin, Heidelberg",
pages="157--171",
}

@inproceedings{groce2005bmc,
  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{ravi2004tacas,
author="Ravi, Kavita
and Somenzi, Fabio",
editor="Jensen, Kurt
and Podelski, Andreas",
title="Minimal Assignments for Bounded Model Checking",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2004",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="31--45"
}