@article(KeY2005,
 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 {KeY} Tool},
 journal      = {Software and System Modeling},
 volume       = {4},
 number       = {1},
 pages        = {32--54},
 doi          = {10.1007/s10270-004-0058-x},
)
@book(DBLP:series/txtcs/BertotC04,
 author       = {Yves Bertot and Pierre Cast{\'{e}}ran},
 year         = {2004},
 title        = {Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions},
 series       = {Texts in Theoretical Computer Science. An {EATCS} Series},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-07964-5},
)
@inproceedings(DBLP:conf/pldi/BohrerTMMP18,
 author       = {Brandon Bohrer and Yong Kiam Tan and Stefan Mitsch and Magnus O. Myreen and Andr{\'{e}} Platzer},
 year         = {2018},
 title        = {{VeriPhy}: Verified Controller Executables from Verified Cyber-Physical System Models},
 editor       = {Dan Grossman},
 booktitle    = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2018},
 publisher    = {{ACM}},
 pages        = {617--630},
 doi          = {10.1145/3192366.3192406},
)
@inproceedings(DBLP:conf/itp/FultonMBP17,
 author       = {Nathan Fulton and Stefan Mitsch and Brandon Bohrer and Andr{\'{e}} Platzer},
 year         = {2017},
 title        = {Bellerophon: Tactical Theorem Proving for Hybrid Systems},
 editor       = {Ayala{-}Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.},
 booktitle    = {ITP},
 series       = {LNCS},
 volume       = {10499},
 publisher    = {Springer},
 pages        = {207--224},
 doi          = {10.1007/978-3-319-66107-0_14},
)
@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 Felty and Aart Middeldorp},
 booktitle    = {CADE},
 series       = {LNCS},
 volume       = {9195},
 publisher    = {Springer},
 address      = {Berlin},
 pages        = {527--538},
 doi          = {10.1007/978-3-319-21401-6_36},
)
@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},
)
@inproceedings(DBLP:conf/emsoft/LiuZZ11,
 author       = {Jiang Liu and Naijun Zhan and Hengjun Zhao},
 year         = {2011},
 title        = {Computing semi-algebraic invariants for polynomial dynamical systems},
 editor       = {Samarjit Chakraborty and Ahmed Jerraya and Sanjoy K. Baruah and Sebastian Fischmeister},
 booktitle    = {Proceedings of the 11th International Conference on Embedded Software, {EMSOFT} 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011},
 publisher    = {{ACM}},
 pages        = {97--106},
 doi          = {10.1145/2038642.2038659},
)
@inproceedings(DBLP:conf/fide/MitschP16,
 author       = {Stefan Mitsch and Andr{\'{e}} Platzer},
 year         = {2016},
 title        = {The {KeYmaera X} proof {IDE}: Concepts on usability in hybrid systems theorem proving},
 editor       = {Catherine Dubois and Paolo Masci and Dominique M{\'{e}}ry},
 booktitle    = {3rd Workshop on Formal Integrated Development Environment},
 series       = {EPTCS},
 volume       = {240},
 pages        = {67--81},
 doi          = {10.4204/EPTCS.240.5},
)
@article(DBLP:journals/fmsd/MitschP16,
 author       = {Stefan Mitsch and Andr{\'{e}} Platzer},
 year         = {2016},
 title        = {{ModelPlex}: Verified Runtime Validation of Verified Cyber-Physical System Models},
 journal      = {Form. Methods Syst. Des.},
 volume       = {49},
 number       = {1-2},
 pages        = {33--74},
 doi          = {10.1007/s10703-016-0241-z},
 note         = {Special issue of selected papers from RV'14},
)
@incollection(DBLP:series/lncs/MitschP20,
 author       = {Stefan Mitsch and Andr{\'{e}} Platzer},
 year         = {2020},
 title        = {A Retrospective on Developing Hybrid Systems Provers in the {KeYmaera} Family - {A} Tale of Three Provers},
 editor       = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Matthias Ulbrich},
 booktitle    = {Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of {KeY}},
 series       = {LNCS},
 volume       = {12345},
 publisher    = {Springer},
 pages        = {21--64},
 doi          = {10.1007/978-3-030-64354-6_2},
)
@article(DBLP:journals/sttt/MullerMRSP18,
 author       = {Andreas M{\"{u}}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'{e}} Platzer},
 year         = {2018},
 title        = {Tactical Contract Composition for Hybrid System Component Verification},
 journal      = {STTT},
 volume       = {20},
 number       = {6},
 pages        = {615--643},
 doi          = {10.1007/s10009-018-0502-9},
 note         = {Special issue for selected papers from FASE'17},
)
@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},
 doi          = {10.1007/3-540-45949-9},
)
@inproceedings(DBLP:conf/cade/Paulson10,
 author       = {Lawrence C. Paulson},
 year         = {2010},
 title        = {Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers},
 editor       = {Renate A. Schmidt and Stephan Schulz and Boris Konev},
 booktitle    = {Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010},
 series       = {EPiC Series},
 volume       = {9},
 publisher    = {EasyChair},
 pages        = {1--10},
 doi          = {10.29007/36dt},
)
@article(DBLP:journals/jar/Platzer17,
 author       = {Andr{\'{e}} Platzer},
 year         = {2017},
 title        = {A Complete Uniform Substitution Calculus for Differential Dynamic Logic},
 journal      = {J. Autom. Reas.},
 volume       = {59},
 number       = {2},
 pages        = {219--265},
 doi          = {10.1007/s10817-016-9385-1},
)
@book(Platzer18,
 author       = {Andr{\'{e}} Platzer},
 year         = {2018},
 title        = {Logical Foundations of Cyber-Physical Systems},
 publisher    = {Springer},
 address      = {Cham},
 doi          = {10.1007/978-3-319-63588-0},
)
@inproceedings(DBLP:conf/cade/PlatzerQ08,
 author       = {Andr{\'{e}} Platzer and Jan-David Quesel},
 year         = {2008},
 title        = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
 editor       = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
 booktitle    = {IJCAR},
 series       = {LNCS},
 volume       = {5195},
 publisher    = {Springer},
 address      = {Berlin},
 pages        = {171--178},
 doi          = {10.1007/978-3-540-71070-7_15},
)
@article(DBLP:journals/jacm/PlatzerT20,
 author       = {Andr{\'{e}} Platzer and Yong Kiam Tan},
 year         = {2020},
 title        = {Differential Equation Invariance Axiomatization},
 journal      = {J. ACM},
 volume       = {67},
 number       = {1},
 pages        = {6:1--6:66},
 doi          = {10.1145/3380825},
)
@inproceedings(DBLP:conf/icfem/RenshawLP11,
 author       = {David W. Renshaw and Sarah M. Loos and Andr{\'{e}} Platzer},
 year         = {2011},
 title        = {Distributed Theorem Proving for Distributed Hybrid Systems},
 editor       = {Shengchao Qin and Zongyan Qiu},
 booktitle    = {ICFEM},
 series       = {LNCS},
 volume       = {6991},
 publisher    = {Springer},
 pages        = {356--371},
 doi          = {10.1007/978-3-642-24559-6_25},
)
@article(DBLP:journals/fmsd/SogokonMTCP,
 author       = {Andrew Sogokon and Stefan Mitsch and Yong Kiam Tan and Katherine Cordwell and Andr{\'{e}} Platzer},
 year         = {2021},
 title        = {Pegasus: Sound Continuous Invariant Generation},
 journal      = {Form. Methods Syst. Des.},
 doi          = {10.1007/s10703-020-00355-z},
 note         = {Special issue for selected papers from FM'19},
)
@inproceedings(DBLP:conf/tacas/TanP21,
 author       = {Yong Kiam Tan and Andr{\'{e}} Platzer},
 year         = {2021},
 title        = {Deductive Stability Proofs for Ordinary Differential Equations},
 editor       = {Jan Friso Groote and Kim Guldstrand Larsen},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, {TACAS} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part {II}},
 series       = {LNCS},
 volume       = {12652},
 publisher    = {Springer},
 pages        = {181--199},
 doi          = {10.1007/978-3-030-72013-1\_10},
)
@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/icfem/WangZZ15,
 author       = {Shuling Wang and Naijun Zhan and Liang Zou},
 year         = {2015},
 title        = {An Improved {HHL} Prover: An Interactive Theorem Prover for Hybrid Systems},
 editor       = {Michael J. Butler and Sylvain Conchon and Za{\"{\i}}di, Fatiha},
 booktitle    = {Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November 3-5, 2015, Proceedings},
 series       = {LNCS},
 volume       = {9407},
 publisher    = {Springer},
 pages        = {382--399},
 doi          = {10.1007/978-3-319-25423-4\_25},
)
@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},
)
@article(DBLP:journals/jar/Wos87c,
 author       = {Larry Wos},
 year         = {1987},
 title        = {The Problem of Definition Expansion and Contraction},
 journal      = {J. Autom. Reason.},
 volume       = {3},
 number       = {4},
 pages        = {433--435},
 doi          = {10.1007/BF00247438},
)