English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Hybrid systems verification is quite important for developing correctcontrollers for physical systems, but is also challenging. Verificationengineers, thus, need to be empowered with ways of guiding hybrid systemsverification while receiving as much help from automation as possible. Due toundecidability, verification tools need sufficient means for intervening duringthe verification and need to allow verification engineers to provide systemdesign insights.  This paper presents the design ideas behind the user interface for the hybridsystems theorem prover KeYmaera X. We discuss how they make it easier to provehybrid systems as well as help learn how to conduct proofs in the first place.Unsurprisingly, the most difficult user interface challenges come from thedesire to integrate automation and human guidance. We also share thoughts howthe success of such a user interface design could be evaluated and anecdotalobservations about it.

The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving