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: "POPL"
  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: "DSVIS"
  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: "ASE"
  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: "tphol"
  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: "cade"
  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: "haskell"
  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: "NFM"
  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: "dt"
  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: "lpar"
  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: "CPP"
  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: "SEFM"
  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: "SBLP"
  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: "ESOP"
  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: "cav"
  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: "PPIG"
  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: "cade"
  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: "tfm"
  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: "ASE"
  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: "iwc"
  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: "vstte"
  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: "JSC"
  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: "tfm"
  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: "ENTCS"
  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"