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

@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 = {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 = {Rastislav Bodik and Rupak Majumdar},
  publisher = {ACM},
  isbn = {978-1-4503-3549-2},
}

@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 = {Design, Specification and Verification of Interactive Systems 96, Proceedings of the Third International Eurographics Workshop, June 5-7, 1996, Namur, Belgium},
  editor = {François Bodart and Jean Vanderdonckt},
  publisher = {Springer},
  isbn = {3-211-82900-8},
}

@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 = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
  editor = {David Lo and Sven Apel and Sarfraz Khurshid},
  publisher = {ACM},
  isbn = {978-1-4503-3845-5},
}

@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 = {Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs 98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
  editor = {Jim Grundy and Malcolm C. Newey},
  volume = {1479},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-64987-5},
}

@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 = {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 = {Ulrich Furbach and Claudia Schon},
  volume = {1412},
  series = {CEUR Workshop Proceedings},
  publisher = {CEUR-WS.org},
}

@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 = {Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2003, Uppsala, Sweden, August 28, 2003},
  publisher = {ACM},
}

@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 = {NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings},
  editor = {Jyotirmoy V. Deshmukh and Klaus Havelund and Ivan Perez 0001},
  volume = {13260},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-031-06773-0},
}

@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 = {IEEE Design & Test of Computers},
  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 = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers},
  editor = {Edmund M. Clarke and Andrei Voronkov},
  volume = {6355},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-17510-7},
}

@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 = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020},
  editor = {Jasmin Blanchette and Catalin Hritcu},
  publisher = {ACM},
  isbn = {978-1-4503-7097-4},
}

@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 = {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 = {Carlos Canal and Akram Idani},
  volume = {8938},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-15200-4},
}

@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 = {Proceedings of the XXII Brazilian Symposium on Programming Languages, SBLP 2018, Sao Carlos, Brazil, September 20-21, 2018},
  editor = {Carlos Camarão and Martin Sulzmann},
  publisher = {ACM},
  isbn = {978-1-4503-6480-5},
}

@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 = {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 = {Matthias Felleisen and Philippa Gardner},
  volume = {7792},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-37035-9},
}

@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 = {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 = {Hana Chockler and Georg Weissenbacher},
  volume = {10981},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-96145-3},
}

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

@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 = {Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012},
  editor = {Vladimir Klebanov and Bernhard Beckert and Armin Biere and Geoff Sutcliffe},
  volume = {873},
  series = {CEUR Workshop Proceedings},
  publisher = {CEUR-WS.org},
}

@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 = {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 = {Brijesh Dongol and Luigia Petre and Graeme Smith},
  volume = {11758},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-32441-4},
}

@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 = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
  editor = {David Lo and Sven Apel and Sarfraz Khurshid},
  publisher = {ACM},
  isbn = {978-1-4503-3845-5},
}

@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 = {Interacting with Computers},
  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 = {Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers},
  editor = {Supratik Chakraborty and Jorge A. Navas},
  volume = {12031},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-41600-3},
}

@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 = {Journal of Symbolic Computation},
  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 = {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 = {Brijesh Dongol and Luigia Petre and Graeme Smith},
  volume = {11758},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-030-32441-4},
}

@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 = {Electronic Notes in Theoretical Computer Science},
  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},
}