% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/usability-of-verification-tools/compact

@inproceedings{SwamyHKRDFBFSKZ16,
  title = {Dependent types and multi-monadic effects in F*},
  author = {Nikhil Swamy and Catalin Hritcu and Chantal Keller and Aseem Rastogi and Antoine Delignat-Lavaud and Simon Forest and Karthikeyan Bhargavan and Cédric Fournet and Pierre-Yves Strub and Markulf Kohlweiss and Jean Karim Zinzindohoue and Santiago Zanella Béguelin},
  year = {2016},
  doi = {10.1145/2837614.2837655},
  url = {http://doi.acm.org/10.1145/2837614.2837655},
  researchr = {https://researchr.org/publication/SwamyHKRDFBFSKZ16},
  cites = {0},
  citedby = {0},
  pages = {256-270},
  booktitle = {POPL},
}

@book{lncs-12345,
  title = {Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY},
  year = {2020},
  doi = {10.1007/978-3-030-64354-6},
  url = {https://doi.org/10.1007/978-3-030-64354-6},
  researchr = {https://researchr.org/publication/lncs-12345},
  cites = {0},
  citedby = {0},
  editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner Hähnle and Mattias Ulbrich},
  volume = {12345},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-64354-6},
}

@inproceedings{MerriamH96,
  title = {Evaluating the Interfaces of Three Theorem Proving Assistants},
  author = {Nicholas A. Merriam and Michael D. Harrison},
  year = {1996},
  researchr = {https://researchr.org/publication/MerriamH96},
  cites = {0},
  citedby = {0},
  pages = {330-346},
  booktitle = {DSVIS},
}

@inproceedings{0002HB16a,
  title = {The interactive verification debugger: effective understanding of interactive proof attempts},
  author = {Martin Hentschel 0002 and Reiner Hähnle and Richard Bubel},
  year = {2016},
  doi = {10.1145/2970276.2970292},
  url = {http://doi.acm.org/10.1145/2970276.2970292},
  tags = {KeyMaera},
  researchr = {https://researchr.org/publication/0002HB16a},
  cites = {0},
  citedby = {0},
  pages = {846-851},
  booktitle = {ASE},
}

@article{Souaf2021,
  title = {Experience Report: Teaching Code Analysis and Verification Using Frama-C},
  author = {Salwa Souaf and Frédéric Loulergue},
  year = {2021},
  month = {nov},
  doi = {10.4204/eptcs.349.5},
  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},
}

@inproceedings{GriffioenH98,
  title = {A Comparison of PVS and Isabelle/HOL},
  author = {W. O. David Griffioen and Marieke Huisman},
  year = {1998},
  researchr = {https://researchr.org/publication/GriffioenH98},
  cites = {0},
  citedby = {0},
  pages = {123-142},
  booktitle = {tphol},
}

@inproceedings{BeckertG15,
  title = {Interactive Theorem Proving - Modelling the User in the Proof Process},
  author = {Bernhard Beckert and Sarah Grebing},
  year = {2015},
  url = {http://ceur-ws.org/Vol-1412/6o.pdf},
  tags = {KeyMaera},
  researchr = {https://researchr.org/publication/BeckertG15},
  cites = {0},
  citedby = {0},
  pages = {60-73},
  booktitle = {cade},
}

@inproceedings{HeerenLI03,
  title = {Helium, for learning Haskell},
  author = {Bastiaan Heeren and Daan Leijen and Arjan van IJzendoorn},
  year = {2003},
  doi = {10.1145/871895.871902},
  url = {http://doi.acm.org/10.1145/871895.871902},
  tags = {error-reporting},
  researchr = {https://researchr.org/publication/HeerenLI03},
  cites = {0},
  citedby = {0},
  pages = {62-71},
  booktitle = {haskell},
}

@inproceedings{NobleSGS22,
  title = {More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme},
  author = {James Noble 0001 and David Streader and Isaac Oscar Gariano and Miniruwani Samarakoon},
  year = {2022},
  doi = {10.1007/978-3-031-06773-0_23},
  url = {https://doi.org/10.1007/978-3-031-06773-0_23},
  researchr = {https://researchr.org/publication/NobleSGS22},
  cites = {0},
  citedby = {0},
  pages = {431-450},
  booktitle = {NFM},
}

@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},
}

@inproceedings{Leino10-2,
  title = {Dafny: An Automatic Program Verifier for Functional Correctness},
  author = {K. Rustan M. Leino},
  year = {2010},
  doi = {10.1007/978-3-642-17511-4_20},
  url = {http://dx.doi.org/10.1007/978-3-642-17511-4_20},
  tags = {program verification, functional programming},
  researchr = {https://researchr.org/publication/Leino10-2},
  cites = {0},
  citedby = {0},
  pages = {348-370},
  booktitle = {lpar},
}

@inproceedings{RingerSGL20,
  title = {REPLica: REPL instrumentation for Coq analysis},
  author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner},
  year = {2020},
  doi = {10.1145/3372885.3373823},
  url = {https://doi.org/10.1145/3372885.3373823},
  researchr = {https://researchr.org/publication/RingerSGL20},
  cites = {0},
  citedby = {0},
  pages = {99-113},
  booktitle = {CPP},
}

@inproceedings{BeckertGB14,
  title = {A Usability Evaluation of Interactive Theorem Provers Using Focus Groups},
  author = {Bernhard Beckert and Sarah Grebing and Florian Böhl},
  year = {2014},
  doi = {10.1007/978-3-319-15201-1_1},
  url = {http://dx.doi.org/10.1007/978-3-319-15201-1_1},
  researchr = {https://researchr.org/publication/BeckertGB14},
  cites = {0},
  citedby = {0},
  pages = {3-19},
  booktitle = {SEFM},
}

@inproceedings{FigueroaGL18,
  title = {Towards progressive program verification in Dafny},
  author = {Ismael Figueroa and Bruno García and Paul Leger},
  year = {2018},
  doi = {10.1145/3264637.3264649},
  url = {https://doi.org/10.1145/3264637.3264649},
  researchr = {https://researchr.org/publication/FigueroaGL18},
  cites = {0},
  citedby = {0},
  pages = {90-97},
  booktitle = {SBLP},
}

@inproceedings{FilliatreP13,
  title = {Why3 - Where Programs Meet Provers},
  author = {Jean-Christophe Filliâtre and  Andrei Paskevich},
  year = {2013},
  doi = {10.1007/978-3-642-37036-6_8},
  url = {http://dx.doi.org/10.1007/978-3-642-37036-6_8},
  researchr = {https://researchr.org/publication/FilliatreP13},
  cites = {0},
  citedby = {0},
  pages = {125-128},
  booktitle = {ESOP},
}

@inproceedings{Eilers018,
  title = {Nagini: A Static Verifier for Python},
  author = {Marco Eilers and Peter Müller 0001},
  year = {2018},
  doi = {10.1007/978-3-319-96145-3_33},
  url = {https://doi.org/10.1007/978-3-319-96145-3_33},
  researchr = {https://researchr.org/publication/Eilers018},
  cites = {0},
  citedby = {0},
  pages = {596-603},
  booktitle = {cav},
}

@inproceedings{KadodaSD99,
  title = {Desirable features of educational theorem provers - a cognitive dimensions viewpoint},
  author = {Gada F. Kadoda and Roger G. Stone and Dan Diaper},
  year = {1999},
  url = {http://ppig.org/library/paper/desirable-features-educational-theorem-provers-cognitive-dimensions-viewpoint},
  researchr = {https://researchr.org/publication/KadodaSD99},
  cites = {0},
  citedby = {0},
  pages = {4},
  booktitle = {PPIG},
}

@inproceedings{BeckertG12,
  title = {Evaluating the Usability of Interactive Verification Systems},
  author = {Bernhard Beckert and Sarah Grebing},
  year = {2012},
  url = {http://ceur-ws.org/Vol-873/papers/paper_4.pdf},
  tags = {KeyMaera},
  researchr = {https://researchr.org/publication/BeckertG12},
  cites = {0},
  citedby = {0},
  pages = {3-17},
  booktitle = {cade},
}

@inproceedings{DuboisPB99,
  title = {Teaching Formal Methods to Future Engineers},
  author = {Catherine Dubois and Virgile Prevosto and Guillaume Burel},
  year = {2019},
  doi = {10.1007/978-3-030-32441-4_5},
  url = {https://doi.org/10.1007/978-3-030-32441-4_5},
  researchr = {https://researchr.org/publication/DuboisPB99},
  cites = {0},
  citedby = {0},
  pages = {69-80},
  booktitle = {tfm},
}

@phdthesis{dnb-250,
  title = {Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study},
  author = {Thorsten Bormer},
  year = {2014},
  url = {http://d-nb.info/1077821883},
  tags = {VCC},
  researchr = {https://researchr.org/publication/dnb-250},
  cites = {0},
  citedby = {0},
  school = {Karlsruhe Institute of Technology},
}

@inproceedings{0002HB16-0,
  title = {An empirical evaluation of two user interfaces of an interactive program verifier},
  author = {Martin Hentschel 0002 and Reiner Hähnle and Richard Bubel},
  year = {2016},
  doi = {10.1145/2970276.2970303},
  url = {http://doi.acm.org/10.1145/2970276.2970303},
  researchr = {https://researchr.org/publication/0002HB16-0},
  cites = {0},
  citedby = {0},
  pages = {403-413},
  booktitle = {ASE},
}

@article{AitkenM00,
  title = {An analysis of errors in interactive proof attempts},
  author = {J. Stuart Aitken and 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},
}

@inproceedings{GrebingKU19,
  title = {Seamless Interactive Program Verification},
  author = {Sarah Grebing and Jonas Klamroth and Mattias Ulbrich},
  year = {2019},
  doi = {10.1007/978-3-030-41600-3_6},
  url = {https://doi.org/10.1007/978-3-030-41600-3_6},
  researchr = {https://researchr.org/publication/GrebingKU19},
  cites = {0},
  citedby = {0},
  pages = {68-86},
  booktitle = {vstte},
}

@article{AitkenGMT98,
  title = {Interactive Theorem Proving: An Empirical Study of User Activity},
  author = {J. Stuart Aitken and Philip D. Gray and Thomas F. Melham and 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},
}

@inproceedings{Blazy99,
  title = {Teaching Deductive Verification in Why3 to Undergraduate Students},
  author = {Sandrine Blazy},
  year = {2019},
  doi = {10.1007/978-3-030-32441-4_4},
  url = {https://doi.org/10.1007/978-3-030-32441-4_4},
  researchr = {https://researchr.org/publication/Blazy99},
  cites = {0},
  citedby = {0},
  pages = {52-66},
  booktitle = {tfm},
}

@inproceedings{Merriam1998MakingDD,
  title = {Making Design Decisions to Support Diversity in Interactive Theorem Proving},
  author = {Nicholas A. Merriam and Michael D. Harrison and Michael D. Harrison},
  year = {1998},
  url = {https://api.semanticscholar.org/CorpusID:16809476},
  researchr = {https://researchr.org/publication/Merriam1998MakingDD},
  cites = {0},
  citedby = {0},
}

@incollection{Dahl1977,
  title = {Can program proving be made practical?},
  author = {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},
}

@article{10.1145-3593374,
  title = {Passport: Improving Automated Formal Verification Using Identifiers},
  author = {Sanchez-Stern, Alex and First, Emily and Zhou, Timothy and Kaufman, Zhanna and Brun, Yuriy and Ringer, Talia},
  year = {2023},
  month = {jun},
  doi = {10.1145/3593374},
  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},
}

@incollection{GrebingU20,
  title = {Usability Recommendations for User Guidance in Deductive Program Verification},
  author = {Sarah Grebing and Mattias Ulbrich},
  year = {2020},
  doi = {10.1007/978-3-030-64354-6_11},
  url = {https://doi.org/10.1007/978-3-030-64354-6_11},
  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 = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner Hähnle and Mattias Ulbrich},
  volume = {12345},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-64354-6},
}

@incollection{HahnleH19,
  title = {Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools},
  author = {Reiner Hähnle and Marieke Huisman},
  year = {2019},
  doi = {10.1007/978-3-319-91908-9_18},
  url = {https://doi.org/10.1007/978-3-319-91908-9_18},
  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},
}

@article{Volker04,
  title = {Thoughts on Requirements and Design Issues of User Interfaces for Proof Assistants},
  author = {Norbert Völker},
  year = {2004},
  doi = {10.1016/j.entcs.2004.05.001},
  url = {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},
}

@mastersthesis{Juhoov2023,
  title = {Bringing Formal Verification into Widespread Programming Language Ecosystems},
  author = {Sára Juhošová},
  year = {2023},
  researchr = {https://researchr.org/publication/Juhoov2023},
  cites = {0},
  citedby = {0},
  school = {TU Delft},
}

@article{gamboausability,
  title = {Usability-Oriented Design of Liquid Types for Java},
  author = {Gamboa, Catarina and Santos, Paulo and Timperley, Christopher Steven and Fonseca, Alcides},
  year = {2023},
  researchr = {https://researchr.org/publication/gamboausability},
  cites = {0},
  citedby = {0},
}