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