Developers
![]() Stefan Mitsch | ![]() André Platzer | ![]() Nathan Fulton |
Contributors
![]() Yong Kiam Tan | ![]() Andrew Sogokon | ![]() Brandon Bohrer |
![]() Fabian Immler | ![]() Katherine Cordwell |
Past Contributors
![]() Jan-David Quesel | ![]() Marcus Völp | ![]() Ran Ji |
Power Users
The KeYmaera X developers are incredibly thankful for the helpful feedback on its earlier versions from all the users everywhere, but especially the power users:![]() Jean-Baptiste Jeannin | ![]() Yanni Kouskoulas | ![]() Khalil Ghorbal |
Primary Responsibilities
If you have a question about KeYmaera X, either ask on the KeYmaera X mailing list or directly ask the right person based on the primary responsibilities listed below.
Developers:- Stefan Mitsch: user interface, archive parser, tactic library, tactic tracing and tactic extraction, lemma mechanism, command line interface, HyDRA web service API, tactic task scheduler, Mathematica+SMT interface, lexer, data model and database storage, ModelPlex tactics, C code generator
- André Platzer: prover microkernel, differential dynamic logic parser+printer, unification-based calculus auto-tactics, forward tactics and engine, help documents
- Nathan Fulton: Bellerophon tactic framework, tactic parser, Mathematica interface, HyDRA web service API
- Yong Kiam Tan: differential equation invariant proving, formula simplifier tactics, Pegasus barrier certificate generation
- Brandon Bohrer: proof term generation and parsing, database storage, security
- Andrew Sogokon: Pegasus invariant generator
- Fabian Immler: interval arithmetic proving
- Katherine Cordwell: Contributions to Pegasus linear invariant generator and qualitative abstraction