Developers
Stefan Mitsch |
André Platzer |
Yong Kiam Tan |
Contributors
Katherine Cordwell |
Aditi Kabra |
Past Developers
Nathan Fulton |
Brandon Bohrer |
Past Contributors
Fabian Immler |
Jan-David Quesel |
Andrew Sogokon |
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
- Yong Kiam Tan: differential equation invariant and liveness proving, formula simplifier tactics, Pegasus barrier certificate generation, switched system stability proving.
- Nathan Fulton: Bellerophon tactic framework, tactic parser, Mathematica interface, HyDRA web service API
- 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