Older News
 11/04/2019: KeYmaera X 4.7.4 release
Differential equation completeness automation improvements [Tactics] Improved equality rewriting: support for rewriting in bound occurrences such as
y=x ==> \forall x x<y
as well asy=x ==> [a(x)]x<y
 [Tactics] Improved Barrier and ODE invariant completeness: automated constification of unchanged variables x to nullary function symbols x() now proves more ODEs automatically
 [Tactics] Differential weakening: fast dW preserves only constants, dWplus conserves full initial state
 [Tactics] Differential ghost: extended unification for division with variations of the shape
y' = y/a + b
 [Backend] (Fix) Initialize a single Mathematica/Wolfram Engine instance to avoid startup hiccups with restricted licenses
 [Backend] (Fix) Wait for backend to stay alive
 [Printer] (Fix) Archive printer: export hybrid program definition names without ()
 [Server] (Fix) Avoid infinite startup when running command line tools (parse, prove etc.)
 [Tactics] Improved equality rewriting: support for rewriting in bound occurrences such as
 10/10/2019: Best Tool Paper Award at FM 2019 for Pegasus, the continuous invariant generator for KeYmaera X
 10/04/2019: KeYmaera X 4.7.3 release
new Wolfram Engine backend and proof inspection features. [Backend] Wolfram Engine backend supporting real arithmetic and ODE invariant generation
 [UI] Expand tactic step details by clicking (≡)
 [UI] Reuse finished proofs as lemmas (Browse→Lemmas menu)
 [Tactics] Explore a model using loop and ODE invariant annotations and show all failing branches (Explore button)
 [Tactics] Proof state labeling: edit branch tab names to set labels in the proof
 09/10/2019: KeYmaera X 4.7.2 release
UI and backend stability updates. [Backend] Stability fixes
 [Parser] Support for model illustration links
 [UI] Model illustration images
 09/01/2019: KeYmaera X 4.7.1 release
User interface improvements and tactic syntax updates. [UI] New tool: Pegasus invariant generator
 [UI] Additional help and examples, improved undo, improved formula pretty printing/layout
 [Tactics] Syntax update double quotation marks "..." for tactic arguments
 [Tactics] Partial QE with simplification using assumptions
 [Tactics] ODE automation improvement (counterexamples, condition search)
 06/16/2019: KeYmaera X 4.7.0 release
major update, automation improvement, performance, and stability updates [Core] Fast onepass uniform substitution
 [Backend] Invariant generator Pegasus for differential equations (Qualitative Analysis, First Integrals, Darboux Polynomials, Barrier Certificates)
 [Backend] Z3 update 4.8.4
 [Parser] Significant performance improvement
 [Tactics] Improved ODE automation
 [Tactics] Interval arithmetic: proves quantifierfree real arithmetic when the antecedent has numerical bounds for all free variables of the succedent
 [UI] Command line: prove verbose for tactic progress printing
 [Code Synthesis] Monitor C code generator: IDs now identify failed monitor subcondition
 01/11/2019: KeYmaera X 4.6.3 release
Stability and usability improvements [UI] Model editing during a proof with the keyboard symbol
 [UI] Tactic help on menu and context menu entries
 [Tactics] Execute until error without discarding nonapplicable tactics
 [Tactics] ODE solve supports all nilpotent linear systems
 [Parser] Support for exercises
 11/26/2018: KeYmaera X 4.6.2 release
Performance and robustness improvements [Tactics] ODE solver performance improvements
 [Tactics] Tactic positioning and input robustness, including quantifier instantiations, abbreviations and special functions, input flexibility for differential ghosts, monotonicity
 [Parser] Improved error messages
 [UI] Robustness improvements, backend tool status polling, polling performance improvement
 10/09/2018: KeYmaera X 4.6.1 release
Stability release [Parser] Improved stability and error reporting
 [Tactics] Preview: modular componentbased proofs
 09/22/2018: KeYmaera X 4.6.0 release
Major improvement in KeYmaera X file format and parser, general tool stability and automation [Tools] Automated proof backup in plaintext archive files
 [Tools] Improved tool stability, tool busy indicator, and tool restart and connection testing
 [Tactics] Improved automation on typical model shapes, ODE tactic improvements
 [Parser] Major update to archive syntax and parser error reporting:
ArchiveEntry "Example" Description "Illustrates the main archive syntax changes". Definitions /* function symbols cannot change their value */ Real A = 5; /* realvalued acceleration constant defined as 5 */ Real B; /* realvalued braking constant is uninterpreted */ Bool inv(Real v) <> (v>=0); /* invariant formula definition */ End. ProgramVariables /* program variables may change their value over time */ Real x, v; /* realvalued position and velocity */ Real a; /* current acceleration chosen by controller */ End. Problem A>0 & B>0 & v>=0 > [ { { ?v<=5; a:=A; ++ a:=0; ++ a:=B } { x'=v, v'=a & v>=0 } }* @invariant(inv(v)) ] v>=0 End. End.
 07/09/2018: KeYmaera X 4.5.0 release
Major improvements on automation, invariant generation, and differential equation automation. [New] Pegasus invariant generator for differential equations
 [New] ODE automation tactics for axiomatic proofs from differential ghost and differential refinement axioms, proofs of barrier certificates, and proofs of invariance properties that involve Darboux polynomials
 [Preview] Invariant generation for loops based on fixpointsearch over invariants for differential equations
 [Tactics] Liveness: loop convergence with userdefinable convergence variable, improved <:=> assignment tactics
 [Tactics] Extended proof search automation in the context of universal/existential quantifiers
 [Tools] C code generator for structured monitors with subroutines and error message printing
 04/18/2018: KeYmaera X 4.4.3 release 3rd birthday release of KeYmaera X
 [New] Tactic
barrier
proves barrier certificates of ODEs (automatically used inODE
tactic)
For example, provex>=0  [{x'=100*x^4+y*x^3x^2+x+c, c'=x+y+z & c>x}]x>=0
with tacticbarrier(1)
or tacticODE(1)
 [New] Tactic
dbx
proves ODEs using Darboux polynomials (automatically used inODE
tactic)
For example, provex+z<0  [{x'=x^2, z'=z*x+y & y=x^2}]x+z<0
with tacticdbx({x},1)
or tacticODE(1)
 [New] Model documentation and proof hints with
@invariant
annotations for ODEs
For example, provide a list of two differential invariants:[{x'=2,y'=1} @invariant(x>=old(x), y<=old(y))]p()
 [New] Conditional differential invariant annotations
For example, provide a list of two differential invariants, one for each branch:[{a:=2; ++ a:=1;} ; {x'=a} @invariant( (x'=2 > x>=old(x)), (x'=1 > x<=old(x))) ]p()
 [UI] Significant performance improvements
 [Tactics] Tactic
dW
now keeps all initial conditions  [Tactics] Configurable timeouts for tactics
QE
andODE
(configuration filekeymaerax.conf
)  [Tactics] Combinator
s > t
runs tactics
first and then tactict
regardless of the result ofs
 [New] Tactic
 02/28/2018: KeYmaera X 4.4.2 release
 [Performance] Significant performance improvements by disabling logging by default
 [UI] New web UI axiom and proof step browser
 [UI] Hint display and tactic popover fixes
 [Tactics] New loop induction with abstraction
throughout(inv,pos)
proves loopinit > [{a;b}*]safe
with throughout invariantinv
from subgoals: base case:
init > inv
 use case:
inv > safe
 induction steps:
inv > [a]inv
andinv > [b]inv
 base case:
 01/18/2018: KeYmaera X 4.4.1 release
 Backend tool and tactic stability improvements
 [New] Store and use lemma entries in
.kyx
archives:
Lemma "My lemma". ... End.
to store the given lemma under the identified name "My lemma". 
useLemma({`My lemma`},{`prop`})
to close goal by lemma, use propositional reasoning to adapt shape 
useLemmaAt({`My lemma`},{`1`},2)
to match lemma expression at subposition 1 with formula at sequent position 2

 [New] Convert KeYmaera X proof terms to Isabelle dL proof checker
 [New] Configuration is now stored in a text file
~/.keymaerax/keymaerax.conf
 [New] Transform hybrid programs to C control code
 09/18/2017: KeYmaera X 4.4 major release
 Core: Uniform substitutions for Nary formula and function definitions.
 Parser: Use
._i
to refer to the ith argument. For example, define a binary function
sum
as:sum(R,R) = ( ._0 + ._1 ).
 define predicate
sumgt
as:sumgt(R,R,R) <> ( sum(._0,._1) > ._2 ).
 define a hybrid program
increment
as:HP increment ::= { x:=x+1; }.
 define a binary function
 Tactics: New: use finished proofs as lemmas.

useLemma({Name of proved model})
when the open goal matches the lemma literally. 
useLemma({Name of proved model}, {prop})
to apply the lemma with propositional reasoning to make goals match.

 Tools: New: proof statistics after checking proof archives with
check
command line argument.  Tools: New: C control code synthesis (feature preview)
 Tools: Improved: C monitor code synthesis (feature preview)
 Stability improvements: archive checking, ODE solution ordering
 08/26/2017: KeYmaera X 4.3.16 release
 Three new tactics for automatic nth Taylor approximation:

circularApproximate(s,c,n,pos)
: for circular dynamics{s'=c, c'=s}

expApproximate(e,n,pos)
: for exponential dynamics{e'=e}

autoApproximate(n,pos)
: Tries to find{e'=e}
then tries to find{s'=c,c'=s}
and applies the relevant approximation tactic.

 More powerful formula editing in UI:

expand(expr)
will expand functions min/max/abs, e.g.,expand(abs(0)) >= 0

abbrv(term,name)
will abbreviate terms, e.g.,x+abbrv(2+3,five) >= 0

 Search and apply lemmas
 Autocompletion search box in the rule application dialog
 Click lemma subformulas to adjust the direction in which lemmas are applied
 User interface startup improved. Browser no longer opens automatically on Linux, because this made Java hang on some configurations.
 Various improvements to the tactics framework and standard library.
 Bug fix in how numbers are prettyprinted.
 Three new tactics for automatic nth Taylor approximation:
 08/08/2017: KeYmaera X 4.3.15 release
 UI: Improvements to presentation and browse mode
 UI: Render nullary function symbols
b()
without parentheses asb
 Updates Z3 solver to 4.5.0, with improved QE support for machines without Mathematica.
 Improved update code for Windows.
 07/28/2017: KeYmaera X 4.3.14 release
Fix: ODE solver tactic printing forsolveEnd
solution tactic with evolution domain constraint only at endpoint  07/27/2017: KeYmaera X 4.3.13 release
 Proof browsing display proof step justification
 New: Model editing
 Web UI and backend fixes and improvements
 Feature preview: exercise models with placeholders
__________
 07/20/2017: KeYmaera X 4.3.12 release
 New: stepbystep proof browsing to illustrate and explain proofs
 New: tactic tooltips on proof step in sequent proofs
 Revamped proof step highlighting
 User interface and backend stability improvements
 07/11/2017: KeYmaera X 4.3.11 release
 Substantially improved Web UI performance by significant factors.
 New: Builtin text editor to edit new models from Models>New Model>Edit.
 New: Models can be plain differential dynamic logic formulas without variable declarations such as
x>=0 & a>0 > [{x'=v,v'=a & v>=0}] x>=0
 New: Abbreviate terms when editing formulas with special function symbol
abbrv(term)
orabbrv(term, abbreviation)
For examplex+abbrv(3+2, v) > y
becomesx+v > y, v = 3+2
with all occurrences of3+2
replaced byv
.  Improved differential cut tactic: refer to initial values of arbitrary terms with
old(term)
and support for multiple uses ofold(term)
 Improved syntax for differential ghost tactic:
dG({`y'=a*y+b`}, {`G`}, 1)
instead ofdG({`y`},{`a`},{`b`}, {`G`}, 1)
 Beta: Parse unicode syntax such as ∧ ∨ ∀ ∃ → ≥
 New: browse model archives on
web.keymaeraX.org/show/itp17/parachute.kya
or on localhost aslocalhost:8090/show/http://url/of/my.kya
 05/24/2017: KeYmaera X 4.3.10 release
 ODE solver generalized for diamond ODEs
 UI syntax highlighting and interaction improvements
 UI displays proof hints on how to proceed
 UI displays equality rewriting in context menu
 Workaround for recent Mathematica bugs by using a TCP version of J/Link
 Bugfix model import
 04/27/2017: KeYmaera X 4.3.9 release
 Tactic input validation to prevent impossible proof attempts
 Performance improvements in user interface
 Function and predicate definitions in
.kyx
modelsFunctions. R init() = (10). /* fixed initial position */ R obs(). /* arbitrary obstacle position */ R dist(R) = ((.)obs()). /* distance of argument (.) to obstacle */ B safe(R) <> (dist((.))>5). /* safe distance of arg (.) from obstacle */ End. ProgramVariables. R x. /* position */ R v. /* velocity */ End. Problem. x=init() & safe(init()) & v>0 > [{x'=v}] safe(x) End.
 04/18/2017: KeYmaera X 4.3.8 release
 Substantial performance improvements
 Improved support for hybrid game proofs
 Updated database format for performance
 03/20/2017: KeYmaera X 4.3.7 release
 Parser supports ifthenelse statement
if (v^2>5) {a:=b;} else {a:=2;}
 Parser supports ifthenelse statement
 03/09/2017: KeYmaera X 4.3.6 release
 Stability improvements, including generalizations for differential equation solving

Concrete syntax updated to help disambiguate
Braces are now required around differential equations{x'=x^2,y'=2*x+y}
Constant symbolsc()
can now be used without parentheses in.kyx
problem files
 02/20/2017: KeYmaera X 4.3.5 release
UI bugfixes and stability improvements  02/15/2017: KeYmaera X 4.3.4 release
Minor stability release generalizing the flexibility of the Axiomatic ODE Solver tactic  02/13/2017: KeYmaera X 4.3.3 release
 Edit: formula editing can rewrite formulas everywhere
 Step into failed tactics to observe partial progress and debug the proof
 ODE solver generalized to systems written in any order
 Simplifier improvements
 Stability advances
 01/28/2017: KeYmaera X 4.3.2 release
 New Learner's mode
 Simplify differential equation tactics
 UI stability and help improvements
 Preview: Obtain internal details on tactical proof steps
 01/20/2017: KeYmaera X 4.3.1 release
 Get quick usage help with ? menu button on each page
 Import and export for model/proof archive (
.kya
file).  Synthesize verified safety metrics from ModelPlex
 Improved automation of
ode
tactic for differential equations.  Prover core fixes
 11/08/2016: KeYmaera X 4.3 release
 Add support for Differential Game Logic (dGL) for Hybrid Games
 ModelPlex web UI integration for both controller and model monitors
 Axiomatic ODE solver improvements (box and diamond properties as well as inplace solving)
 UI improvements and bug fixes (tactic difference, tactic parser errors)
 Stability improvements (unifier, UI, quantifier instantiation)
 09/28/2016: KeYmaera X 4.2.2 release
 Extraction and execution of tactics with input
 Web user interface improvements
 Tactic and lemma download on finished proof
 09/17/2016: KeYmaera X 4.2.1 release
 Significant performance advances for a snappier interaction with KeYmaera X
 Readability improvements in tactic extraction
 User interface polishing, improvements, and styling, including position highlighting
 Faster database interaction
 Prover core fixes for bound renaming (unexploited)
 Inverse characteristic method for differential invariant generation
 Better command line interfaces
 09/02/2016: KeYmaera X 4.2 first stable release
 User interface advances
 Tactic extraction, tactic programming, and replay
 Major backend tool improvements
 KeYmaera X runs standalone without the need to install additional tools since it ships with the Z3 solver. Mathematica is recommended as an addon installation for advanced automation and simulation features, though.
 Axiomatic differential equation solver with solvebyproof technology

ODE
tactic for automatic proofs of differential equations  Invariant and differential invariant generation techniques
 Tutorial import feature
 Faster unificationbased tactics
 Significant prover core advances, fixes, and simplifications
 07/20/2016: KeYmaera X 4.2b2 release
 Axiomatic ODE Solver
 Differential ghosts are now exposed in web UI (diffGhost)
 Rewrite of the Mathematica interface for improved stability
 Improved kernel functionality for interpreted functions
 SSL mode for hosted web servers
 04/11/2016: KeYmaera X 4.2b1 release
 Major improvements to prover core
 Pencil tool for simplifying arithmetic in place
 Simple system simulation feature
 Various bug fixes
 Ships with tutorial examples from CPSWEEEK 2016
 03/01/2016: KeYmaera X 4.1b4 release
UI bug fixes  02/19/2016: KeYmaera X 4.1b3 release
 UI improvements and bug fixes
 Improved differential equation solving tactics
 01/22/2016: KeYmaera X 4.1b2 release
 Draganddrop support for constructing proofs
 Major performance enhancement make KeYmaera X snappier to use
 More userfriendly error messages when things go wrong
 01/15/2016: KeYmaera X 4.1b1 release
 Entirely new user interface with native sequent proofs
 Support proofbypointing intuition in user interface
 Contextual proof development supported in user interface
 New Bellerophon tactic language and tactic framework
 Undo proof steps, stopping tactics, counterexample support
 Proof storage format and proof management backend redesigned
 09/25/2015: KeYmaera X 4.0b1 release
First public release of KeYmaera X source code, open source license GPLv2  04/18/2015: First public KeYmaera X 4.0a1 release