Older News on KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

Older News

• 2019-11-04: 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 as y=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.)
• 2019-10-10: Best Tool Paper Award at FM 2019 for Pegasus, the continuous invariant generator for KeYmaera X
• 2019-10-04: 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
• 2019-09-10: KeYmaera X 4.7.2 release
  UI and backend stability updates.
  • Backend: Stability fixes
  • Parser: Support for model illustration links
  • UI: Model illustration images
• 2019-09-01: 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)
• 2019-06-16: KeYmaera X 4.7.0 major release
  Major 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 4.8.4
  • 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 generator: Monitor C code generator: IDs now identify failed monitor sub-condition
• 2019-01-11: 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 non-applicable tactics
  • Tactics: ODE solve supports all nilpotent linear systems
  • Parser: Support for exercises
• 2018-11-26: 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
• 2018-10-09: KeYmaera X 4.6.1 release
  Stability release
  • Parser: Improved stability and error reporting
  • Tactics: Preview: modular component-based proofs
• 2018-09-22: KeYmaera X 4.6.0 major 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;    /* real-valued acceleration constant defined as 5 */
      Real B;        /* real-valued 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;     /* 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.
    

• 2018-07-09: KeYmaera X 4.5.0 major 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 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
• 2018-04-18: KeYmaera X 4.4.3 release 3rd birthday release of KeYmaera X
  • 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), 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 and ODE (configuration file keymaerax.conf)
  • Tactics: Combinator s > t runs tactic s first and then tactic t regardless of the result of s
• 2018-02-28: 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 loop init -> [{a;b}*]safe with throughout invariant inv from subgoals:
    • base case: init -> inv
    • use case: inv -> safe
    • induction steps: inv -> [a]inv and inv -> [b]inv
• 2018-01-18: 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 sub-position 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
• 2017-09-18: KeYmaera X 4.4 major release
  • Core: Uniform substitutions for N-ary 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; }.
  • 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
• 2017-08-26: 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
    • Auto-completion 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 pretty-printed.
• 2017-08-08: KeYmaera X 4.3.15 release
  • UI: Improvements to presentation and browse mode
  • UI: Render nullary function symbols b() without parentheses as b
  • Updates Z3 solver to 4.5.0, with improved QE support for machines without Mathematica.
  • Improved update code for Windows.
• 2017-07-28: KeYmaera X 4.3.14 release
  Fix: ODE solver tactic printing for solveEnd solution tactic with evolution domain constraint only at endpoint
• 2017-07-27: 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 __________
• 2017-07-20: KeYmaera X 4.3.12 release
  • New: step-by-step 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
• 2017-07-11: KeYmaera X 4.3.11 release
  • Substantially improved Web UI performance by significant factors.
  • New: Built-in 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) or

    abbrv(term, abbreviation)

    For example x+abbrv(3+2, v) > y becomes x+v > y, v = 3+2 with all occurrences of 3+2 replaced by v.
  • Improved differential cut tactic: refer to initial values of arbitrary terms with old(term) and support for multiple uses of old(term)
  • Improved syntax for differential ghost tactic:

    dG({`y'=a*y+b`}, {`G`}, 1)

    instead of dG({`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 as localhost:8090/show/http://url/of/my.kya
• 2017-05-24: 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
• 2017-04-27: 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 models

    Functions.
      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.
      

• 2017-04-18: KeYmaera X 4.3.8 release
  • Substantial performance improvements
  • Improved support for hybrid game proofs
  • Updated database format for performance
• 2017-03-20: KeYmaera X 4.3.7 release
  • Parser supports if-then-else statement

        if (v^2>5) {a:=-b;} else {a:=2;}
        

• 2017-03-09: 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 symbols c() can now be used without parentheses in .kyx problem files
• 2017-02-20: KeYmaera X 4.3.5 release
  UI bugfixes and stability improvements
• 2017-02-15: KeYmaera X 4.3.4 release
  Minor stability release generalizing the flexibility of the Axiomatic ODE Solver tactic
• 2017-02-13: 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
• 2017-01-28: 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
• 2017-01-20: 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
• 2016-11-08: KeYmaera X 4.3 major 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 in-place solving)
  • UI improvements and bug fixes (tactic difference, tactic parser errors)
  • Stability improvements (unifier, UI, quantifier instantiation)
• 2016-09-28: KeYmaera X 4.2.2 release
  • Extraction and execution of tactics with input
  • Web user interface improvements
  • Tactic and lemma download on finished proof
• 2016-09-17: 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
• 2016-09-02: 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 add-on installation for advanced automation and simulation features, though.
  • Axiomatic differential equation solver with solve-by-proof technology
  • ODE tactic for automatic proofs of differential equations
  • Invariant and differential invariant generation techniques
  • Tutorial import feature
  • Faster unification-based tactics
  • Significant prover core advances, fixes, and simplifications
• 2016-07-20: 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
• 2016-04-11: 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
• 2016-03-01: KeYmaera X 4.1b4 release
  UI bug fixes
• 2016-02-19: KeYmaera X 4.1b3 release
  • UI improvements and bug fixes
  • Improved differential equation solving tactics
• 2016-01-22: KeYmaera X 4.1b2 release
  • Drag-and-drop support for constructing proofs
  • Major performance enhancement make KeYmaera X snappier to use
  • More user-friendly error messages when things go wrong
• 2016-01-15: KeYmaera X 4.1b1 release
  • Entirely new user interface with native sequent proofs
  • Support proof-by-pointing 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
• 2015-09-25: KeYmaera X 4.0b1 release
  First public release of KeYmaera X source code, open source license GPLv2
• 2015-04-18: First public KeYmaera X 4.0a1 release