@misc(leftover,
 note         = {\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\topsep 6\p@ plus2\p@ minus2\p@ \parsep3\p@ plus2\p@ minus\p@ \itemsep\parsep {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip \url{https://www.kitchensoap.com/2012/09/21/a-mature-role-for-automation-part-i/} and \url{https://www.kitchensoap.com/2013/08/20/a-mature-role-for-automation-part-ii/}},
)
@misc(leftover2,
 note         = {\relax\fontsize {9}{11}\selectfont\abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip\z@ plus\p@ \belowdisplayshortskip4\p@ plus2\p@ minus2\p@ \def\leftmargin \leftmargini\topsep 6\p@ plus2\p@ minus2\p@ \parsep3\p@ plus2\p@ minus\p@ \itemsep\parsep {\leftmargin\leftmargini \topsep4\p@ plus2\p@ minus2\p@ \parsep2\p@ plus\p@ minus\p@ \itemsep\parsep }\belowdisplayskip\abovedisplayskip \url{https://queue.acm.org/detail.cfm?id=2841313}},
)
@inproceedings(comperr,
 author       = {Brett A. Becker and Paul Denny and Raymond Pettit and Durell Bouchard and Dennis J. Bouvier and Brian Harrington and Amir Kamil and Amey Karkare and Chris McDonald and Peter-Michael Osera and Janice L. Pearce and James Prather},
 year         = {2019},
 title        = {Compiler Error Messages Considered Unhelpful: The Landscape of Text-Based Programming Error Message Research},
 booktitle    = {Proceedings of the Working Group Reports on Innovation and Technology in Computer Science Education},
 series       = {ITiCSE-WGR '19},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {177\IeC{\textendash}210},
 doi          = {10.1145/3344429.3372508},
)
@inproceedings(cognitive,
 author       = {A. F. Blackwell and C. Britton and A. Cox and T. R. G. Green and C. Gurr and G. Kadoda and M. S. Kutar and M. Loomes and C. L. Nehaniv and M. Petre and C. Roast and C. Roe and A. Wong and R. M. Young},
 year         = {2001},
 title        = {Cognitive Dimensions of Notations: Design Tools for Cognitive Technology},
 editor       = {Meurig Beynon and Chrystopher L. Nehaniv and Kerstin Dautenhahn},
 booktitle    = {Cognitive Technology: Instruments of Mind},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {325--341},
 doi          = {10.1007/3-540-44617-6\_31},
)
@inproceedings(christakis16tacas,
 author       = {Maria Christakis and K. Rustan M. Leino and Peter M{\"u}ller and Valentin W{\"u}stholz},
 year         = {2016},
 title        = {Integrated Environment for Diagnosing Verification Errors},
 booktitle    = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)},
 pages        = {424--441},
 doi          = {10.1007/978-3-662-49674-9\_25},
)
@article(Cok2010,
 author       = {David R. Cok},
 year         = {2010},
 title        = {Improved usability and performance of {SMT} solvers for debugging specifications},
 journal      = {Int. Journal on Software Tools for Technology Transfer},
 volume       = {12},
 number       = {6},
 pages        = {467--481},
 doi          = {10.1007/s10009-010-0138-x},
)
@article(dailler:hal-01802488,
 author       = {Sylvain Dailler and David Hauzar and Claude March{\'e} and Yannick Moy},
 year         = {2018},
 title        = {{Instrumenting a Weakest Precondition Calculus for Counterexample Generation}},
 journal      = {{Journal of Logical and Algebraic Methods in Programming}},
 volume       = {99},
 pages        = {97--113},
 doi          = {10.1016/j.jlamp.2018.05.003},
 url          = {https://hal.inria.fr/hal-01802488},
)
@inproceedings(dailler:hal-01936302,
 author       = {Sylvain Dailler and Claude March{\'e} and Yannick Moy},
 year         = {2018},
 title        = {{Lightweight Interactive Proving inside an Automatic Program Verifier}},
 editor       = {Paolo Masci and Rosemary Monahan and Virgile Prevosto},
 booktitle    = {{4th Workshop on Formal Integrated Development Environment}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {284},
 publisher    = {{Open Publishing Association}},
 address      = {Oxford, United Kingdom},
 doi          = {10.4204/EPTCS.284.1},
 url          = {https://hal.inria.fr/hal-01936302},
)
@inbook(Hentschel2016,
 author       = {Martin Hentschel and Reiner H{\"a}hnle and Richard Bubel},
 year         = {2016},
 title        = {Deductive Software Verification --- The KeY Book},
 chapter      = {Debugging and Visualization},
 pages        = {383--413},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-49812-6_11},
)
@inproceedings(jacobs11nfm,
 author       = {Bart Jacobs and Jan Smans and Pieter Philippaerts and Fr\IeC{\'e}d\IeC{\'e}ric Vogels and Willem Penninckx and Frank Piessens},
 year         = {2011},
 title        = {{VeriFast}: A Powerful, Sound, Predictable, Fast Verifier for {C} and {Java}},
 editor       = {Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi},
 booktitle    = {NASA Formal Methods},
 volume       = {6617},
 pages        = {41--55},
 doi          = {10.1007/978-3-642-20398-5\_4},
)
@article(tenchallenges,
 author       = {G. {Klien} and D. D. {Woods} and J. M. {Bradshaw} and R. R. {Hoffman} and P. J. {Feltovich}},
 year         = {2004},
 title        = {Ten challenges for making automation a "team player" in joint human-agent activity},
 journal      = {IEEE Intelligent Systems},
 volume       = {19},
 number       = {6},
 pages        = {91--95},
 doi          = {10.1109/MIS.2004.74},
)
@inproceedings(goues11sefm,
 author       = {{Le Goues}, Claire and K. Rustan M. Leino and Michal Moskal},
 year         = {2011},
 title        = {The {Boogie} {V}erification {D}ebugger},
 editor       = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
 booktitle    = {Software Engineering and Formal Methods - 9th International Conference, (SEFM)},
 volume       = {7041},
 pages        = {407--414},
 doi          = {10.1007/978-3-642-24690-6\_28},
)
@inproceedings(muller11fm,
 author       = {Peter M{\"{u}}ller and Joseph N. Ruskiewicz},
 year         = {2011},
 title        = {Using Debuggers to Understand Failed Verification Attempts},
 editor       = {Michael J. Butler and Wolfram Schulte},
 booktitle    = {17th International Symposium on Formal Methods},
 volume       = {6664},
 pages        = {73--87},
 doi          = {10.1007/978-3-642-21437-0\_8},
)
@inproceedings(petiot16tap,
 author       = {Guillaume Petiot and Nikolai Kosmatov and Bernard Botella and Alain Giorgetti and Jacques Julliand},
 year         = {2016},
 title        = {Your Proof Fails? Testing Helps to Find the Reason},
 booktitle    = {Tests and Proofs - 10th International Conference},
 volume       = {9762},
 pages        = {130--150},
 doi          = {10.1007/978-3-319-41135-4\_8},
)