Packages

object KeYmaeraX

Command-line interface launcher for KeYmaera X, the aXiomatic Tactical Theorem Prover for Hybrid Systems and Hybrid Games.

- edu.cmu.cs.ls.keymaerax.core - KeYmaera X kernel, proof certificates, main data structures - edu.cmu.cs.ls.keymaerax.btactics - Tactic language library - edu.cmu.cs.ls.keymaerax.bellerophon - Bellerophon tactic language and tactic interpreter

See also

Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012

Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981

Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. KeYmaeraX
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. class KeYmaeraXSecurityManager extends SecurityManager

    Implements the security policy for the KeYmaera X web server.

    Implements the security policy for the KeYmaera X web server.

    Preferably we would heavily restrict uses of reflection (to prevent, for example, creating fake Provables), but we know of no way to do so except relying on extremely fragile methods such as crawling the call stack. The same goes for restricting read access to files.

    Instead we settle for preventing people from installing less-restrictive security managers and restricting all writes to be inside the .keymaerax directory.

  2. case class ProofStatistics(name: String, tacticName: String, status: String, timeout: Long, duration: Long, qeDuration: Long, proofSteps: Int, tacticSize: Int) extends Product with Serializable

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. var LAUNCH: Boolean
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def check(options: OptionMap): Unit

    Checks the given archive file.

    Checks the given archive file.

    KeYmaeraXLemmaPrinter(Prover(tactic)(KeYmaeraXProblemParser(input)))
    options

    The prover options.

  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. def codegen(options: OptionMap): Unit

    Code generation

    Code generation

    CGenerator()(input)
  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  11. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. def launchUI(args: Array[String]): Unit

    Launch the web user interface

  16. def main(args: Array[String]): Unit
  17. def modelplex(options: OptionMap): Unit

    ModelPlex monitor synthesis for the given input files

    ModelPlex monitor synthesis for the given input files

    KeYmaeraXPrettyPrinter(ModelPlex(vars)(KeYmaeraXProblemParser(input))
    options

    in describes input file name, vars describes the list of variables, out describes the output file name.

  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. def printNode(node: Sequent): Unit
  22. def printOpenGoals(node: ProvableSig): Unit

    Print brief information about all open goals in the proof tree under node

  23. def prove(options: OptionMap): Unit

    Prove given input file (with given tactic) to produce a lemma.

    Prove given input file (with given tactic) to produce a lemma.

    KeYmaeraXLemmaPrinter(Prover(tactic)(KeYmaeraXProblemParser(input)))
    options

    The prover options.

  24. def repl(options: OptionMap): Unit
  25. def stripHints(options: OptionMap): Unit

    Strips proof hints from the model.

  26. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  27. def toString(): String
    Definition Classes
    AnyRef → Any
  28. val usage: String

    Usage -help information.

    Usage -help information.

    Note

    Formatted to 80 characters terminal width.

  29. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped