@article(DBLP:journals/sosym/AhrendtBBBGHMMRSS05,
 author       = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H{\"{a}}hnle and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager and Peter H. Schmitt},
 year         = {2005},
 title        = {The {K}e{Y} tool},
 journal      = {Software and System Modeling},
 volume       = {4},
 number       = {1},
 pages        = {32--54},
 doi          = {10.1007/s10270-004-0058-x},
)
@inproceedings(DBLP:conf/vstte/AhrendtBBBGGHHHKMSSU14,
 author       = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and Christoph Gladisch and Sarah Grebing and Reiner H{\"{a}}hnle and Martin Hentschel and Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
 year         = {2014},
 title        = {The {KeY} Platform for Verification and Analysis of {Java} Programs},
 editor       = {Dimitra Giannakopoulou and Daniel Kroening},
 booktitle    = {Verified Software: Theories, Tools and Experiments - 6th International Conference, {VSTTE} 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers},
 series       = {LNCS},
 volume       = {8471},
 publisher    = {Springer},
 pages        = {55--71},
 doi          = {10.1007/978-3-319-12154-3_4},
)
@article(DBLP:journals/jsc/AitkenGMT98,
 author       = {J. Stuart Aitken and Philip D. Gray and Thomas F. Melham and Muffy Thomas},
 year         = {1998},
 title        = {Interactive Theorem Proving: An Empirical Study of User Activity},
 journal      = {J. Symb. Comput.},
 volume       = {25},
 number       = {2},
 pages        = {263--284},
 doi          = {10.1006/jsco.1997.0175},
)
@article(DBLP:journals/entcs/AspinallL04a,
 author       = {David Aspinall and Christoph L{\"{u}}th},
 year         = {2004},
 title        = {Proof General meets {IsaWin}: Combining Text-Based And Graphical User Interfaces},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {103},
 pages        = {3--26},
 doi          = {10.1016/j.entcs.2004.09.011},
)
@inproceedings(DBLP:conf/mkm/AspinallLW07,
 author       = {David Aspinall and Christoph L{\"{u}}th and Daniel Winterstein},
 year         = {2007},
 title        = {A Framework for Interactive Proof},
 editor       = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
 booktitle    = {Towards Mechanized Math. Assistants, 14th Symp., Calculemus, 6th Int. Conf., {MKM}, Hagenberg, Austria, June 27-30, 2007, Proc.},
 series       = {LNCS},
 volume       = {4573},
 publisher    = {Springer},
 pages        = {161--175},
 doi          = {10.1007/978-3-540-73086-6_15},
)
@inproceedings(DBLP:conf/cade/BeckertG12,
 author       = {Bernhard Beckert and Sarah Grebing},
 year         = {2012},
 title        = {Evaluating the Usability of Interactive Verification Systems},
 editor       = {Vladimir Klebanov and Bernhard Beckert and Armin Biere and Geoff Sutcliffe},
 booktitle    = {Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {873},
 publisher    = {CEUR-WS.org},
 pages        = {3--17},
)
@inproceedings(DBLP:conf/sefm/BeckertGB14,
 author       = {Bernhard Beckert and Sarah Grebing and Florian B{\"{o}}hl},
 year         = {2014},
 title        = {A Usability Evaluation of Interactive Theorem Provers Using Focus Groups},
 editor       = {Carlos Canal and Akram Idani},
 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},
 series       = {LNCS},
 volume       = {8938},
 publisher    = {Springer},
 pages        = {3--19},
 doi          = {10.1007/978-3-319-15201-1_1},
)
@inproceedings(DBLP:conf/ct/BlackwellBCGGKKLNPRRWY01,
 author       = {Alan F. Blackwell and Carol Britton and Anna Louise Cox and Thomas R. G. Green and Corin A. Gurr and Gada F. Kadoda and Maria Kutar and Martin Loomes and Chrystopher L. Nehaniv and Marian Petre and Chris Roast and Chris Roe and Allan Wong and R. Michael 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, 4th International Conference, {CT} 2001, Warwick, UK, August 6-9, 2001, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2117},
 publisher    = {Springer},
 pages        = {325--341},
 doi          = {10.1007/3-540-44617-6_31},
)
@article(DBLP:journals/jsc/DavenportH88,
 author       = {James H. Davenport and Joos Heintz},
 year         = {1988},
 title        = {Real Quantifier Elimination is Doubly Exponential},
 journal      = {J. Symb. Comput.},
 volume       = {5},
 number       = {1/2},
 pages        = {29--35},
 doi          = {10.1016/S0747-7171(88)80004-X},
)
@inproceedings(DBLP:conf/cav/FrehseGDCRLRGDM11,
 author       = {Goran Frehse and Colas Le Guernic and Alexandre Donz{\'{e}} and Scott Cotton and Rajarshi Ray and Olivier Lebeltel and Rodolfo Ripado and Antoine Girard and Thao Dang and Oded Maler},
 year         = {2011},
 title        = {{SpaceEx}: Scalable Verification of Hybrid Systems},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {{CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proc.},
 series       = {LNCS},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {379--395},
 doi          = {10.1007/978-3-642-22110-1_30},
)
@inproceedings(DBLP:conf/cade/FultonMQVP15,
 author       = {Nathan Fulton and Stefan Mitsch and Jan-David Quesel and Marcus V{\"o}lp and Andr{\'e} Platzer},
 year         = {2015},
 title        = {{KeYmaera X}: An Axiomatic Tactical Theorem Prover for Hybrid Systems},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {CADE},
 series       = {LNCS},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {527--538},
 doi          = {10.1007/978-3-319-21401-6_36},
)
@inproceedings(Kadoda1999,
 author       = {D. Diaper G. Kadoda, R. G. Stone},
 year         = {1999},
 title        = {Desirable features of educational theorem provers - a cognitive dimensions viewpoint},
 booktitle    = {11th Annual Workshop of Psychology of Programming Interest Group},
 organization = {PPIG},
 pages        = {1--6},
)
@inproceedings(DBLP:conf/kbse/0002HB16,
 author       = {Martin Hentschel and Reiner H{\"{a}}hnle and Richard Bubel},
 year         = {2016},
 title        = {An empirical evaluation of two user interfaces of an interactive program verifier},
 editor       = {Lo},
 pages        = {403--413},
 doi          = {10.1145/2970276.2970303},
)
@inproceedings(DBLP:conf/kbse/0002HB16a,
 author       = {Martin Hentschel and Reiner H{\"{a}}hnle and Richard Bubel},
 year         = {2016},
 title        = {The interactive verification debugger: effective understanding of interactive proof attempts},
 editor       = {Lo},
 pages        = {846--851},
 doi          = {10.1145/2970276},
)
@misc(Jackson1997,
 author       = {Michael J. Jackson},
 year         = {1997},
 title        = {Evaluation of a Semi-Automated Theorem Prover (Part II)},
)
@inproceedings(DBLP:conf/cav/KovacsV13,
 author       = {Laura Kov{\'{a}}cs and Andrei Voronkov},
 year         = {2013},
 title        = {First-Order Theorem Proving and {Vampire}},
 editor       = {Natasha Sharygina and Helmut Veith},
 booktitle    = {Computer Aided Verification - 25th Int. Conf., {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proc.},
 series       = {LNCS},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {1--35},
 doi          = {10.1007/978-3-642-39799-8_1},
)
@inproceedings(DBLP:conf/icse/Leino04,
 author       = {K. Rustan M. Leino},
 year         = {2013},
 title        = {Developing verified programs with {Dafny}},
 editor       = {David Notkin and Betty H. C. Cheng and Klaus Pohl},
 booktitle    = {35th Int. Conf. on Software Engineering, {ICSE} '13, San Francisco, CA, USA, May 18-26, 2013},
 publisher    = {{IEEE} Computer Soc.},
 pages        = {1488--1490},
 doi          = {10.1109/ICSE.2013.6606754},
)
@inproceedings(DBLP:journals/corr/LeinoW14,
 author       = {K. Rustan M. Leino and Valentin W{\"{u}}stholz},
 year         = {2014},
 title        = {The {Dafny} Integrated Development Environment},
 editor       = {Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
 booktitle    = {Proceedings 1st Workshop on Formal Integrated Development Environment, {F-IDE} 2014, Grenoble, France, April 6, 2014.},
 series       = {{EPTCS}},
 volume       = {149},
 pages        = {3--15},
 doi          = {10.4204/EPTCS.149.2},
)
@proceedings(DBLP:conf/kbse/2016,
 editor       = {David Lo and Sven Apel and Sarfraz Khurshid},
 year         = {2016},
 title        = {Proceedings of the 31st {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2016, Singapore, September 3-7, 2016},
 publisher    = {{ACM}},
 doi          = {10.1145/2970276},
)
@manual(Coq:manual,
 author       = {\unhbox\voidb@x \hbox{The Coq development team}},
 year         = {2015},
 title        = {The Coq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.5},
)
@inproceedings(DBLP:conf/types/Nipkow02,
 author       = {Tobias Nipkow},
 year         = {2002},
 title        = {Structured Proofs in {Isar/HOL}},
 editor       = {Herman Geuvers and Freek Wiedijk},
 booktitle    = {Types for Proofs and Programs, 2nd Int. Workshop, {TYPES} 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers},
 series       = {LNCS},
 volume       = {2646},
 publisher    = {Springer},
 pages        = {259--278},
 doi          = {10.1007/3-540-39185-1_15},
)
@book(DBLP:books/sp/NipkowPW02,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {LNCS},
 volume       = {2283},
 publisher    = {Springer},
)
@article(DBLP:journals/jar/Platzer08,
 author       = {Andr{\'e} Platzer},
 year         = {2008},
 title        = {Differential Dynamic Logic for Hybrid Systems.},
 journal      = {J. Autom. Reas.},
 volume       = {41},
 number       = {2},
 pages        = {143--189},
 doi          = {10.1007/s10817-008-9103-8},
)
@inproceedings(DBLP:conf/lics/Platzer12a,
 author       = {Andr{\'e} Platzer},
 year         = {2012},
 title        = {Logics of Dynamical Systems},
 booktitle    = {LICS},
 publisher    = {IEEE},
 pages        = {13--24},
 doi          = {10.1109/LICS.2012.13},
)
@inproceedings(DBLP:conf/cpsed/Platzer13,
 author       = {Andr{\'e} Platzer},
 year         = {2013},
 title        = {Teaching {CPS} Foundations With Contracts},
 booktitle    = {CPS-Ed},
 pages        = {7--10},
)
@inproceedings(DBLP:conf/cade/Platzer15,
 author       = {Andr{\'{e}} Platzer},
 year         = {2015},
 title        = {A Uniform Substitution Calculus for Differential Dynamic Logic},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {CADE},
 series       = {LNCS},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {467--481},
 doi          = {10.1007/978-3-319-21401-6_32},
)
@article(DBLP:journals/jar/Platzer16,
 author       = {Andr{\'e} Platzer},
 year         = {2016},
 title        = {A Complete Uniform Substitution Calculus for Differential Dynamic Logic},
 journal      = {J. Autom. Reas.},
 doi          = {10.1007/s10817-016-9385-1},
)
@inproceedings(DBLP:conf/cade/PlatzerQ08,
 author       = {Andr{\'{e}} Platzer and Jan{-}David Quesel},
 year         = {2008},
 title        = {{KeYmaera}: {A} Hybrid Theorem Prover for Hybrid Systems (System Description)},
 editor       = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
 booktitle    = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008, Sydney, Australia, August 12-15, 2008, Proc.},
 series       = {LNCS},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {171--178},
 doi          = {10.1007/978-3-540-71070-7_15},
)
@article(DBLP:journals/sttt/QueselMLAP16,
 author       = {Jan{-}David Quesel and Stefan Mitsch and Sarah M. Loos and Nikos Arechiga and Andr{\'{e}} Platzer},
 year         = {2016},
 title        = {How to model and prove hybrid systems with {KeYmaera}: a tutorial on safety},
 journal      = {{STTT}},
 volume       = {18},
 number       = {1},
 pages        = {67--91},
 doi          = {10.1007/s10009-015-0367-0},
)
@inproceedings(DBLP:conf/tacas/TschannenFNP15,
 author       = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova},
 year         = {2015},
 title        = {AutoProof: Auto-Active Functional Verification of Object-Oriented Programs},
 editor       = {Christel Baier and Cesare Tinelli},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, {TACAS} 2015, London, UK, April 11-18, 2015. Proceedings},
 series       = {LNCS},
 volume       = {9035},
 publisher    = {Springer},
 pages        = {566--580},
 doi          = {10.1007/978-3-662-46681-0},
)
@inproceedings(DBLP:conf/aisc/Wenzel12,
 author       = {Makarius Wenzel},
 year         = {2012},
 title        = {{Isabelle}/{jEdit} - {A} Prover {IDE} within the {PIDE} Framework},
 editor       = {Johan Jeuring and John A. Campbell and Jacques Carette and Gabriel Dos Reis and Petr Sojka and Makarius Wenzel and Volker Sorge},
 booktitle    = {Intelligent Computer Mathematics - 11th International Conference, {AISC} 2012, 19th Symp., Calculemus 2012, 5th Int. Workshop, {DML} 2012, 11th Int. Conf., {MKM} 2012, Systems and Projects, Held as Part of {CICM} 2012, Bremen, Germany, July 8-13, 2012. Proc.},
 series       = {LNCS},
 volume       = {7362},
 publisher    = {Springer},
 pages        = {468--471},
 doi          = {10.1007/978-3-642-31374-5},
)
@book(DBLP:books/daglib/0029933,
 author       = {Claes Wohlin and Per Runeson and Martin H{\"{o}}st and Magnus C. Ohlsson and Bj{\"{o}}rn Regnell},
 year         = {2012},
 title        = {Experimentation in Software Engineering},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-29044-2},
)