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.
Yves Bertot & Pierre Castéran (2004):
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS Series.
Springer,
doi:10.1007/978-3-662-07964-5.
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen & André Platzer (2018):
VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models.
In: Dan Grossman: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018.
ACM,
pp. 617–630,
doi:10.1145/3192366.3192406.
Nathan Fulton, Stefan Mitsch, Brandon Bohrer & André Platzer (2017):
Bellerophon: Tactical Theorem Proving for Hybrid Systems.
In: Mauricio Ayala-Rincón & César A. Muñoz: ITP,
LNCS 10499.
Springer,
pp. 207–224,
doi:10.1007/978-3-319-66107-0_14.
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 Felty & Aart Middeldorp: CADE,
LNCS 9195.
Springer,
Berlin,
pp. 527–538,
doi:10.1007/978-3-319-21401-6_36.
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.
Jiang Liu, Naijun Zhan & Hengjun Zhao (2011):
Computing semi-algebraic invariants for polynomial dynamical systems.
In: Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah & Sebastian Fischmeister: 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.
ACM,
pp. 97–106,
doi:10.1145/2038642.2038659.
Stefan Mitsch & André Platzer (2016):
The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving.
In: Catherine Dubois, Paolo Masci & Dominique Méry: 3rd Workshop on Formal Integrated Development Environment,
EPTCS 240,
pp. 67–81,
doi:10.4204/EPTCS.240.5.
Stefan Mitsch & André Platzer (2016):
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models.
Form. Methods Syst. Des. 49(1-2),
pp. 33–74,
doi:10.1007/s10703-016-0241-z.
Special issue of selected papers from RV'14.
Stefan Mitsch & André Platzer (2020):
A Retrospective on Developing Hybrid Systems Provers in the KeYmaera Family - A Tale of Three Provers.
In: Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle & Matthias Ulbrich: Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY,
LNCS 12345.
Springer,
pp. 21–64,
doi:10.1007/978-3-030-64354-6_2.
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger & André Platzer (2018):
Tactical Contract Composition for Hybrid System Component Verification.
STTT 20(6),
pp. 615–643,
doi:10.1007/s10009-018-0502-9.
Special issue for selected papers from FASE'17.
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,
doi:10.1007/3-540-45949-9.
Lawrence C. Paulson (2010):
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers.
In: Renate A. Schmidt, Stephan Schulz & Boris Konev: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010,
EPiC Series 9.
EasyChair,
pp. 1–10,
doi:10.29007/36dt.
André Platzer (2017):
A Complete Uniform Substitution Calculus for Differential Dynamic Logic.
J. Autom. Reas. 59(2),
pp. 219–265,
doi:10.1007/s10817-016-9385-1.
André Platzer (2018):
Logical Foundations of Cyber-Physical Systems.
Springer,
Cham,
doi:10.1007/978-3-319-63588-0.
André Platzer & Jan-David Quesel (2008):
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems..
In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: IJCAR,
LNCS 5195.
Springer,
Berlin,
pp. 171–178,
doi:10.1007/978-3-540-71070-7_15.
André Platzer & Yong Kiam Tan (2020):
Differential Equation Invariance Axiomatization.
J. ACM 67(1),
pp. 6:1–6:66,
doi:10.1145/3380825.
David W. Renshaw, Sarah M. Loos & André Platzer (2011):
Distributed Theorem Proving for Distributed Hybrid Systems.
In: Shengchao Qin & Zongyan Qiu: ICFEM,
LNCS 6991.
Springer,
pp. 356–371,
doi:10.1007/978-3-642-24559-6_25.
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell & André Platzer (2021):
Pegasus: Sound Continuous Invariant Generation.
Form. Methods Syst. Des.,
doi:10.1007/s10703-020-00355-z.
Special issue for selected papers from FM'19.
Yong Kiam Tan & André Platzer (2021):
Deductive Stability Proofs for Ordinary Differential Equations.
In: Jan Friso Groote & Kim Guldstrand Larsen: 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,
LNCS 12652.
Springer,
pp. 181–199,
doi:10.1007/978-3-030-72013-1_10.
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.
Shuling Wang, Naijun Zhan & Liang Zou (2015):
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems.
In: Michael J. Butler, Sylvain Conchon & Fatiha Zaïdi: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings,
LNCS 9407.
Springer,
pp. 382–399,
doi:10.1007/978-3-319-25423-4_25.
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.
Larry Wos (1987):
The Problem of Definition Expansion and Contraction.
J. Autom. Reason. 3(4),
pp. 433–435,
doi:10.1007/BF00247438.
eptcs@eptcs.org