% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/formal-verification-in-industry

@inproceedings{CuoqKKPSY12,
  title = {Frama-C - A Software Analysis Perspective},
  author = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile Prevosto and Julien Signoles and Boris Yakobowski},
  year = {2012},
  doi = {10.1007/978-3-642-33826-7_16},
  url = {http://dx.doi.org/10.1007/978-3-642-33826-7_16},
  researchr = {https://researchr.org/publication/CuoqKKPSY12},
  cites = {0},
  citedby = {0},
  pages = {233-247},
  booktitle = {Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings},
  editor = {George Eleftherakis and Mike Hinchey and Mike Holcombe},
  volume = {7504},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-33825-0},
}

@article{LuckcuckFDDF19,
  title = {Formal Specification and Verification of Autonomous Robotic Systems: A Survey},
  author = {Matt Luckcuck and Marie Farrell and Louise A. Dennis and Clare Dixon and Michael Fisher},
  year = {2019},
  doi = {10.1145/3342355},
  url = {https://doi.org/10.1145/3342355},
  tags = {Isabelle/HOL, robotics, KeyMaera},
  researchr = {https://researchr.org/publication/LuckcuckFDDF19},
  cites = {0},
  citedby = {0},
  journal = {ACM Computing Surveys},
  volume = {52},
  number = {5},
}

@inproceedings{CalcagnoD11,
  title = {Infer: An Automatic Program Verifier for Memory Safety of C Programs},
  author = {Cristiano Calcagno and Dino Distefano},
  year = {2011},
  doi = {10.1007/978-3-642-20398-5_33},
  url = {http://dx.doi.org/10.1007/978-3-642-20398-5_33},
  tags = {program verification, C++},
  researchr = {https://researchr.org/publication/CalcagnoD11},
  cites = {0},
  citedby = {0},
  pages = {459-465},
  booktitle = {NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings},
  editor = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
  volume = {6617},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-20397-8},
}

@inproceedings{TodorovBT18,
  title = {Formal verification of automotive embedded software},
  author = {Vassil Todorov and Frédéric Boulanger and Safouan Taha},
  year = {2018},
  url = {http://ieeexplore.ieee.org/document/8536209},
  tags = {Automotive, Frama-C, SPARK, B method},
  researchr = {https://researchr.org/publication/TodorovBT18},
  cites = {0},
  citedby = {0},
  pages = {84-87},
  booktitle = {Proceedings of the 6th Conference on Formal Methods in Software Engineering, FormaliSE 2018, collocated with ICSE 2018, Gothenburg, Sweden, June 2, 2018},
  editor = {Stefania Gnesi and Nico Plat and Paola Spoletini and Patrizio Pelliccione},
  publisher = {ACM},
}

@article{DistefanoFLO19,
  title = {Scaling static analyses at Facebook},
  author = {Dino Distefano and Manuel Fähndrich and Francesco Logozzo and Peter W. O'Hearn},
  year = {2019},
  doi = {10.1145/3338112},
  url = {https://doi.org/10.1145/3338112},
  researchr = {https://researchr.org/publication/DistefanoFLO19},
  cites = {0},
  citedby = {0},
  journal = {Communications of the ACM},
  volume = {62},
  number = {8},
  pages = {62-70},
}

@article{BarbosaPFV10,
  title = {A Deductive Verification Platform for Cryptographic Software},
  author = {Manuel Barbosa and Jorge Sousa Pinto and Jean-Christophe Filliåtre and Bárbara Vieira},
  year = {2010},
  url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461},
  tags = {Frama-C, cryptography},
  researchr = {https://researchr.org/publication/BarbosaPFV10},
  cites = {0},
  citedby = {0},
  journal = {ECEASST},
  volume = {33},
}

@article{RushbyH93,
  title = {Formal Verification of Algorithms for Critical Systems},
  author = {John M. Rushby and Friedrich W. von Henke},
  year = {1993},
  url = {http://www.computer.org/tse/ts1993/e0013abs.htm},
  tags = {EHDM, Aerospace},
  researchr = {https://researchr.org/publication/RushbyH93},
  cites = {0},
  citedby = {0},
  journal = {IEEE Trans. Software Eng.},
  volume = {19},
  number = {1},
  pages = {13-23},
}

@inproceedings{SelvarajAF19,
  title = {Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study},
  author = {Yuvaraj Selvaraj and Wolfgang Ahrendt and Martin Fabian},
  year = {2019},
  doi = {10.1007/978-3-030-27008-7_9},
  url = {https://doi.org/10.1007/978-3-030-27008-7_9},
  tags = {Automotive, SPARK},
  researchr = {https://researchr.org/publication/SelvarajAF19},
  cites = {0},
  citedby = {0},
  pages = {143-159},
  booktitle = {Formal Methods for Industrial Critical Systems - 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30-31, 2019, Proceedings},
  editor = {Kim Guldstrand Larsen and Tim A. C. Willemse},
  volume = {11687},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-27008-7},
}

@article{BhadraAWR07,
  title = {A Survey of Hybrid Techniques for Functional Verification},
  author = {Jayanta Bhadra and Magdy S. Abadir and Li-C. Wang and Sandip Ray},
  year = {2007},
  doi = {10.1109/MDT.2007.30},
  url = {http://doi.ieeecomputersociety.org/10.1109/MDT.2007.30},
  tags = {survey, C++},
  researchr = {https://researchr.org/publication/BhadraAWR07},
  cites = {0},
  citedby = {0},
  journal = {IEEE Design & Test of Computers},
  volume = {24},
  number = {2},
  pages = {112-122},
}

@article{OwreRSH95,
  title = {Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS},
  author = {Sam Owre and John M. Rushby and Natarajan Shankar and Friedrich W. von Henke},
  year = {1995},
  url = {http://www.computer.org/tse/ts1995/e0107abs.htm},
  tags = {EHDM, architecture, PVS, Aerospace, design},
  researchr = {https://researchr.org/publication/OwreRSH95},
  cites = {0},
  citedby = {0},
  journal = {IEEE Trans. Software Eng.},
  volume = {21},
  number = {2},
  pages = {107-125},
}

@inproceedings{CreuseDGHH99,
  title = {Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists},
  author = {Léo Creuse and Claire Dross and Christophe Garion and Jérôme Hugues and Joffrey Huguet},
  year = {2019},
  doi = {10.1007/978-3-030-32441-4_2},
  url = {https://doi.org/10.1007/978-3-030-32441-4_2},
  researchr = {https://researchr.org/publication/CreuseDGHH99},
  cites = {0},
  citedby = {0},
  pages = {23-36},
  booktitle = {Formal Methods Teaching - Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings},
  editor = {Brijesh Dongol and Luigia Petre and Graeme Smith},
  volume = {11758},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-32441-4},
}

@article{meng2022adversarial,
  title = {Adversarial robustness of deep neural networks: A survey from a formal verification perspective},
  author = {Meng, Mark Huasong and Bai, Guangdong and Teo, Sin Gee and Hou, Zhe and Xiao, Yan and Lin, Yun and Dong, Jin Song},
  year = {2022},
  tags = {deep learning},
  researchr = {https://researchr.org/publication/meng2022adversarial},
  cites = {0},
  citedby = {0},
  journal = {IEEE Transactions on Dependable and Secure Computing},
}

@inproceedings{NybergGLRW18,
  title = {Formal Verification in Automotive Industry: Enablers and Obstacles},
  author = {Mattias Nyberg and Dilian Gurov and Christian Lidström and Andreas Rasmusson and Jonas Westman},
  year = {2018},
  doi = {10.1007/978-3-030-03427-6_14},
  url = {https://doi.org/10.1007/978-3-030-03427-6_14},
  researchr = {https://researchr.org/publication/NybergGLRW18},
  cites = {0},
  citedby = {0},
  pages = {139-158},
  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV},
  editor = {Tiziana Margaria and Bernhard Steffen},
  volume = {11247},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-03427-6},
}

@inproceedings{GuaspariMP92,
  title = {Formal Verification of Ada Programs},
  author = {David Guaspari and Carla Marceau and Wolfgang Polak},
  year = {1992},
  tags = {Larch, program verification},
  researchr = {https://researchr.org/publication/GuaspariMP92},
  cites = {0},
  citedby = {0},
  pages = {104-141},
  booktitle = {First International Workshop on Larch, Proceedings of the first First International Workshop on Larch, Dedham, Massachusetts, USA, 13-15 July 1992},
  editor = {Ursula Martin and Jeannette M. Wing},
  series = {Workshops in Computing},
  publisher = {Springer},
  isbn = {3-540-19804-0},
}

@inproceedings{MasciZJCT14,
  title = {Formal Verification of Medical Device User Interfaces Using PVS},
  author = {Paolo Masci and Yi Zhang and Paul L. Jones and Paul Curzon and Harold W. Thimbleby},
  year = {2014},
  doi = {10.1007/978-3-642-54804-8_14},
  url = {http://dx.doi.org/10.1007/978-3-642-54804-8_14},
  tags = {PVS},
  researchr = {https://researchr.org/publication/MasciZJCT14},
  cites = {0},
  citedby = {0},
  pages = {200-214},
  booktitle = {Fundamental Approaches to Software Engineering - 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings},
  editor = {Stefania Gnesi and Arend Rensink},
  volume = {8411},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-54803-1},
}

@article{Leroy09,
  title = {Formal verification of a realistic compiler},
  author = {Xavier Leroy},
  year = {2009},
  doi = {10.1145/1538788.1538814},
  url = {http://doi.acm.org/10.1145/1538788.1538814},
  tags = {programming languages, semantics, semantic preservation, proof assistant, CompCert, program verification, formal semantics, type soundness, source-to-source, C++, compiler, programming, context-aware, open-source},
  researchr = {https://researchr.org/publication/Leroy09},
  cites = {0},
  citedby = {0},
  journal = {Communications of the ACM},
  volume = {52},
  number = {7},
  pages = {107-115},
}

@article{PhilippaertsMPS0P14,
  title = {Software verification with VeriFast: Industrial case studies},
  author = {Pieter Philippaerts and Jan Tobias Mühlberg and Willem Penninckx and Jan Smans and Bart Jacobs 0002 and Frank Piessens},
  year = {2014},
  doi = {10.1016/j.scico.2013.01.006},
  url = {http://dx.doi.org/10.1016/j.scico.2013.01.006},
  researchr = {https://researchr.org/publication/PhilippaertsMPS0P14},
  cites = {0},
  citedby = {0},
  journal = {Science of Computer Programming},
  volume = {82},
  pages = {77-97},
}

@inproceedings{MurrayO18,
  title = {BP: Formal Proofs, the Fine Print and Side Effects},
  author = {Toby C. Murray and Paul C. van Oorschot},
  year = {2018},
  doi = {10.1109/SecDev.2018.00009},
  url = {https://doi.org/10.1109/SecDev.2018.00009},
  researchr = {https://researchr.org/publication/MurrayO18},
  cites = {0},
  citedby = {0},
  pages = {1-10},
  booktitle = {2018 IEEE Cybersecurity Development, SecDev 2018, Cambridge, MA, USA, September 30 - October 2, 2018},
  publisher = {IEEE Computer Society},
  isbn = {978-1-5386-7662-2},
}

@article{KleinAEMSKH14,
  title = {Comprehensive formal verification of an OS microkernel},
  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Toby C. Murray and Thomas Sewell and Rafal Kolanski and Gernot Heiser},
  year = {2014},
  doi = {10.1145/2560537},
  url = {http://doi.acm.org/10.1145/2560537},
  tags = {Isabelle/HOL},
  researchr = {https://researchr.org/publication/KleinAEMSKH14},
  cites = {0},
  citedby = {0},
  journal = {ACM Trans. Comput. Syst.},
  volume = {32},
  number = {1},
  pages = {2},
}

@article{wiels:hal-01184099,
  title = {Formal Verification of Critical Aerospace Software},
  author = {Wiels, Virginie and Delmas, Robert and Doose, David and Garoche, Pierre-Lo{\"i}c and Cazin, J. and Durrieu, Guy},
  year = {2012},
  month = {May},
  url = {https://hal.science/hal-01184099},
  tags = {Aerospace, B method},
  researchr = {https://researchr.org/publication/wiels%3Ahal-01184099},
  cites = {0},
  citedby = {0},
  journal = {Aerospace Lab},
  number = {4},
}

@inproceedings{JacobsSPVPP11,
  title = {VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java},
  author = {Bart Jacobs and Jan Smans and Pieter Philippaerts and Frédéric Vogels and Willem Penninckx and Frank Piessens},
  year = {2011},
  doi = {10.1007/978-3-642-20398-5_4},
  url = {http://dx.doi.org/10.1007/978-3-642-20398-5_4},
  tags = {Java, C++},
  researchr = {https://researchr.org/publication/JacobsSPVPP11},
  cites = {0},
  citedby = {0},
  pages = {41-55},
  booktitle = {NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings},
  editor = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
  volume = {6617},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-20397-8},
}

@inproceedings{CassezFQ22,
  title = {Deductive Verification of Smart Contracts with Dafny},
  author = {Franck Cassez and Joanne Fuller and Horacio Mijail Anton Quiles},
  year = {2022},
  doi = {10.1007/978-3-031-15008-1_5},
  url = {https://doi.org/10.1007/978-3-031-15008-1_5},
  tags = {Dafny},
  researchr = {https://researchr.org/publication/CassezFQ22},
  cites = {0},
  citedby = {0},
  pages = {50-66},
  booktitle = {Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, Proceedings},
  editor = {Jan Friso Groote and Marieke Huisman},
  volume = {13487},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-031-15008-1},
}

@inproceedings{GroceHJ07,
  title = {Randomized Differential Testing as a Prelude to Formal Verification},
  author = {Alex Groce and Gerard J. Holzmann and Rajeev Joshi},
  year = {2007},
  doi = {10.1109/ICSE.2007.68},
  url = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2007.68},
  tags = {testing, random testing, Aerospace},
  researchr = {https://researchr.org/publication/GroceHJ07},
  cites = {0},
  citedby = {0},
  pages = {621-631},
  booktitle = {29th International Conference on Software Engineering (ICSE 2007), Minneapolis, MN, USA, May 20-26, 2007},
  publisher = {IEEE Computer Society},
}

@article{EldibWS14-0,
  title = {Formal Verification of Software Countermeasures against Side-Channel Attacks},
  author = {Hassan Eldib and Chao Wang and Patrick Schaumont},
  year = {2014},
  doi = {10.1145/2685616},
  url = {http://doi.acm.org/10.1145/2685616},
  researchr = {https://researchr.org/publication/EldibWS14-0},
  cites = {0},
  citedby = {0},
  journal = {ACM Transactions on Software Engineering Methodology},
  volume = {24},
  number = {2},
  pages = {11},
}

@inproceedings{FirstB22,
  title = {Diversity-Driven Automated Formal Verification},
  author = {Emily First and Yuriy Brun},
  year = {2022},
  doi = {10.1145/3510003.3510138},
  url = {https://doi.org/10.1145/3510003.3510138},
  researchr = {https://researchr.org/publication/FirstB22},
  cites = {0},
  citedby = {0},
  pages = {1-13},
  booktitle = {44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022},
  publisher = {IEEE},
  isbn = {978-1-4503-9221-1},
}

@article{chapman2000industrial,
  title = {Industrial experience with SPARK},
  author = {Chapman, Roderick},
  year = {2000},
  researchr = {https://researchr.org/publication/chapman2000industrial},
  cites = {0},
  citedby = {0},
  journal = {ACM SIGAda Ada Letters},
  volume = {20},
  number = {4},
  pages = {64-68},
}

@inproceedings{AndronickJKKSZZ12,
  title = {Large-scale formal verification in practice: A process perspective},
  author = {June Andronick and D. Ross Jeffery and Gerwin Klein and Rafal Kolanski and Mark Staples and He Zhang and Liming Zhu},
  year = {2012},
  doi = {10.1109/ICSE.2012.6227120},
  url = {http://dx.doi.org/10.1109/ICSE.2012.6227120},
  tags = {microkernel, ACL2},
  researchr = {https://researchr.org/publication/AndronickJKKSZZ12},
  cites = {0},
  citedby = {0},
  pages = {1002-1011},
  booktitle = {34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland},
  editor = {Martin Glinz and Gail C. Murphy and Mauro Pezzè},
  publisher = {IEEE},
  isbn = {978-1-4673-1067-3},
}

@inproceedings{GurovLNW17,
  title = {Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report},
  author = {Dilian Gurov and Christian Lidström and Mattias Nyberg and Jonas Westman},
  year = {2017},
  doi = {10.1007/978-3-319-67113-0_1},
  url = {https://doi.org/10.1007/978-3-319-67113-0_1},
  researchr = {https://researchr.org/publication/GurovLNW17},
  cites = {0},
  citedby = {0},
  pages = {3-18},
  booktitle = {Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017, Proceedings},
  editor = {Laure Petrucci and Cristina Seceleanu and Ana Cavalcanti},
  volume = {10471},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-67113-0},
}

@book{0015096,
  title = {The B-book - assigning programs to meanings},
  author = {Jean-Raymond Abrial},
  year = {2005},
  researchr = {https://researchr.org/publication/0015096},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
  isbn = {978-0-521-02175-3},
}