Version 4.7

Version 4.7 major core update, automation improvement, performance, and stability updates

• [Core] Fast one-pass uniform substitution
• [Backend] Invariant generator Pegasus for differential equations (Qualitative Analysis, First Integrals, Darboux Polynomials, Barrier Certificates)
• [Backend] Z3 update
• [Parser] Significant performance improvement
• [Tactics] Improved ODE automation
• [Tactics] Interval arithmetic: proves quantifier-free 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 sub-condition

Version 4.6.3

Version 4.6.3 provides UI and tactic improvements

• [UI] Model editing during a proof
• [UI] Tactic help on menu and context menu entries
• [Tactics] Execute until error without discarding non-applicable tactics
• [Tactics] ODE solve support for nilpotent linear systems
• [Parser] Support for exercises

Version 4.6.2

Version 4.6.2 provides performance and robustness improvements

• [Tactics] ODE solver performance improvements
• [Tactics] Tactic positioning and input robustness: abbreviation and special function handling in context, quantifier instantiation with variables and terms, input unificiation for differential ghosts, monotonicity at any succedent position
• [Parser] Improved error messages
• [UI] Robustness improvements, backend tool status polling, polling performance improvement

Version 4.6.1

• [Parser] Improved stability and error reporting
• [Tactics] Preview: modular component-based proofs

Version 4.6.0

Version 4.6.0 provides a major update to the archive syntax and archive parsing.

• [Parser] Major update to archive syntax and parser error reporting

           ArchiveEntry "Example"
           Description "Illustrates the main archive syntax changes".
           
           Definitions
             Real A = 5;
             Real B;
             Bool inv(Real v) <-> v>=0;
           End.
           
           ProgramVariables
             Real x, v;   /* real-valued 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.

• [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

Version 4.5.0

Version 4.5.0 provides a major update to the invariant generation and proving techniques for differential equations in its automated ODE tactic.

• [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 fixpoint-search over invariants for differential equations

• [Tactics] Liveness: loop convergence with user-definable 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 sub-routines and error message printing

Version 4.4.3

• [New] Tactic barrier proves barrier certificates of ODEs (automatically used in ODE tactic)
  For example, prove x>=0 |- [{x'=100*x^4+y*x^3-x^2+x+c, c'=x+y+z & c>x}]x>=0
  with tactic barrier(1) or tactic ODE(1)

• [New] Tactic dbx proves ODEs using Darboux polynomials (automatically used in ODE tactic)
  For example, prove x+z<0 |- [{x'=x^2, z'=z*x+y & y=-x^2}]x+z<0
  with tactic dbx({x},1) or tactic ODE(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), /* x increases */ y<=old(y)) /* y descreases */ ]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 increases */ (x'=-1 -> x<=old(x))) /* x decreases */ ]p()

• [UI] Performance improvements

• [Tactics] Tactic dW now keeps all initial conditions

• [Tactics] Configurable timeouts for tactics QE and ODE (configuration file keymaerax.conf)

• [Tactics] Combinator s > t runs tactic s first and then tactic t regardless of the result of s

Version 4.4.2

• [UI] New web UI axiom and proof step browser
• [UI] Hint display and tactic popover fixes
• [Performance] Significant performance improvements by disabling logging by default
• [Tactics] New loop induction with abstraction
  • throughout(inv,pos) for loops init -> [{a;b}*]safe
    proves loop from subgoals
    base case: init -> inv
    use case: inv -> safe
    induction steps: inv -> [a]inv and inv -> [b]inv

Version 4.4.1

• Backend tool and tactic stability improvements
• [New] Store and use lemma entries in .kyx archives:
  Store: Lemma "My lemma". ... End. to store the given lemma under the identified name "My lemma".
  Use:
  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 sub-position 1 with formula at sequent position 2
• [New] Convert 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

Version 4.4

KeYmaera X version 4.4

• [Core] New: N-ary formula and function definitions.
  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 ).
• [Parser] New: Program definitions.
  For example, HP increment ::= { x:=x+1; }.
• [Tactics] New: use finished proofs as lemmas, for example 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.
• [Tools] New: proof statistics after checking archives with -check
• [Tools] New: C control code synthesis (feature preview)
• [Tools] Improved: C monitor code synthesis (feature preview)
• Stability improvements: archive checking, ODE solution ordering