publications:
- title: "Frama-C - A Software Analysis Perspective"
  author:
  - name: "Pascal Cuoq"
    link: "https://researchr.org/alias/pascal-cuoq"
  - name: "Florent Kirchner"
    link: "https://researchr.org/alias/florent-kirchner"
  - name: "Nikolai Kosmatov"
    link: "https://researchr.org/alias/nikolai-kosmatov"
  - name: "Virgile Prevosto"
    link: "https://researchr.org/alias/virgile-prevosto"
  - name: "Julien Signoles"
    link: "https://researchr.org/alias/julien-signoles"
  - name: "Boris Yakobowski"
    link: "https://researchr.org/alias/boris-yakobowski"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/978-3-642-33826-7_16"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-33826-7_16"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sefm/CuoqKKPSY12"
  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:
  - name: "George Eleftherakis"
    link: "https://researchr.org/alias/george-eleftherakis"
  - name: "Mike Hinchey"
    link: "https://researchr.org/alias/mike-hinchey"
  - name: "Mike Holcombe"
    link: "https://researchr.org/alias/mike-holcombe"
  volume: "7504"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-33825-0"
  kind: "inproceedings"
  key: "CuoqKKPSY12"
- title: "Formal Specification and Verification of Autonomous Robotic Systems: A Survey"
  author:
  - name: "Matt Luckcuck"
    link: "https://researchr.org/alias/matt-luckcuck"
  - name: "Marie Farrell"
    link: "https://researchr.org/alias/marie-farrell"
  - name: "Louise A. Dennis"
    link: "https://researchr.org/alias/louise-a.-dennis"
  - name: "Clare Dixon"
    link: "https://researchr.org/alias/clare-dixon"
  - name: "Michael Fisher"
    link: "https://researchr.org/alias/michael-fisher"
  year: "2019"
  doi: "https://doi.org/10.1145/3342355"
  links:
    doi: "https://doi.org/10.1145/3342355"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/csur/LuckcuckFDDF19"
  tags:
  - "Isabelle/HOL"
  - "robotics"
  - "KeyMaera"
  researchr: "https://researchr.org/publication/LuckcuckFDDF19"
  cites: 0
  citedby: 0
  journal: "ACM Computing Surveys"
  volume: "52"
  number: "5"
  kind: "article"
  key: "LuckcuckFDDF19"
- title: "Infer: An Automatic Program Verifier for Memory Safety of C Programs"
  author:
  - name: "Cristiano Calcagno"
    link: "https://researchr.org/alias/cristiano-calcagno"
  - name: "Dino Distefano"
    link: "https://researchr.org/alias/dino-distefano"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_33"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_33"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/CalcagnoD11"
  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:
  - name: "Mihaela Gheorghiu Bobaru"
    link: "https://researchr.org/alias/mihaela-gheorghiu-bobaru"
  - name: "Klaus Havelund"
    link: "https://researchr.org/alias/klaus-havelund"
  - name: "Gerard J. Holzmann"
    link: "https://researchr.org/alias/gerard-j.-holzmann"
  - name: "Rajeev Joshi"
    link: "https://researchr.org/alias/rajeev-joshi"
  volume: "6617"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-20397-8"
  kind: "inproceedings"
  key: "CalcagnoD11"
- title: "Formal verification of automotive embedded software"
  author:
  - name: "Vassil Todorov"
    link: "https://researchr.org/alias/vassil-todorov"
  - name: "Frédéric Boulanger"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-boulanger"
  - name: "Safouan Taha"
    link: "https://researchr.org/alias/safouan-taha"
  year: "2018"
  doi: "http://ieeexplore.ieee.org/document/8536209"
  links:
    doi: "http://ieeexplore.ieee.org/document/8536209"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icse/TodorovBT18"
  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:
  - name: "Stefania Gnesi"
    link: "https://researchr.org/alias/stefania-gnesi"
  - name: "Nico Plat"
    link: "https://researchr.org/alias/nico-plat"
  - name: "Paola Spoletini"
    link: "https://researchr.org/alias/paola-spoletini"
  - name: "Patrizio Pelliccione"
    link: "https://researchr.org/alias/patrizio-pelliccione"
  publisher: "ACM"
  kind: "inproceedings"
  key: "TodorovBT18"
- title: "Scaling static analyses at Facebook"
  author:
  - name: "Dino Distefano"
    link: "https://researchr.org/alias/dino-distefano"
  - name: "Manuel Fähndrich"
    link: "https://researchr.org/alias/manuel-f%C3%A4hndrich"
  - name: "Francesco Logozzo"
    link: "https://researchr.org/alias/francesco-logozzo"
  - name: "Peter W. O'Hearn"
    link: "https://researchr.org/alias/peter-w.-o%27hearn"
  year: "2019"
  doi: "https://doi.org/10.1145/3338112"
  links:
    doi: "https://doi.org/10.1145/3338112"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/cacm/DistefanoFLO19"
  researchr: "https://researchr.org/publication/DistefanoFLO19"
  cites: 0
  citedby: 0
  journal: "Communications of the ACM"
  volume: "62"
  number: "8"
  pages: "62-70"
  kind: "article"
  key: "DistefanoFLO19"
- title: "A Deductive Verification Platform for Cryptographic Software"
  author:
  - name: "Manuel Barbosa"
    link: "https://researchr.org/alias/manuel-barbosa"
  - name: "Jorge Sousa Pinto"
    link: "https://researchr.org/alias/jorge-sousa-pinto"
  - name: "Jean-Christophe Filliåtre"
    link: "https://researchr.org/alias/jean-christophe-filli%C3%A5tre"
  - name: "Bárbara Vieira"
    link: "https://researchr.org/alias/b%C3%A1rbara-vieira"
  year: "2010"
  doi: "http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461"
  links:
    doi: "http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/eceasst/BarbosaPFV10"
  tags:
  - "Frama-C"
  - "cryptography"
  researchr: "https://researchr.org/publication/BarbosaPFV10"
  cites: 0
  citedby: 0
  journal: "ECEASST"
  volume: "33"
  kind: "article"
  key: "BarbosaPFV10"
- title: "Formal Verification of Algorithms for Critical Systems"
  author:
  - name: "John M. Rushby"
    link: "https://researchr.org/alias/john-m.-rushby"
  - name: "Friedrich W. von Henke"
    link: "https://researchr.org/alias/friedrich-w.-von-henke"
  year: "1993"
  doi: "http://www.computer.org/tse/ts1993/e0013abs.htm"
  links:
    doi: "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"
  kind: "article"
  key: "RushbyH93"
- title: "Verification of Decision Making Software in an Autonomous Vehicle: An Industrial Case Study"
  author:
  - name: "Yuvaraj Selvaraj"
    link: "https://researchr.org/alias/yuvaraj-selvaraj"
  - name: "Wolfgang Ahrendt"
    link: "https://researchr.org/alias/wolfgang-ahrendt"
  - name: "Martin Fabian"
    link: "https://researchr.org/alias/martin-fabian"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-27008-7_9"
  links:
    doi: "https://doi.org/10.1007/978-3-030-27008-7_9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fmics/SelvarajAF19"
  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:
  - name: "Kim Guldstrand Larsen"
    link: "https://researchr.org/alias/kim-guldstrand-larsen"
  - name: "Tim A. C. Willemse"
    link: "https://researchr.org/alias/tim-a.-c.-willemse"
  volume: "11687"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-27008-7"
  kind: "inproceedings"
  key: "SelvarajAF19"
- title: "A Survey of Hybrid Techniques for Functional Verification"
  author:
  - name: "Jayanta Bhadra"
    link: "https://researchr.org/alias/jayanta-bhadra"
  - name: "Magdy S. Abadir"
    link: "https://researchr.org/alias/magdy-s.-abadir"
  - name: "Li-C. Wang"
    link: "https://researchr.org/alias/li-c.-wang"
  - name: "Sandip Ray"
    link: "https://researchr.org/alias/sandip-ray"
  year: "2007"
  doi: "http://doi.ieeecomputersociety.org/10.1109/MDT.2007.30"
  links:
    doi: "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"
  kind: "article"
  key: "BhadraAWR07"
- title: "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS"
  author:
  - name: "Sam Owre"
    link: "https://researchr.org/alias/sam-owre"
  - name: "John M. Rushby"
    link: "https://researchr.org/alias/john-m.-rushby"
  - name: "Natarajan Shankar"
    link: "https://researchr.org/alias/natarajan-shankar"
  - name: "Friedrich W. von Henke"
    link: "https://researchr.org/alias/friedrich-w.-von-henke"
  year: "1995"
  doi: "http://www.computer.org/tse/ts1995/e0107abs.htm"
  links:
    doi: "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"
  kind: "article"
  key: "OwreRSH95"
- title: "Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists"
  author:
  - name: "Léo Creuse"
    link: "https://researchr.org/alias/l%C3%A9o-creuse"
  - name: "Claire Dross"
    link: "https://researchr.org/alias/claire-dross"
  - name: "Christophe Garion"
    link: "https://researchr.org/alias/christophe-garion"
  - name: "Jérôme Hugues"
    link: "https://researchr.org/alias/j%C3%A9r%C3%B4me-hugues"
  - name: "Joffrey Huguet"
    link: "https://researchr.org/alias/joffrey-huguet"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-32441-4_2"
  links:
    doi: "https://doi.org/10.1007/978-3-030-32441-4_2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tfm/CreuseDGHH99"
  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:
  - name: "Brijesh Dongol"
    link: "https://researchr.org/alias/brijesh-dongol"
  - name: "Luigia Petre"
    link: "https://researchr.org/alias/luigia-petre"
  - name: "Graeme Smith"
    link: "https://researchr.org/alias/graeme-smith"
  volume: "11758"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-32441-4"
  kind: "inproceedings"
  key: "CreuseDGHH99"
- title: "Adversarial robustness of deep neural networks: A survey from a formal verification perspective"
  author:
  - name: "Meng, Mark Huasong"
    link: "https://researchr.org/alias/meng%2C-mark-huasong"
  - name: "Bai, Guangdong"
    link: "https://researchr.org/alias/bai%2C-guangdong"
  - name: "Teo, Sin Gee"
    link: "https://researchr.org/alias/teo%2C-sin-gee"
  - name: "Hou, Zhe"
    link: "https://researchr.org/alias/hou%2C-zhe"
  - name: "Xiao, Yan"
    link: "https://researchr.org/alias/xiao%2C-yan"
  - name: "Lin, Yun"
    link: "https://researchr.org/alias/lin%2C-yun"
  - name: "Dong, Jin Song"
    link: "https://researchr.org/alias/dong%2C-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"
  kind: "article"
  key: "meng2022adversarial"
- title: "Formal Verification in Automotive Industry: Enablers and Obstacles"
  author:
  - name: "Mattias Nyberg"
    link: "https://researchr.org/alias/mattias-nyberg"
  - name: "Dilian Gurov"
    link: "https://researchr.org/alias/dilian-gurov"
  - name: "Christian Lidström"
    link: "https://researchr.org/alias/christian-lidstr%C3%B6m"
  - name: "Andreas Rasmusson"
    link: "https://researchr.org/alias/andreas-rasmusson"
  - name: "Jonas Westman"
    link: "https://researchr.org/alias/jonas-westman"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-030-03427-6_14"
  links:
    doi: "https://doi.org/10.1007/978-3-030-03427-6_14"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/isola/NybergGLRW18"
  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:
  - name: "Tiziana Margaria"
    link: "https://researchr.org/alias/tiziana-margaria"
  - name: "Bernhard Steffen"
    link: "https://researchr.org/alias/bernhard-steffen"
  volume: "11247"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-03427-6"
  kind: "inproceedings"
  key: "NybergGLRW18"
- title: "Formal Verification of Ada Programs"
  author:
  - name: "David Guaspari"
    link: "https://researchr.org/alias/david-guaspari"
  - name: "Carla Marceau"
    link: "https://researchr.org/alias/carla-marceau"
  - name: "Wolfgang Polak"
    link: "https://researchr.org/alias/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:
  - name: "Ursula Martin"
    link: "https://researchr.org/alias/ursula-martin"
  - name: "Jeannette M. Wing"
    link: "http://www.cs.cmu.edu/~wing/"
  series: "Workshops in Computing"
  publisher: "Springer"
  isbn: "3-540-19804-0"
  kind: "inproceedings"
  key: "GuaspariMP92"
- title: "Formal Verification of Medical Device User Interfaces Using PVS"
  author:
  - name: "Paolo Masci"
    link: "https://researchr.org/alias/paolo-masci"
  - name: "Yi Zhang"
    link: "https://researchr.org/alias/yi-zhang"
  - name: "Paul L. Jones"
    link: "https://researchr.org/alias/paul-l.-jones"
  - name: "Paul Curzon"
    link: "https://researchr.org/alias/paul-curzon"
  - name: "Harold W. Thimbleby"
    link: "https://researchr.org/alias/harold-w.-thimbleby"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-642-54804-8_14"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-54804-8_14"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fase/MasciZJCT14"
  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:
  - name: "Stefania Gnesi"
    link: "https://researchr.org/alias/stefania-gnesi"
  - name: "Arend Rensink"
    link: "https://researchr.org/alias/arend-rensink"
  volume: "8411"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-54803-1"
  kind: "inproceedings"
  key: "MasciZJCT14"
- title: "Formal verification of a realistic compiler"
  author:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2009"
  doi: "http://doi.acm.org/10.1145/1538788.1538814"
  abstract: "This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well."
  links:
    doi: "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"
  kind: "article"
  key: "Leroy09"
- title: "Software verification with VeriFast: Industrial case studies"
  author:
  - name: "Pieter Philippaerts"
    link: "https://researchr.org/alias/pieter-philippaerts"
  - name: "Jan Tobias Mühlberg"
    link: "https://researchr.org/alias/jan-tobias-m%C3%BChlberg"
  - name: "Willem Penninckx"
    link: "https://researchr.org/alias/willem-penninckx"
  - name: "Jan Smans"
    link: "https://researchr.org/alias/jan-smans"
  - name: "Bart Jacobs 0002"
    link: "https://researchr.org/alias/bart-jacobs-0002"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2014"
  doi: "http://dx.doi.org/10.1016/j.scico.2013.01.006"
  links:
    doi: "http://dx.doi.org/10.1016/j.scico.2013.01.006"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/scp/PhilippaertsMPS0P14"
  researchr: "https://researchr.org/publication/PhilippaertsMPS0P14"
  cites: 0
  citedby: 0
  journal: "Science of Computer Programming"
  volume: "82"
  pages: "77-97"
  kind: "article"
  key: "PhilippaertsMPS0P14"
- title: "BP: Formal Proofs, the Fine Print and Side Effects"
  author:
  - name: "Toby C. Murray"
    link: "https://researchr.org/alias/toby-c.-murray"
  - name: "Paul C. van Oorschot"
    link: "https://researchr.org/alias/paul-c.-van-oorschot"
  year: "2018"
  doi: "https://doi.org/10.1109/SecDev.2018.00009"
  links:
    doi: "https://doi.org/10.1109/SecDev.2018.00009"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/secdev/MurrayO18"
  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"
  kind: "inproceedings"
  key: "MurrayO18"
- title: "Comprehensive formal verification of an OS microkernel"
  author:
  - name: "Gerwin Klein"
    link: "https://researchr.org/alias/gerwin-klein"
  - name: "June Andronick"
    link: "https://researchr.org/alias/june-andronick"
  - name: "Kevin Elphinstone"
    link: "https://researchr.org/alias/kevin-elphinstone"
  - name: "Toby C. Murray"
    link: "https://researchr.org/alias/toby-c.-murray"
  - name: "Thomas Sewell"
    link: "https://researchr.org/alias/thomas-sewell"
  - name: "Rafal Kolanski"
    link: "https://researchr.org/alias/rafal-kolanski"
  - name: "Gernot Heiser"
    link: "https://researchr.org/alias/gernot-heiser"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2560537"
  links:
    doi: "http://doi.acm.org/10.1145/2560537"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tocs/KleinAEMSKH14"
  tags:
  - "Isabelle/HOL"
  researchr: "https://researchr.org/publication/KleinAEMSKH14"
  cites: 0
  citedby: 0
  journal: "ACM Trans. Comput. Syst."
  volume: "32"
  number: "1"
  pages: "2"
  kind: "article"
  key: "KleinAEMSKH14"
- title: "Formal Verification of Critical Aerospace Software"
  author:
  - name: "Wiels, Virginie"
    link: "https://researchr.org/alias/wiels%2C-virginie"
  - name: "Delmas, Robert"
    link: "https://researchr.org/alias/delmas%2C-robert"
  - name: "Doose, David"
    link: "https://researchr.org/alias/doose%2C-david"
  - name: "Garoche, Pierre-Lo{\\\"i}c"
    link: "https://researchr.org/alias/garoche%2C-pierre-lo%7B%5Eb%22i%7Dc"
  - name: "Cazin, J."
    link: "https://researchr.org/alias/cazin%2C-j."
  - name: "Durrieu, Guy"
    link: "https://researchr.org/alias/durrieu%2C-guy"
  year: "2012"
  month: "May"
  links:
    "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"
  kind: "article"
  key: "wiels:hal-01184099"
- title: "VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java"
  author:
  - name: "Bart Jacobs"
    link: "https://researchr.org/alias/bart-jacobs"
  - name: "Jan Smans"
    link: "https://researchr.org/alias/jan-smans"
  - name: "Pieter Philippaerts"
    link: "http://distrinet.cs.kuleuven.be/people/showMember.do?memberID=u0055108"
  - name: "Frédéric Vogels"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-vogels"
  - name: "Willem Penninckx"
    link: "https://researchr.org/alias/willem-penninckx"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2011"
  doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_4"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-20398-5_4"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/JacobsSPVPP11"
  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:
  - name: "Mihaela Gheorghiu Bobaru"
    link: "https://researchr.org/alias/mihaela-gheorghiu-bobaru"
  - name: "Klaus Havelund"
    link: "https://researchr.org/alias/klaus-havelund"
  - name: "Gerard J. Holzmann"
    link: "https://researchr.org/alias/gerard-j.-holzmann"
  - name: "Rajeev Joshi"
    link: "https://researchr.org/alias/rajeev-joshi"
  volume: "6617"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-20397-8"
  kind: "inproceedings"
  key: "JacobsSPVPP11"
- title: "Deductive Verification of Smart Contracts with Dafny"
  author:
  - name: "Franck Cassez"
    link: "https://researchr.org/alias/franck-cassez"
  - name: "Joanne Fuller"
    link: "https://researchr.org/alias/joanne-fuller"
  - name: "Horacio Mijail Anton Quiles"
    link: "https://researchr.org/alias/horacio-mijail-anton-quiles"
  year: "2022"
  doi: "https://doi.org/10.1007/978-3-031-15008-1_5"
  links:
    doi: "https://doi.org/10.1007/978-3-031-15008-1_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fmics/CassezFQ22"
  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:
  - name: "Jan Friso Groote"
    link: "https://researchr.org/alias/jan-friso-groote"
  - name: "Marieke Huisman"
    link: "https://researchr.org/alias/marieke-huisman"
  volume: "13487"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-031-15008-1"
  kind: "inproceedings"
  key: "CassezFQ22"
- title: "Randomized Differential Testing as a Prelude to Formal Verification"
  author:
  - name: "Alex Groce"
    link: "https://researchr.org/alias/alex-groce"
  - name: "Gerard J. Holzmann"
    link: "https://researchr.org/alias/gerard-j.-holzmann"
  - name: "Rajeev Joshi"
    link: "https://researchr.org/alias/rajeev-joshi"
  year: "2007"
  doi: "http://doi.ieeecomputersociety.org/10.1109/ICSE.2007.68"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "GroceHJ07"
- title: "Formal Verification of Software Countermeasures against Side-Channel Attacks"
  author:
  - name: "Hassan Eldib"
    link: "https://researchr.org/alias/hassan-eldib"
  - name: "Chao Wang"
    link: "https://researchr.org/alias/chao-wang"
  - name: "Patrick Schaumont"
    link: "https://researchr.org/alias/patrick-schaumont"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2685616"
  links:
    doi: "http://doi.acm.org/10.1145/2685616"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tosem/EldibWS14"
  researchr: "https://researchr.org/publication/EldibWS14-0"
  cites: 0
  citedby: 0
  journal: "ACM Transactions on Software Engineering Methodology"
  volume: "24"
  number: "2"
  pages: "11"
  kind: "article"
  key: "EldibWS14-0"
- title: "Diversity-Driven Automated Formal Verification"
  author:
  - name: "Emily First"
    link: "https://researchr.org/alias/emily-first"
  - name: "Yuriy Brun"
    link: "https://researchr.org/alias/yuriy-brun"
  year: "2022"
  doi: "https://doi.org/10.1145/3510003.3510138"
  links:
    doi: "https://doi.org/10.1145/3510003.3510138"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icse/FirstB22"
  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"
  kind: "inproceedings"
  key: "FirstB22"
- title: "Industrial experience with SPARK"
  author:
  - name: "Chapman, Roderick"
    link: "https://researchr.org/alias/chapman%2C-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"
  kind: "article"
  key: "chapman2000industrial"
- title: "Large-scale formal verification in practice: A process perspective"
  author:
  - name: "June Andronick"
    link: "https://researchr.org/alias/june-andronick"
  - name: "D. Ross Jeffery"
    link: "https://researchr.org/alias/d.-ross-jeffery"
  - name: "Gerwin Klein"
    link: "https://researchr.org/alias/gerwin-klein"
  - name: "Rafal Kolanski"
    link: "https://researchr.org/alias/rafal-kolanski"
  - name: "Mark Staples"
    link: "https://researchr.org/alias/mark-staples"
  - name: "He Zhang"
    link: "https://researchr.org/alias/he-zhang"
  - name: "Liming Zhu"
    link: "https://researchr.org/alias/liming-zhu"
  year: "2012"
  doi: "http://dx.doi.org/10.1109/ICSE.2012.6227120"
  links:
    doi: "http://dx.doi.org/10.1109/ICSE.2012.6227120"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icse/AndronickJKKSZZ12"
  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:
  - name: "Martin Glinz"
    link: "https://researchr.org/alias/martin-glinz"
  - name: "Gail C. Murphy"
    link: "https://researchr.org/alias/gail-c.-murphy"
  - name: "Mauro Pezzè"
    link: "https://researchr.org/alias/mauro-pezz%C3%A8"
  publisher: "IEEE"
  isbn: "978-1-4673-1067-3"
  kind: "inproceedings"
  key: "AndronickJKKSZZ12"
- title: "Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report"
  author:
  - name: "Dilian Gurov"
    link: "https://researchr.org/alias/dilian-gurov"
  - name: "Christian Lidström"
    link: "https://researchr.org/alias/christian-lidstr%C3%B6m"
  - name: "Mattias Nyberg"
    link: "https://researchr.org/alias/mattias-nyberg"
  - name: "Jonas Westman"
    link: "https://researchr.org/alias/jonas-westman"
  year: "2017"
  doi: "https://doi.org/10.1007/978-3-319-67113-0_1"
  links:
    doi: "https://doi.org/10.1007/978-3-319-67113-0_1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fmics/GurovLNW17"
  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:
  - name: "Laure Petrucci"
    link: "https://researchr.org/alias/laure-petrucci"
  - name: "Cristina Seceleanu"
    link: "https://researchr.org/alias/cristina-seceleanu"
  - name: "Ana Cavalcanti"
    link: "https://researchr.org/alias/ana-cavalcanti"
  volume: "10471"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-67113-0"
  kind: "inproceedings"
  key: "GurovLNW17"
- title: "The B-book - assigning programs to meanings"
  author:
  - name: "Jean-Raymond Abrial"
    link: "https://researchr.org/alias/jean-raymond-abrial"
  year: "2005"
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0015096"
  researchr: "https://researchr.org/publication/0015096"
  cites: 0
  citedby: 0
  publisher: "Cambridge University Press"
  isbn: "978-0-521-02175-3"
  kind: "book"
  key: "0015096"