% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/formal-verification-in-industry/compact @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 = {SEFM}, } @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 Comput. Surv.}, 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 = {NFM}, } @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 = {ICSE}, } @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 = {CACM}, 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 = {TSE}, 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 = {fmics}, } @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 = {dt}, 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 = {TSE}, 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 = {tfm}, } @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 = {ISoLA}, } @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 = {larch}, } @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 = {FASE}, } @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 = {CACM}, 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 = {SCP}, 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 = {secdev}, } @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 = {tocs}, 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 = {NFM}, } @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 = {fmics}, } @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 = {ICSE}, } @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 = {TOSEM}, 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 = {ICSE}, } @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 = {ICSE}, } @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 = {fmics}, } @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}, }