publications:
- title: "Dependent types and multi-monadic effects in F*"
  author:
  - name: "Nikhil Swamy"
    link: "https://researchr.org/alias/nikhil-swamy"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  - name: "Chantal Keller"
    link: "https://researchr.org/alias/chantal-keller"
  - name: "Aseem Rastogi"
    link: "https://researchr.org/alias/aseem-rastogi"
  - name: "Antoine Delignat-Lavaud"
    link: "https://researchr.org/alias/antoine-delignat-lavaud"
  - name: "Simon Forest"
    link: "https://researchr.org/alias/simon-forest"
  - name: "Karthikeyan Bhargavan"
    link: "https://researchr.org/alias/karthikeyan-bhargavan"
  - name: "Cédric Fournet"
    link: "https://researchr.org/alias/c%C3%A9dric-fournet"
  - name: "Pierre-Yves Strub"
    link: "https://researchr.org/alias/pierre-yves-strub"
  - name: "Markulf Kohlweiss"
    link: "https://researchr.org/alias/markulf-kohlweiss"
  - name: "Jean Karim Zinzindohoue"
    link: "https://researchr.org/alias/jean-karim-zinzindohoue"
  - name: "Santiago Zanella Béguelin"
    link: "https://researchr.org/alias/santiago-zanella-b%C3%A9guelin"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2837614.2837655"
  links:
    doi: "http://doi.acm.org/10.1145/2837614.2837655"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/SwamyHKRDFBFSKZ16"
  researchr: "https://researchr.org/publication/SwamyHKRDFBFSKZ16"
  cites: 0
  citedby: 0
  pages: "256-270"
  booktitle: "Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016"
  editor:
  - name: "Rastislav Bodik"
    link: "https://researchr.org/alias/rastislav-bodik"
  - name: "Rupak Majumdar"
    link: "https://researchr.org/alias/rupak-majumdar"
  publisher: "ACM"
  isbn: "978-1-4503-3549-2"
  kind: "inproceedings"
  key: "SwamyHKRDFBFSKZ16"
- title: "Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY"
  year: "2020"
  doi: "https://doi.org/10.1007/978-3-030-64354-6"
  links:
    doi: "https://doi.org/10.1007/978-3-030-64354-6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/series/lncs/12345"
  researchr: "https://researchr.org/publication/lncs-12345"
  cites: 0
  citedby: 0
  editor:
  - name: "Wolfgang Ahrendt"
    link: "https://researchr.org/alias/wolfgang-ahrendt"
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Richard Bubel"
    link: "https://researchr.org/alias/richard-bubel"
  - name: "Reiner Hähnle"
    link: "https://researchr.org/alias/reiner-h%C3%A4hnle"
  - name: "Mattias Ulbrich"
    link: "https://researchr.org/alias/mattias-ulbrich"
  volume: "12345"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-64354-6"
  kind: "book"
  key: "lncs-12345"
- title: "Evaluating the Interfaces of Three Theorem Proving Assistants"
  author:
  - name: "Nicholas A. Merriam"
    link: "https://researchr.org/alias/nicholas-a.-merriam"
  - name: "Michael D. Harrison"
    link: "https://researchr.org/alias/michael-d.-harrison"
  year: "1996"
  researchr: "https://researchr.org/publication/MerriamH96"
  cites: 0
  citedby: 0
  pages: "330-346"
  booktitle: "Design, Specification and Verification of Interactive Systems 96, Proceedings of the Third International Eurographics Workshop, June 5-7, 1996, Namur, Belgium"
  editor:
  - name: "François Bodart"
    link: "https://researchr.org/alias/fran%C3%A7ois-bodart"
  - name: "Jean Vanderdonckt"
    link: "https://researchr.org/alias/jean-vanderdonckt"
  publisher: "Springer"
  isbn: "3-211-82900-8"
  kind: "inproceedings"
  key: "MerriamH96"
- title: "The interactive verification debugger: effective understanding of interactive proof attempts"
  author:
  - name: "Martin Hentschel 0002"
    link: "https://researchr.org/alias/martin-hentschel-0002"
  - name: "Reiner Hähnle"
    link: "https://researchr.org/alias/reiner-h%C3%A4hnle"
  - name: "Richard Bubel"
    link: "https://researchr.org/alias/richard-bubel"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2970276.2970292"
  links:
    doi: "http://doi.acm.org/10.1145/2970276.2970292"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/kbse/0002HB16a"
  tags:
  - "KeyMaera"
  researchr: "https://researchr.org/publication/0002HB16a"
  cites: 0
  citedby: 0
  pages: "846-851"
  booktitle: "Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering"
  editor:
  - name: "David Lo"
    link: "https://researchr.org/alias/david-lo"
  - name: "Sven Apel"
    link: "https://researchr.org/alias/sven-apel"
  - name: "Sarfraz Khurshid"
    link: "https://researchr.org/alias/sarfraz-khurshid"
  publisher: "ACM"
  isbn: "978-1-4503-3845-5"
  kind: "inproceedings"
  key: "0002HB16a"
- title: "Experience Report: Teaching Code Analysis and Verification Using Frama-C"
  author:
  - name: "Salwa Souaf"
    link: "https://researchr.org/alias/salwa-souaf"
  - name: "Frédéric Loulergue"
    link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-loulergue"
  year: "2021"
  month: "nov"
  doi: "10.4204/eptcs.349.5"
  links:
    "url": "https://doi.org/10.4204%2Feptcs.349.5"
  researchr: "https://researchr.org/publication/Souaf2021"
  cites: 0
  citedby: 0
  journal: "Electronic Proceedings in Theoretical Computer Science"
  volume: "349"
  pages: "69-75"
  kind: "article"
  key: "Souaf2021"
- title: "A Comparison of PVS and Isabelle/HOL"
  author:
  - name: "W. O. David Griffioen"
    link: "https://researchr.org/alias/w.-o.-david-griffioen"
  - name: "Marieke Huisman"
    link: "https://researchr.org/alias/marieke-huisman"
  year: "1998"
  researchr: "https://researchr.org/publication/GriffioenH98"
  cites: 0
  citedby: 0
  pages: "123-142"
  booktitle: "Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs 98, Canberra, Australia, September 27 - October 1, 1998, Proceedings"
  editor:
  - name: "Jim Grundy"
    link: "https://researchr.org/alias/jim-grundy"
  - name: "Malcolm C. Newey"
    link: "https://researchr.org/alias/malcolm-c.-newey"
  volume: "1479"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-64987-5"
  kind: "inproceedings"
  key: "GriffioenH98"
- title: "Interactive Theorem Proving - Modelling the User in the Proof Process"
  author:
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Sarah Grebing"
    link: "https://researchr.org/alias/sarah-grebing"
  year: "2015"
  doi: "http://ceur-ws.org/Vol-1412/6o.pdf"
  links:
    doi: "http://ceur-ws.org/Vol-1412/6o.pdf"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/BeckertG15"
  tags:
  - "KeyMaera"
  researchr: "https://researchr.org/publication/BeckertG15"
  cites: 0
  citedby: 0
  pages: "60-73"
  booktitle: "Proceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning - A workshop of the 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, August 1, 2015"
  editor:
  - name: "Ulrich Furbach"
    link: "https://researchr.org/alias/ulrich-furbach"
  - name: "Claudia Schon"
    link: "https://researchr.org/alias/claudia-schon"
  volume: "1412"
  series: "CEUR Workshop Proceedings"
  publisher: "CEUR-WS.org"
  kind: "inproceedings"
  key: "BeckertG15"
- title: "Helium, for learning Haskell"
  author:
  - name: "Bastiaan Heeren"
    link: "http://www.open.ou.nl/bhr/"
  - name: "Daan Leijen"
    link: "https://researchr.org/alias/daan-leijen"
  - name: "Arjan van IJzendoorn"
    link: "https://researchr.org/alias/arjan-van-ijzendoorn"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/871895.871902"
  links:
    doi: "http://doi.acm.org/10.1145/871895.871902"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/HeerenLI03"
  tags:
  - "error-reporting"
  researchr: "https://researchr.org/publication/HeerenLI03"
  cites: 0
  citedby: 0
  pages: "62-71"
  booktitle: "Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2003, Uppsala, Sweden, August 28, 2003"
  publisher: "ACM"
  kind: "inproceedings"
  key: "HeerenLI03"
- title: "More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme"
  author:
  - name: "James Noble 0001"
    link: "https://researchr.org/alias/james-noble-0001"
  - name: "David Streader"
    link: "https://researchr.org/alias/david-streader"
  - name: "Isaac Oscar Gariano"
    link: "https://researchr.org/alias/isaac-oscar-gariano"
  - name: "Miniruwani Samarakoon"
    link: "https://researchr.org/alias/miniruwani-samarakoon"
  year: "2022"
  doi: "https://doi.org/10.1007/978-3-031-06773-0_23"
  links:
    doi: "https://doi.org/10.1007/978-3-031-06773-0_23"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/nfm/NobleSGS22"
  researchr: "https://researchr.org/publication/NobleSGS22"
  cites: 0
  citedby: 0
  pages: "431-450"
  booktitle: "NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings"
  editor:
  - name: "Jyotirmoy V. Deshmukh"
    link: "https://researchr.org/alias/jyotirmoy-v.-deshmukh"
  - name: "Klaus Havelund"
    link: "https://researchr.org/alias/klaus-havelund"
  - name: "Ivan Perez 0001"
    link: "https://researchr.org/alias/ivan-perez-0001"
  volume: "13260"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-031-06773-0"
  kind: "inproceedings"
  key: "NobleSGS22"
- 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: "Dafny: An Automatic Program Verifier for Functional Correctness"
  author:
  - name: "K. Rustan M. Leino"
    link: "https://researchr.org/alias/k.-rustan-m.-leino"
  year: "2010"
  doi: "http://dx.doi.org/10.1007/978-3-642-17511-4_20"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-17511-4_20"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lpar/Leino10"
  tags:
  - "program verification"
  - "functional programming"
  researchr: "https://researchr.org/publication/Leino10-2"
  cites: 0
  citedby: 0
  pages: "348-370"
  booktitle: "Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers"
  editor:
  - name: "Edmund M. Clarke"
    link: "https://researchr.org/alias/edmund-m.-clarke"
  - name: "Andrei Voronkov"
    link: "https://researchr.org/alias/andrei-voronkov"
  volume: "6355"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-17510-7"
  kind: "inproceedings"
  key: "Leino10-2"
- title: "REPLica: REPL instrumentation for Coq analysis"
  author:
  - name: "Talia Ringer"
    link: "https://researchr.org/alias/talia-ringer"
  - name: "Alex Sanchez-Stern"
    link: "https://researchr.org/alias/alex-sanchez-stern"
  - name: "Dan Grossman"
    link: "https://researchr.org/alias/dan-grossman"
  - name: "Sorin Lerner"
    link: "https://researchr.org/alias/sorin-lerner"
  year: "2020"
  doi: "https://doi.org/10.1145/3372885.3373823"
  links:
    doi: "https://doi.org/10.1145/3372885.3373823"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/RingerSGL20"
  researchr: "https://researchr.org/publication/RingerSGL20"
  cites: 0
  citedby: 0
  pages: "99-113"
  booktitle: "Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020"
  editor:
  - name: "Jasmin Blanchette"
    link: "https://researchr.org/alias/jasmin-blanchette"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  publisher: "ACM"
  isbn: "978-1-4503-7097-4"
  kind: "inproceedings"
  key: "RingerSGL20"
- title: "A Usability Evaluation of Interactive Theorem Provers Using Focus Groups"
  author:
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Sarah Grebing"
    link: "https://researchr.org/alias/sarah-grebing"
  - name: "Florian Böhl"
    link: "https://researchr.org/alias/florian-b%C3%B6hl"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-15201-1_1"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-15201-1_1"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sefm/BeckertGB14"
  researchr: "https://researchr.org/publication/BeckertGB14"
  cites: 0
  citedby: 0
  pages: "3-19"
  booktitle: "Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers"
  editor:
  - name: "Carlos Canal"
    link: "https://researchr.org/alias/carlos-canal"
  - name: "Akram Idani"
    link: "https://researchr.org/alias/akram-idani"
  volume: "8938"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-15200-4"
  kind: "inproceedings"
  key: "BeckertGB14"
- title: "Towards progressive program verification in Dafny"
  author:
  - name: "Ismael Figueroa"
    link: "https://researchr.org/alias/ismael-figueroa"
  - name: "Bruno García"
    link: "https://researchr.org/alias/bruno-garc%C3%ADa"
  - name: "Paul Leger"
    link: "http://pleger.cl"
  year: "2018"
  doi: "https://doi.org/10.1145/3264637.3264649"
  links:
    doi: "https://doi.org/10.1145/3264637.3264649"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sblp/FigueroaGL18"
  researchr: "https://researchr.org/publication/FigueroaGL18"
  cites: 0
  citedby: 0
  pages: "90-97"
  booktitle: "Proceedings of the XXII Brazilian Symposium on Programming Languages, SBLP 2018, Sao Carlos, Brazil, September 20-21, 2018"
  editor:
  - name: "Carlos Camarão"
    link: "https://researchr.org/alias/carlos-camar%C3%A3o"
  - name: "Martin Sulzmann"
    link: "https://researchr.org/alias/martin-sulzmann"
  publisher: "ACM"
  isbn: "978-1-4503-6480-5"
  kind: "inproceedings"
  key: "FigueroaGL18"
- title: "Why3 - Where Programs Meet Provers"
  author:
  - name: "Jean-Christophe Filliâtre"
    link: "https://researchr.org/alias/jean-christophe-filli%C3%A2tre"
  - name: " Andrei Paskevich"
    link: "https://researchr.org/alias/andrei-paskevich"
  year: "2013"
  doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_8"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_8"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/FilliatreP13"
  researchr: "https://researchr.org/publication/FilliatreP13"
  cites: 0
  citedby: 0
  pages: "125-128"
  booktitle: "Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings"
  editor:
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Philippa Gardner"
    link: "https://researchr.org/alias/philippa-gardner"
  volume: "7792"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-37035-9"
  kind: "inproceedings"
  key: "FilliatreP13"
- title: "Nagini: A Static Verifier for Python"
  author:
  - name: "Marco Eilers"
    link: "https://researchr.org/alias/marco-eilers"
  - name: "Peter Müller 0001"
    link: "https://researchr.org/alias/peter-m%C3%BCller-0001"
  year: "2018"
  doi: "https://doi.org/10.1007/978-3-319-96145-3_33"
  links:
    doi: "https://doi.org/10.1007/978-3-319-96145-3_33"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cav/Eilers018"
  researchr: "https://researchr.org/publication/Eilers018"
  cites: 0
  citedby: 0
  pages: "596-603"
  booktitle: "Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I"
  editor:
  - name: "Hana Chockler"
    link: "https://researchr.org/alias/hana-chockler"
  - name: "Georg Weissenbacher"
    link: "https://researchr.org/alias/georg-weissenbacher"
  volume: "10981"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-96145-3"
  kind: "inproceedings"
  key: "Eilers018"
- title: "Desirable features of educational theorem provers - a cognitive dimensions viewpoint"
  author:
  - name: "Gada F. Kadoda"
    link: "https://researchr.org/alias/gada-f.-kadoda"
  - name: "Roger G. Stone"
    link: "https://researchr.org/alias/roger-g.-stone"
  - name: "Dan Diaper"
    link: "https://researchr.org/alias/dan-diaper"
  year: "1999"
  doi: "http://ppig.org/library/paper/desirable-features-educational-theorem-provers-cognitive-dimensions-viewpoint"
  links:
    doi: "http://ppig.org/library/paper/desirable-features-educational-theorem-provers-cognitive-dimensions-viewpoint"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppig/KadodaSD99"
  researchr: "https://researchr.org/publication/KadodaSD99"
  cites: 0
  citedby: 0
  pages: "4"
  booktitle: "Proceedings of the 11th Annual Workshop of the Psychology of Programming Interest Group, PPIG 1999, Leeds, UK, January 5-7, 1999"
  publisher: "Psychology of Programming Interest Group"
  kind: "inproceedings"
  key: "KadodaSD99"
- title: "Evaluating the Usability of Interactive Verification Systems"
  author:
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Sarah Grebing"
    link: "https://researchr.org/alias/sarah-grebing"
  year: "2012"
  doi: "http://ceur-ws.org/Vol-873/papers/paper_4.pdf"
  links:
    doi: "http://ceur-ws.org/Vol-873/papers/paper_4.pdf"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cade/BeckertG12"
  tags:
  - "KeyMaera"
  researchr: "https://researchr.org/publication/BeckertG12"
  cites: 0
  citedby: 0
  pages: "3-17"
  booktitle: "Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012"
  editor:
  - name: "Vladimir Klebanov"
    link: "https://researchr.org/alias/vladimir-klebanov"
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Armin Biere"
    link: "https://researchr.org/alias/armin-biere"
  - name: "Geoff Sutcliffe"
    link: "https://researchr.org/alias/geoff-sutcliffe"
  volume: "873"
  series: "CEUR Workshop Proceedings"
  publisher: "CEUR-WS.org"
  kind: "inproceedings"
  key: "BeckertG12"
- title: "Teaching Formal Methods to Future Engineers"
  author:
  - name: "Catherine Dubois"
    link: "https://researchr.org/alias/catherine-dubois"
  - name: "Virgile Prevosto"
    link: "https://researchr.org/alias/virgile-prevosto"
  - name: "Guillaume Burel"
    link: "https://researchr.org/alias/guillaume-burel"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-32441-4_5"
  links:
    doi: "https://doi.org/10.1007/978-3-030-32441-4_5"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tfm/DuboisPB99"
  researchr: "https://researchr.org/publication/DuboisPB99"
  cites: 0
  citedby: 0
  pages: "69-80"
  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: "DuboisPB99"
- title: "Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study"
  author:
  - name: "Thorsten Bormer"
    link: "https://researchr.org/alias/thorsten-bormer"
  year: "2014"
  doi: "http://d-nb.info/1077821883"
  links:
    doi: "http://d-nb.info/1077821883"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/dnb/Bormer14"
  tags:
  - "VCC"
  researchr: "https://researchr.org/publication/dnb-250"
  cites: 0
  citedby: 0
  school: "Karlsruhe Institute of Technology"
  kind: "phdthesis"
  key: "dnb-250"
- title: "An empirical evaluation of two user interfaces of an interactive program verifier"
  author:
  - name: "Martin Hentschel 0002"
    link: "https://researchr.org/alias/martin-hentschel-0002"
  - name: "Reiner Hähnle"
    link: "https://researchr.org/alias/reiner-h%C3%A4hnle"
  - name: "Richard Bubel"
    link: "https://researchr.org/alias/richard-bubel"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2970276.2970303"
  links:
    doi: "http://doi.acm.org/10.1145/2970276.2970303"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/kbse/0002HB16"
  researchr: "https://researchr.org/publication/0002HB16-0"
  cites: 0
  citedby: 0
  pages: "403-413"
  booktitle: "Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering"
  editor:
  - name: "David Lo"
    link: "https://researchr.org/alias/david-lo"
  - name: "Sven Apel"
    link: "https://researchr.org/alias/sven-apel"
  - name: "Sarfraz Khurshid"
    link: "https://researchr.org/alias/sarfraz-khurshid"
  publisher: "ACM"
  isbn: "978-1-4503-3845-5"
  kind: "inproceedings"
  key: "0002HB16-0"
- title: "An analysis of errors in interactive proof attempts"
  author:
  - name: "J. Stuart Aitken"
    link: "https://researchr.org/alias/j.-stuart-aitken"
  - name: "Thomas F. Melham"
    link: "https://researchr.org/alias/thomas-f.-melham"
  year: "2000"
  tags:
  - "Isabelle/HOL"
  - "analysis"
  researchr: "https://researchr.org/publication/AitkenM00"
  cites: 0
  citedby: 0
  journal: "Interacting with Computers"
  volume: "12"
  number: "6"
  pages: "565-586"
  kind: "article"
  key: "AitkenM00"
- title: "Seamless Interactive Program Verification"
  author:
  - name: "Sarah Grebing"
    link: "https://researchr.org/alias/sarah-grebing"
  - name: "Jonas Klamroth"
    link: "https://researchr.org/alias/jonas-klamroth"
  - name: "Mattias Ulbrich"
    link: "https://researchr.org/alias/mattias-ulbrich"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-41600-3_6"
  links:
    doi: "https://doi.org/10.1007/978-3-030-41600-3_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/vstte/GrebingKU19"
  researchr: "https://researchr.org/publication/GrebingKU19"
  cites: 0
  citedby: 0
  pages: "68-86"
  booktitle: "Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers"
  editor:
  - name: "Supratik Chakraborty"
    link: "https://researchr.org/alias/supratik-chakraborty"
  - name: "Jorge A. Navas"
    link: "https://researchr.org/alias/jorge-a.-navas"
  volume: "12031"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-41600-3"
  kind: "inproceedings"
  key: "GrebingKU19"
- title: "Interactive Theorem Proving: An Empirical Study of User Activity"
  author:
  - name: "J. Stuart Aitken"
    link: "https://researchr.org/alias/j.-stuart-aitken"
  - name: "Philip D. Gray"
    link: "https://researchr.org/alias/philip-d.-gray"
  - name: "Thomas F. Melham"
    link: "https://researchr.org/alias/thomas-f.-melham"
  - name: "Muffy Thomas"
    link: "https://researchr.org/alias/muffy-thomas"
  year: "1998"
  tags:
  - "empirical"
  - "Isabelle/HOL"
  researchr: "https://researchr.org/publication/AitkenGMT98"
  cites: 0
  citedby: 0
  journal: "Journal of Symbolic Computation"
  volume: "25"
  number: "2"
  pages: "263-284"
  kind: "article"
  key: "AitkenGMT98"
- title: "Teaching Deductive Verification in Why3 to Undergraduate Students"
  author:
  - name: "Sandrine Blazy"
    link: "https://researchr.org/alias/sandrine-blazy"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-030-32441-4_4"
  links:
    doi: "https://doi.org/10.1007/978-3-030-32441-4_4"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tfm/Blazy99"
  researchr: "https://researchr.org/publication/Blazy99"
  cites: 0
  citedby: 0
  pages: "52-66"
  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: "Blazy99"
- title: "Making Design Decisions to Support Diversity in Interactive Theorem Proving"
  author:
  - name: "Nicholas A. Merriam"
    link: "https://researchr.org/alias/nicholas-a.-merriam"
  - name: "Michael D. Harrison"
    link: "https://researchr.org/alias/michael-d.-harrison"
  - name: "Michael D. Harrison"
    link: "https://researchr.org/alias/michael-d.-harrison"
  year: "1998"
  links:
    "url": "https://api.semanticscholar.org/CorpusID:16809476"
  researchr: "https://researchr.org/publication/Merriam1998MakingDD"
  cites: 0
  citedby: 0
  kind: "inproceedings"
  key: "Merriam1998MakingDD"
- title: "Can program proving be made practical?"
  author:
  - name: "Ole-Johan Dahl"
    link: "https://researchr.org/alias/ole-johan-dahl"
  year: "1977"
  researchr: "https://researchr.org/publication/Dahl1977"
  cites: 0
  citedby: 0
  booktitle: "Lectures Presented at the EEC-crest Course on Programming Foundations, Toulouse 1977"
  organization: "Universitetet i Oslo"
  publisher: "Institute of Informatics"
  kind: "incollection"
  key: "Dahl1977"
- title: "Passport: Improving Automated Formal Verification Using Identifiers"
  author:
  - name: "Sanchez-Stern, Alex"
    link: "https://researchr.org/alias/sanchez-stern%2C-alex"
  - name: "First, Emily"
    link: "https://researchr.org/alias/first%2C-emily"
  - name: "Zhou, Timothy"
    link: "https://researchr.org/alias/zhou%2C-timothy"
  - name: "Kaufman, Zhanna"
    link: "https://researchr.org/alias/kaufman%2C-zhanna"
  - name: "Brun, Yuriy"
    link: "https://researchr.org/alias/brun%2C-yuriy"
  - name: "Ringer, Talia"
    link: "https://researchr.org/alias/ringer%2C-talia"
  year: "2023"
  month: "jun"
  doi: "10.1145/3593374"
  abstract: "Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpora to synthesize proofs have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the powerful logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than on how to make the most of the proof data. This article systematically explores how to most effectively exploit one aspect of that proof data: identifiers.We develop the Passport approach, a method for enriching the predictive Coq model used by an existing proof-synthesis tool with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We evaluate our approach?s enrichment effect on three existing base tools: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29\\% more theorems than the best-performing of these base tools. Combining the three tools enhanced by the Passport approach automatically proves 38\\% more theorems than combining the three base tools. Finally, together, these base tools and their enhanced versions prove 45\\% more theorems than the combined base tools. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software."
  links:
    "url": "https://doi.org/10.1145/3593374"
  researchr: "https://researchr.org/publication/10.1145-3593374"
  cites: 0
  citedby: 0
  journal: "ACM Trans. Program. Lang. Syst."
  volume: "45"
  number: "2"
  kind: "article"
  key: "10.1145-3593374"
- title: "Usability Recommendations for User Guidance in Deductive Program Verification"
  author:
  - name: "Sarah Grebing"
    link: "https://researchr.org/alias/sarah-grebing"
  - name: "Mattias Ulbrich"
    link: "https://researchr.org/alias/mattias-ulbrich"
  year: "2020"
  doi: "https://doi.org/10.1007/978-3-030-64354-6_11"
  links:
    doi: "https://doi.org/10.1007/978-3-030-64354-6_11"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/series/lncs/GrebingU20"
  tags:
  - "KeyMaera"
  researchr: "https://researchr.org/publication/GrebingU20"
  cites: 0
  citedby: 0
  pages: "261-284"
  booktitle: "Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY"
  editor:
  - name: "Wolfgang Ahrendt"
    link: "https://researchr.org/alias/wolfgang-ahrendt"
  - name: "Bernhard Beckert"
    link: "https://researchr.org/alias/bernhard-beckert"
  - name: "Richard Bubel"
    link: "https://researchr.org/alias/richard-bubel"
  - name: "Reiner Hähnle"
    link: "https://researchr.org/alias/reiner-h%C3%A4hnle"
  - name: "Mattias Ulbrich"
    link: "https://researchr.org/alias/mattias-ulbrich"
  volume: "12345"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-030-64354-6"
  kind: "incollection"
  key: "GrebingU20"
- title: "Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools"
  author:
  - name: "Reiner Hähnle"
    link: "https://researchr.org/alias/reiner-h%C3%A4hnle"
  - name: "Marieke Huisman"
    link: "https://researchr.org/alias/marieke-huisman"
  year: "2019"
  doi: "https://doi.org/10.1007/978-3-319-91908-9_18"
  links:
    doi: "https://doi.org/10.1007/978-3-319-91908-9_18"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/series/lncs/HahnleH19"
  researchr: "https://researchr.org/publication/HahnleH19"
  cites: 0
  citedby: 0
  pages: "345-373"
  booktitle: "VIDEO: Lecture Notes in Computer Science Celebrates 10,000th Manuscript!"
  volume: "10000"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  kind: "incollection"
  key: "HahnleH19"
- title: "Thoughts on Requirements and Design Issues of User Interfaces for Proof Assistants"
  author:
  - name: "Norbert Völker"
    link: "https://researchr.org/alias/norbert-v%C3%B6lker"
  year: "2004"
  doi: "http://dx.doi.org/10.1016/j.entcs.2004.05.001"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2004.05.001"
  tags:
  - "proof assistant"
  - "design"
  researchr: "https://researchr.org/publication/Volker04"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "103"
  pages: "139-159"
  kind: "article"
  key: "Volker04"
- title: "Bringing Formal Verification into Widespread Programming Language Ecosystems"
  author:
  - name: "Sára Juhošová"
    link: "https://researchr.org/alias/s%C3%A1ra-juho%C5%A1ov%C3%A1"
  year: "2023"
  researchr: "https://researchr.org/publication/Juhoov2023"
  cites: 0
  citedby: 0
  school: "TU Delft"
  kind: "mastersthesis"
  key: "Juhoov2023"
- title: "Usability-Oriented Design of Liquid Types for Java"
  author:
  - name: "Gamboa, Catarina"
    link: "https://researchr.org/alias/gamboa%2C-catarina"
  - name: "Santos, Paulo"
    link: "https://researchr.org/alias/santos%2C-paulo"
  - name: "Timperley, Christopher Steven"
    link: "https://researchr.org/alias/timperley%2C-christopher-steven"
  - name: "Fonseca, Alcides"
    link: "https://researchr.org/alias/fonseca%2C-alcides"
  year: "2023"
  researchr: "https://researchr.org/publication/gamboausability"
  cites: 0
  citedby: 0
  kind: "article"
  key: "gamboausability"