The KeYmaera X Proof IDE

Stefan Mitsch (Computer Science Department; Carnegie Mellon; University); Andr\'e Platzer (Computer Science Department; Carnegie Mellon; University)

arXiv:1701.08469·cs.LO·January 31, 2017·F-IDE@FM

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

Stefan Mitsch (Computer Science Department, Carnegie Mellon, University), Andr\'e Platzer (Computer Science Department, Carnegie Mellon, University)

PDF

TL;DR

This paper discusses the design of the user interface for KeYmaera X, a hybrid systems theorem prover, focusing on usability, automation integration, and aiding verification engineers in proving complex hybrid systems.

Contribution

It presents novel design ideas for the KeYmaera X proof IDE that enhance usability and facilitate hybrid systems verification through better automation and human guidance.

Findings

01

Design ideas improve proof usability and learning

02

Integration of automation and human guidance is challenging

03

Anecdotal observations suggest positive impact on verification process

Abstract

Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights. This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface…

Figures7

Click any figure to enlarge with its caption.

Equations22

\underbrace{x\geq 2\land v\geq 0\rightarrow}_{\_}\text{initial conditions}{[{\underbrace{{\bigl{(}({?x>1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v}\bigr{)}}^{*}}_{\_}\text{hybrid program}}]}\underbrace{x\geq 0}_{\_}{\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\textstyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\scriptstyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\text{safety condition}}$\hss}}}

\underbrace{x\geq 2\land v\geq 0\rightarrow}_{\_}\text{initial conditions}{[{\underbrace{{\bigl{(}({?x>1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v}\bigr{)}}^{*}}_{\_}\text{hybrid program}}]}\underbrace{x\geq 0}_{\_}{\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\textstyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\scriptstyle{\text{safety condition}}$\hss}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\text{safety condition}}$\hss}}}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\phi~{}&\vdash{[{\alpha}]}\psi\land{[{\beta}]}\psi\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:choiceb}}}$}&\phi~{}&\vdash{[{{\alpha}\cup{\beta}}]}\psi\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\phi~{}&\vdash{[{\alpha}]}\psi\land{[{\beta}]}\psi\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:choiceb}}}$}&\phi~{}&\vdash{[{{\alpha}\cup{\beta}}]}\psi\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{>}0,v{\geq}0,x{>}1~{}&\vdash x-1{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:assignb}}}$}&x{>}0,v{\geq}0,x{>}1~{}&\vdash{[{x\mathrel{{:}{=}}x-1}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:testb},\ref{ir:implyR}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1}]}{[{x\mathrel{{:}{=}}x-1}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:composeb}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1;x\mathrel{{:}{=}}x-1}]}x{>}0\end{array}~{}&~{}~{}~{}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x_{\_}0{>}0,v{\geq}0~{}&\vdash\forall t{\geq}0\,\forall 0{\leq}s{\leq}t~{}(x=x_{\_}0+vs\rightarrow x{>}0)\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:ode}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{x^{\prime}=v}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:andR}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1;x\mathrel{{:}{=}}x-1}]}x{>}0\land{[{x^{\prime}=v}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:choiceb}}}$}&\ldots\leavevmode\hbox to6.67pt{\vbox to6.67pt{\pgfpicture\makeatletter\hbox{\hskip-0.2pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{>}0,v{\geq}0,x{>}1~{}&\vdash x-1{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:assignb}}}$}&x{>}0,v{\geq}0,x{>}1~{}&\vdash{[{x\mathrel{{:}{=}}x-1}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:testb},\ref{ir:implyR}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1}]}{[{x\mathrel{{:}{=}}x-1}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:composeb}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1;x\mathrel{{:}{=}}x-1}]}x{>}0\end{array}~{}&~{}~{}~{}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x_{\_}0{>}0,v{\geq}0~{}&\vdash\forall t{\geq}0\,\forall 0{\leq}s{\leq}t~{}(x=x_{\_}0+vs\rightarrow x{>}0)\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:ode}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{x^{\prime}=v}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:andR}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{?x{>}1;x\mathrel{{:}{=}}x-1}]}x{>}0\land{[{x^{\prime}=v}]}x{>}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:choiceb}}}$}&\ldots\leavevmode\hbox to6.67pt{\vbox to6.67pt{\pgfpicture\makeatletter\hbox{\hskip-0.2pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\text{(base case)}{}~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{\geq}2,v{\geq}0~{}&\vdash x{>}0\end{array}~{}&~{}~{}~{}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\text{(use case)}{}~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{>}0~{}&\vdash x{\geq}0\end{array}}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\leavevmode\hbox to6.67pt{\vbox to6.67pt{\pgfpicture\makeatletter\hbox{\hskip-0.2pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}\text{(induction step)}~{}\\ \cline{2-3}\cr&x{>}0,v{\geq}0~{}&\vdash{[{{(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:loop}}}$}&x{\geq}2,v{\geq}0~{}&\vdash{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:andL}}}$}&x{\geq}2\land v{\geq}0~{}&\vdash{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:implyR}}}$}&{}\hfil~{}&\vdash x{\geq}2\land v{\geq}0\rightarrow{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\text{(base case)}{}~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{\geq}2,v{\geq}0~{}&\vdash x{>}0\end{array}~{}&~{}~{}~{}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\text{(use case)}{}~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:QE}}}$}&x{>}0~{}&\vdash x{\geq}0\end{array}}{~{}~{}~{}\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\leavevmode\hbox to6.67pt{\vbox to6.67pt{\pgfpicture\makeatletter\hbox{\hskip-0.2pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.533pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}\text{(induction step)}~{}\\ \cline{2-3}\cr&x{>}0,v{\geq}0~{}&\vdash{[{{(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:loop}}}$}&x{\geq}2,v{\geq}0~{}&\vdash{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:andL}}}$}&x{\geq}2\land v{\geq}0~{}&\vdash{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:implyR}}}$}&{}\hfil~{}&\vdash x{\geq}2\land v{\geq}0\rightarrow{[{{({(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}}]}x{\geq}0\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&x{>}0,v{\geq}0,x{>}1~{}&\vdash x-1\geq 0\end{array}~{}&\quad{\quad\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&x{>}0,v{\geq}0~{}&\vdash{[{x^{\prime}=v}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:unfold}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{{?x{>}1;x\mathrel{{:}{=}}x-1}\cup{x^{\prime}=v}}]}x{>}0\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&x{>}0,v{\geq}0,x{>}1~{}&\vdash x-1\geq 0\end{array}~{}&\quad{\quad\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&x{>}0,v{\geq}0~{}&\vdash{[{x^{\prime}=v}]}x{>}0\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:unfold}}}$}&x{>}0,v{\geq}0~{}&\vdash{[{{?x{>}1;x\mathrel{{:}{=}}x-1}\cup{x^{\prime}=v}}]}x{>}0\end{array}

\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\textstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\scriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}\cfrac{{\Gamma}\vdash{{[{a}]}P,\Delta}\quad{\Gamma}\vdash{{[{b}]}P,\Delta}}{{\Gamma}\vdash{{[{{a}\cup{b}}]}P,\Delta}}\qquad\qquad\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\textstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\scriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}\cfrac{{\Gamma,{[{a}]}P,{[{b}]}P}\vdash{\Delta}}{{\Gamma,{[{{a}\cup{b}}]}P}\vdash{\Delta}}

\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\textstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\scriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andR}}}}$}}\cfrac{{\Gamma}\vdash{{[{a}]}P,\Delta}\quad{\Gamma}\vdash{{[{b}]}P,\Delta}}{{\Gamma}\vdash{{[{{a}\cup{b}}]}P,\Delta}}\qquad\qquad\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\textstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\scriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\scriptstyle{\text{\ref{ir:choiceb},\ref{ir:andL}}}}$}}\cfrac{{\Gamma,{[{a}]}P,{[{b}]}P}\vdash{\Delta}}{{\Gamma,{[{{a}\cup{b}}]}P}\vdash{\Delta}}

⊢ x > 0 \to [(? x > 1; x : = x - 1) \cup x^{'} = v] x > 0

⊢ x > 0 \to [(? x > 1; x : = x - 1) \cup x^{'} = v] x > 0

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash f()=g()\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CQ}}}$}&{}\hfil~{}&\vdash C\{p(f())\}\leftrightarrow C\{p(g())\}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash f()=g()\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CQ}}}$}&{}\hfil~{}&\vdash C\{p(f())\}\leftrightarrow C\{p(g())\}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash P\leftrightarrow Q\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CE}}}$}&{}\hfil~{}&\vdash C\{P\}\leftrightarrow C\{Q\}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash P\leftrightarrow Q\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CE}}}$}&{}\hfil~{}&\vdash C\{P\}\leftrightarrow C\{Q\}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash y>2\land 7>5\end{array}~{}&\quad{\quad\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:axiomAssignb}}}$}&{}\hfil~{}&\vdash\phantom{y>2\land\,}{[{x\mathrel{{:}{=}}f()}]}p(x)\leftrightarrow p(f())\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:us}}}$}&{}\hfil~{}&\vdash\phantom{y>2\land{}}{[{x\mathrel{{:}{=}}7}]}x>5\leftrightarrow\phantom{y>2\land{}}7>5\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CE}}}$}&{}\hfil~{}&\vdash y>2\land{[{x\mathrel{{:}{=}}7}]}x>5\leftrightarrow y>2\land 7>5\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:cutAt}}}$}&{}\hfil~{}&\vdash y>2\land\underbrace{{[{x\mathrel{{:}{=}}7}]}x>5}_{\_}{\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\textstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\scriptstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash y>2\land 7>5\end{array}~{}&\quad{\quad\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:axiomAssignb}}}$}&{}\hfil~{}&\vdash\phantom{y>2\land\,}{[{x\mathrel{{:}{=}}f()}]}p(x)\leftrightarrow p(f())\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:us}}}$}&{}\hfil~{}&\vdash\phantom{y>2\land{}}{[{x\mathrel{{:}{=}}7}]}x>5\leftrightarrow\phantom{y>2\land{}}7>5\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:CE}}}$}&{}\hfil~{}&\vdash y>2\land{[{x\mathrel{{:}{=}}7}]}x>5\leftrightarrow y>2\land 7>5\end{array}}\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:cutAt}}}$}&{}\hfil~{}&\vdash y>2\land\underbrace{{[{x\mathrel{{:}{=}}7}]}x>5}_{\_}{\mathchoice{\hbox to0.0pt{\hss$\displaystyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\textstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\scriptstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}{\hbox to0.0pt{\hss$\scriptscriptstyle{\text{unifies with underlined key in axiom }\underline{{[{x\mathrel{{:}{=}}f()}]}p(x)}\leftrightarrow p(f())~{}\leadsto~{}\text{replace with }p(f())\text{, which is }7>5}$\hss}}}\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash P\rightarrow({[{x^{\prime}=2}]}x\geq 5)\lor Q\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:useAt}}}$}&{}\hfil~{}&\vdash P\rightarrow(\underbrace{{[{{x^{\prime}=2}\cup{x\mathrel{{:}{=}}5}}]}x\geq 5}_{\_}{{[{\beta}]}B\rightarrow(\underline{{[{{\alpha}\cup{\beta}}]}B}\leftrightarrow{[{\alpha}]}B)})\lor Q\end{array}

\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&{}\hfil~{}&\vdash P\rightarrow({[{x^{\prime}=2}]}x\geq 5)\lor Q\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:useAt}}}$}&{}\hfil~{}&\vdash P\rightarrow(\underbrace{{[{{x^{\prime}=2}\cup{x\mathrel{{:}{=}}5}}]}x\geq 5}_{\_}{{[{\beta}]}B\rightarrow(\underline{{[{{\alpha}\cup{\beta}}]}B}\leftrightarrow{[{\alpha}]}B)})\lor Q\end{array}

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Full text

Concepts on Usability in Hybrid Systems Theorem Proving

Stefan Mitsch

Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

[email protected]

Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

André Platzer

Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

[email protected]

Abstract

Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights.

This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface design could be evaluated and anecdotal observations about it.

1 Introduction

Cyber-physical systems such as cars, aircraft, and robots combine computation and physics, and provide exceedingly interesting and important verification challenges. KeYmaera X [12] is a theorem prover for hybrid systems, i. e., systems with interacting discrete and continuous dynamics, which arise in virtually all mathematical models of cyber-physical systems.111KeYmaera X is available at http://keymaeraX.org/ It implements differential dynamic logic (d $\mathcal{L}$ [24, 25, 28]) for hybrid programs, a program notation for hybrid systems. Differential dynamic logic provides compositional techniques for proving properties about hybrid systems. Despite the substantial advances in automation, user input is often quite important, since hybrid systems verification is not semidecidable [24]. Human insight is needed most notably for finding invariants for loop induction and finding differential invariants for unsolvable differential equations [25]. But even some of the perfectly decidable questions in hybrid systems verification are intractable in practice, such as the final step of checking the validity of formulas in real arithmetic222Decision procedures are doubly exponential in the number of quantifier alternations [10], and practical implementations doubly exponential in the number of variables. in a d $\mathcal{L}$ proof.

To overcome those verification challenges, KeYmaera X combines automation and interaction capabilities to enable users to verify their applications even if they are still out of reach for state-of-the-art automation techniques. The central question in usability, thus, is how interaction and automation can jointly solve verification challenges. For isolated strategic aspects of the proofs, such user guidance is easily separated, for example when using system insights to provide loop invariants and differential invariants. Other aspects of human insights are more invasive, such as picking and transforming relevant formulas to make intractable arithmetic tractable. Users have to link the logical level of proving (e. g., the conjecture, available proof rules and axioms) to the abstract interaction level (e. g., visualization of formulas in a sequent) and decide about concrete interaction steps (e. g., where to click, what to type) [4]. Hence, going back and forth between automated proof tactics and user guidance poses several challenges:

•

Users need to be provided with a way of understanding the proof state produced by automated tactics. What are the open proof goals? How are these goals related to the proof of the conclusion? And why did the automated tactic stop making progress?

•

Users need to be provided with efficient ways of understanding the options for making progress. What tactics are available and where can they be applied? What input is needed? And what interactions provide genuinely new insights into a proof that the automation would not have tried?

•

Users need efficient tools for executing proof steps. How to provide gradual progress for novices? How to let experienced users operate with minimal input? How to reuse proof steps across similar goals? And how to generalize a specific tactic script into a proof search procedure for similar problems?

Users may additionally benefit from picking an appropriate interaction paradigms, such as proof as programming, proof by pointing, or proof by structure editing [4].

This paper discusses how KeYmaera X addresses these challenges through its web-based user interface. The complexity of larger hybrid systems verification challenges require that users be granted significant control over how a proof is conducted and what heuristics are applied for proof search. To this end, KeYmaera X separates user interaction and proof search from the actual proof steps in the prover kernel to ensure soundness while providing reasoning flexibility [12]. All proof steps follow from a small set of axioms by uniform substitution [27, 28]. This paper further introduces an evaluation concept to determine how effectively alternative user interaction concepts implemented in KeYmaera X address these challenges, as well as whether or not the combination of these concepts compare favorably to our previous hybrid systems theorem prover KeYmaera [29]. The experiments are yet to be conducted; our reports on the effectiveness of the user interaction concept remain anecdotal based on feedback from external users and students.

2 Preliminaries: Differential Dynamic Logic

This section recalls the syntax and semantics of differential dynamic logic by example of the motion of a person on an escalator. This example serves for illustrating prover interaction throughout the paper.

Syntax and semantics by example.

Suppose a person is standing on an escalator, which moves upwards with non-negative speed $v{\geq}0$ , so the person’s vertical position $x$ follows the differential equation $x^{\prime}=v$ . If the person is not at the bottom-most step ( $?x{>}1$ ), she may step down one step ( $x\mathrel{{:}{=}}x-1$ ) or may just continue moving upwards; since she may or may not step down, even if allowed, we use a non-deterministic choice ( $\cup$ ). We want to prove that the person never falls off the bottom end of the escalator ( $x{\geq}0$ ) when stepping down and moving upwards are repeated arbitrarily often (modeled with the repetition operator ∗).

[TABLE]

The formula (1) captures this example as a safety property in d $\mathcal{L}$ . Suppose, the person is initially at some position $x\geq 2$ when the escalator turns on. From any state satisfying the initial conditions $x\geq 2\land v\geq 0$ , all runs of the hybrid program ${({(?x>1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v})}^{*}$ reach only states that satisfy the safety condition $x\geq 0$ . More detailed examples on modeling hybrid systems are in [30].

Manual proof in d $\mathcal{L}$ .

Formulas in d $\mathcal{L}$ , such as the simple example (1), can be proved with the d $\mathcal{L}$ proof calculus. Proofs in d $\mathcal{L}$ are sequent proofs: a sequent has the shape ${\Gamma}\vdash{\Delta}$ , where we assume all formulas $\Gamma$ in the antecedent (to the left of the turnstile ${{}}\vdash{{}}$ ) to show any of the formulas $\Delta$ in the succedent (right of the turnstile). The sequent notation works from the desired conclusion at the bottom toward the resulting subgoals at the top. While sometimes surprising for novices, this notation emphasizes how the truth of the conclusions follows from the truth of their respective premises top-down. This notation also highlights the current subquestion at the very top of the deduction. Steps in the sequent proof are visualized through a horizontal line, which separates the conclusion at the bottom from the premises at the top. The name of the deduction step is annotated to the left of the horizontal line. For example, the proof rule ${[{\cup}]}$ says that to conclude safety of a non-deterministic choice of programs ${\alpha}\cup{\beta}$ (below the bar) it suffices to prove safety of both $\alpha$ and $\beta$ individually (above bar).

[TABLE]

Manual proof example.

Starting from the formula (1) at the very bottom of the deduction, we develop a safety proof as follows. As first step, the rule $\rightarrow\textsf{R}$ moves the assumptions from the left-hand side of an implication into the antecedent. Next $\land\textsf{L}$ splits the conjunction $x\geq 2\land v\geq 0$ into individual facts (i. e., we get to assume both, $x\geq 2$ and $v\geq 0$ individually). Then, we use loop induction with the invariant $x>0$ . We have to show three cases: the loop invariant must hold initially (base case $x\geq 2\rightarrow x>0$ ), it must be strong enough to entail safety (use case $x>0\rightarrow x\geq 0$ ), and it must be preserved by the loop body (induction step ${[{{(?x>1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v}}]}x>0$ ).

[TABLE]

Here, the base case and use case can be shown easily using quantifier elimination QE. The induction step proceeds using the proof rule ${[{\cup}]}$ for non-deterministic choice that we saw above, followed by $\land\textsf{R}$ to split the induction step proof into two branches. On the first branch, we first turn the sequential composition (;) into nested boxes ( ${[{?x>1}]}{[{x\mathrel{{:}{=}}x-1}]}x>0$ ), and then use the test condition ( $x>1$ ) as an additional assumption using rule ${[{?}]}$ followed by $\rightarrow\textsf{R}$ . We show safety of the assignment $x\mathrel{{:}{=}}x-1$ using quantifier elimination QE to close the proof. On the second branch, we show safety of the differential equation $x^{\prime}=v$ using the proof rule ODE followed by QE. ∎

3 KeYmaera X Proof Automation

As a basis for understanding how KeYmaera X searches for proofs and where and why it asks for user guidance, this section gives a high-level explanation of KeYmaera X tactics.

KeYmaera X automates the tedious task of proving steps that follow unambiguously from the structure of the conjecture. It further provides (heuristic) tactics to generate and explore invariant candidates for loop induction and differential equations. One might imagine KeYmaera X to try to solve differential equations and use the solution to guide a differential invariant proof, before it resorts to more involved differential invariant proofs. KeYmaera X provides proof tactics for propositional reasoning, reasoning about hybrid programs, and closing (arithmetic) proof goals, which are combined into a fully automated proof search tactic. For example, with a loop invariant candidate annotated in the KeYmaera X input file, the running example in this paper proves fully automated.

Propositional reasoning prop and program unfolding unfold of hybrid programs follows along propositional sequent rules and the axioms of d $\mathcal{L}$ . These tactics successively match on the shape of a formula to transform it into simpler parts, before the tactics descend into the resulting parts. Program unfolding focuses on the decidable fragment of reasoning about hybrid programs: it stops and asks for user guidance when it encounters loops or ODEs. The following proof snippet applies unfold to just the induction step of the escalator proof.

Induction step by unfold.

The tactic unfold applies hybrid program axioms and splits conjunctions in the succedent into proof branches, but stops when it encounters loops or ODEs. The resulting two subgoals correspond to the two (logically unfolded) paths through our running example: we have to show safety of the discrete assignment $x\mathrel{{:}{=}}x-1$ as well as of the differential equation $x^{\prime}=v$ .

[TABLE]

∎

KeYmaera X ships with proof search tactic auto, which combines propositional reasoning with program unfolding, loop invariant exploration, certain automated proof techniques for differential equations, and proof closing by quantifier elimination. Even though the auto tactic finds proofs for important classes of hybrid systems automatically, it still may stop exploration and ask for user guidance in complicated cases (e. g., when none of the explored differential invariants helps closing the proof).

4 KeYmaera X User Interaction

When the automated tactics shipped with KeYmaera X fail to find a proof (due to a wrong model, missing loop or differential invariants, or intractable arithmetic), user interaction is needed to improve the model and make progress with the proof. This section introduces the KeYmaera X user interaction concepts and their implementation in a graphical web-based user interface. The user interface of KeYmaera X is based on these principles and hypotheses:

Familiarity

Prover user interfaces benefit from a familiar look&feel that resembles how proofs are conducted in theoretical developments and that are compatible with the way that proof rules are presented.

Traceability

Sophisticated verification challenges, especially in hybrid systems, need a way of mixing automation with user guidance in a way that the user can trace and understand the respective remaining questions.

Tutoring

Interactive proof-by-pointing at formulas and terms are an efficient way of learning how to conduct proofs and help internalizing reasoning principles by observation. Tactic recording is an efficient way of learning how to write tactics by observing to which interactive proof steps they correspond.

Flexibility

Humans reason in more flexible ways than automation procedures. User interfaces should allow proof steps at any part of a proof as well as free-style transformations of formulas, and they should embrace multiple reasoning styles, such as explicit proofs, proof-by-pointing, and proof-by-search.

Experimentation

A strict separation of prover core and prover interface not only helps soundness, but also enables more agile experimentation with new styles of conducting proofs and of interacting with provers.

Figure 1 shows a screenshot of the KeYmaera X user interface with user interface elements annotated by their interaction purpose. We discuss these design choices in more detail in the following paragraphs.

4.1 Familiarity

The KeYmaera X prover kernel implements Hilbert-style proofs by uniform substitution from a small set of locally sound axioms [28] together with a first-order sequent calculus [24]. The user interface of KeYmaera X presents proofs in sequent form as in Figure 2, which enables users to equivalently read the logical transformations as either sequent proof rule uses [24] or axiom uses [28]. The rendering is consistent with the notation used in Section 2 and in the Foundations of Cyber-Physical Systems course [26], which should make it easy to switch between proof development on paper and proving in KeYmaera X. Proof suggestions for tactics are rendered by their primary nature either as axioms (e. g., the d $\mathcal{L}$ axiom ${[{\cup}]}$ , see Figure 2b), proof rules (e. g., the propositional proof rule $\land\textsf{L}$ , see Figure 2c), or proof rules with input (e. g., the sequent proof rule loop, which requires input, combines multiple axioms in a tactic to implement a proof rule, and creates multiple subgoals, see Figure 2d).

The hypothesis is that the ability to work from a small number of reasoning principles, which is crucial for a small prover core, helps human understanding as well. The experience with the Foundations of Cyber-Physical Systems course [26], in which KeYmaera and KeYmaera X have been used, suggests that equivalence axioms indeed make it easier for students to understand reasoning principles than explicit sequent proof rules [24], which obscure inherent dualities for novices. For example, the equivalence $\boldsymbol{{[{{a}\cup{b}}]}P}\leftrightarrow{[{a}]}P\land{[{b}]}P$ characterizes nondeterministic choices under all circumstances. Its conjunction $\land$ and the rules for $\land$ make it apparent that such nondeterministic choices will branch in the succedent but not in the antecedent:

[TABLE]

Of course, it is exactly the same reasoning principle either way, but understanding the direct sequent proof rules still requires two logical principles at once compared to the single axiom.

4.2 Traceability

When switching from automated mode to user guidance, it is important to visualize just enough contextual information about the open proof goals to understand where the present subgoals came from and how they relate to the proof of the ultimate conclusion. KeYmaera X shows local views of proofs that illustrate the way how the current question came about and how it is related to the proof of the conclusion. The idea is that this enables traceability and gives local justifications while limiting information to the presently relevant part of the proof.

Visualizing the proof state.

Visualizing the entire proof tree that unfolds from the original conjecture as tree root is not a viable option, since proofs in d $\mathcal{L}$ unfold into many branches and therefore easily exceed the screen width when rendered in a single tree. Even simple models, such as the escalator example with only four branches (induction base case, induction use case, and stepping down plus moving upwards in the induction step) become hard to navigate and keep track of when both horizontal and vertical scrolling is needed. KeYmaera X, therefore, renders a proof tree in sequent deduction paths from the tree root representing the original conjecture at the bottom of the screen to a leave representing an open goal at the top, see Figure 1.

The sequent deduction paths are arranged in tabs; branching occurs when a deduction step has more than one premise, so that premises are spread over multiple tabs and interconnected with links between the tabs.

Proof navigation.

Users can focus solely on the open goal by collapsing the entire deduction path ( $\boxminus$ ), or they can keep some part of the proof structure visible, e. g., by collapsing only between branching points in the proof, see Figure 1. Triangles left of the sequent path identify groups: when uncollapsed, down/up arrows ( $\asymp$ ) indicate the group borders; when collapsed ( $\rangle$ ), the steps in a group are abbreviated into “…”. Additionally, sequents can be expanded over multiple lines ( $\blacktriangledown$ , one formula per line) or collapsed into a single line ( $\blacktriangleright$ ).

When proof automation hands over to the user, the topmost line in a sequent deduction path represents an open goal. This means that either the goal cannot be proved at all because the model is wrong, or it is not yet proved because user guidance is needed. In the former case, the counterexample tool allows users to find concrete values that make all formulas on the left of the sequent true but violate all formulas on the right. In the latter case, users are interested in what to do next (see Section 4.3).

4.3 Tutoring

Suggesting possible proof steps.

KeYmaera X analyzes the shape of formulas to suggest proof steps on demand. A tactic comes with a description of the shape of its conclusion (must match the current open goal so that the tactic is applicable), a description of the premises that remain to be proved after applying the tactic, and a description of required user input (such as invariants for loops). Such meta-information allows tactic suggestion in two different flavors, as depicted in Figure 3:

•

When users know where to continue with the proof (i. e., exactly on which formula or term or part thereof), KeYmaera X displays a dialog with important applicable tactics and their required input, which resembles the user interaction of KeY [2, 3] and its hybrid systems descendant KeYmaera [29].

•

When users know what to do next, KeYmaera X searches for formulas or terms where the desired tactic is applicable.

For example, when pointing to a loop, KeYmaera X suggests the induction tactic loop as well as loop unrolling $[{}^{*}]$ as shown in Figure 3. The tactic loop requires a loop invariant $j(x)$ as input and produces three branches that remain to be proved to conclude safety of the program with the loop. Loop unrolling $[{}^{*}]$ turns a formula of the shape in boldface (left-hand side $\boldsymbol{{[{{\alpha}^{*}}]}P}$ of the equivalence) into a formula of the right-hand side $P\land{[{\alpha}]}{[{{\alpha}^{*}}]}P$ of the equivalence.

For reasons of flexibility, KeYmaera X supports contextual reasoning to apply axioms deeply nested inside a formula, not only on the top-level operator as in Figure 3. As a consequence, users may have many options to work on a single formula. In the induction step of the escalator example

[TABLE]

we used $\rightarrow\textsf{R}$ top-level to get ${x{>}0}\vdash{{[{{(?x{>}1;x\mathrel{{:}{=}}x-1)}\cup{x^{\prime}=v}}]}x{>}0}$ as a next goal. Alternatively, the non-deterministic choice tactic ${[{\cup}]}$ on the right-hand side of the implication would result in a conjunction ${{}}\vdash{x{>}0\rightarrow{[{?x{>}1;x\mathrel{{:}{=}}x-1}]}x{>}0\land{[{x^{\prime}=v}]}x{>}0}$ .

For novice users, it is often easiest to focus on the top-level operator and work on formulas outside-in, i. e., apply $\rightarrow\textsf{R}$ first and then ${[{\cup}]}$ next. But it quickly becomes more convenient to apply proof rules in any order anywhere in the middle of the formulas to follow whatever line of thought the user may have in mind. Such proofs in arbitrary order also often reduce the branching or repetition of proof steps in different branches.

Tactic extraction.

In order to conduct proofs effectively, interactive theorem provers typically ship with extensive tactic libraries (e. g., Coq [21], Isabelle [23]), accompanied with library documentation and examples to facilitate learning. Still, extensive tactic libraries incur a steep learning curve. We conjecture that observing how tactics evolve while doing a proof (similar to observing an expert) can reduce the steep learning curve associated with extensive tactic libraries. KeYmaera X automatically generates tactics that correspond to the point-and-click interaction that the user performed and displays these tactics below the graphical sequent view, see Figure 4.

The graphical sequent view and the tactic editor operate on the same proof, so that users can switch between both interaction concepts as they see fit. As a rule of thumb, the sequent view is designed for conducting specific steps at specific positions (e. g., use a specific equality $x=y$ to rewrite $x$ into $y$ in some other term), while the tactic editor is intended for describing proof search (e. g., repeat some step exhaustively $\land\textsf{L('L)*}$ or follow a high-level proof strategy such as unfold & ODE & QE).

4.4 Flexibility

To allow users to reason in flexible ways and reduce manual proof effort, KeYmaera X supports proof steps by pointing at formula parts and lets users transform and abbreviate formulas as well as execute tactic scripts. As underlying technique for proof-by-pointing and flexible reasoning anywhere in formulas, KeYmaera X provides contextual reasoning CQ and CE [28], so that questions about contextual equality or equivalence in a context $C\{\dots\}$ reduce to reasoning about arguments as follows.

[TABLE]

When contextual reasoning is combined with uniform substitution US and axiom lookup, axioms can be applied inside formulas, which enables proof by pointing at the desired formula part. Often, the next proof step follows unambiguously from just the shape of the pointed formula part by indexing [28], so that the proof advances without further user input.

[TABLE]

Note that side branches with contextual reasoning, uniform substitution, and axiom lookup (as in the proof above) close fully automatically. Hence, the user interface displays only the result of applying axioms by pointing, while it hides the minutia of the side deductions from the user as in the following example.

[TABLE]

4.5 Experimentation

The prover kernel and the prover interface are strictly separated, to the extent that the prover kernel only knows about making single deduction steps and combining them, but is completely oblivious of organizing these steps in a tree structure. For soundness, it suffices to know that any step between the original conjecture and the current subgoals must have been done in the prover kernel. Intermediate steps are only necessary to repeat a proof from the original conjecture, and can therefore be tracked outside the prover kernel. As a result, proof organization features (such as undoing proof steps, pruning the proof tree) can be implemented conveniently in the user interface without affecting soundness.

The separation between the prover core and the tactics becomes especially useful when adding compiled tactics to the server-side implementation. Complementing the interpreted tactics from the web-based user interface, server-side tactics can base on a rich implementation language (Scala) to try proof steps that are only sound in the usual cases and just rely on the prover core to catch when they happen to be applied in one of the unsound corner cases.

5 Evaluation Concept

Compared to its predecessor KeYmaera [29], the clean-slate implementation KeYmaera X introduces significant changes in user interaction. Although the user interaction changes are based on informal feedback from KeYmaera users and our own observations on how students used KeYmaera, it still remains to be checked by an experimental user study which style of user interaction is more effective. Additionally, KeYmaera X introduces new interaction concepts (e. g., tactic programming and tactic recording), which seem promising for experienced users to conduct large proofs, but are not yet backed by evidence that indeed prover interaction is improved compared to only mouse-based interaction. Similar user-related research questions were addressed in a recent controlled user experiment [14], which followed methods from empirical software engineering [33] to compare two very different user interfaces of the KeY theorem prover [2, 3]. The obtained results are encouraging pointers towards controlled user experiments being an appropriate method for testing theorem prover interaction.

Such controlled experiments, however, require a large number of participants with varying experience and deliberately exposing them to different user interaction concepts. In order to avoid adverse effects from pre-assigned interaction styles, we propose gathering data from normal operation on how often users rely on certain interaction patterns (e. g., clicking vs. automated tactic), how often they use a certain functionality during a proof, and how successful they were, even if that might lead to selection bias. Learnability of theorem provers can be measured based on cognitive dimensions [9], such as visibility (how easy are relevant steps accessed), juxtaposability (different notations side-by-side), viscosity (resistance to change), premature commitment (to an order how to do steps), error-proneness (how likely are errors), and consistency (similar information presented in similar ways). Theorem provers, especially in education and also in industrial applications, should have high visibility and juxtaposability, high consistency, and low viscosity [13]. The following metrics should be easily recordable from KeYmaera X without changing user interaction and give insights into cognitive dimensions.

Interaction concept

Number of proof steps by clicking/tactic programming/automated proof search. Supporting evidence: number of proof steps at top-level/inside formulas; for clicking: number of steps executed by pointing/from tactic suggestion. Related to visibility and premature commitment.

Functionality

Number of undo operations, length of pruned deduction paths with distance to next branching point above and below, number of find counterexample operations. Number of interactions in pruned proofs. Related to viscosity and error-proneness.

Time

Proof duration (including estimates of user time and number of reproof attempts)

Trends

Compare trends as students gain experience and examples become more complex

We believe this data should enable a study that tests the following hypotheses.

Interaction preference

Novice users prefer automated proof search over clicking over tactic programming. Novice users prefer working top-level over working inside formulas. Experienced users balance interaction.

Functionality

Novice users either undo short paths or entire proofs and end up with more open branches. Experienced users undo branching and exercise branching control techniques.

Trends

Automated usage drops with increased example complexity and student experience, while use of tactic programming increases; the focus on applying steps top-level drops while applying steps inside formulas increases with experience.

Influence

Students that engage more direct control over proofs also for simpler examples are more productive in conducting proofs of complex cases than students who relied on full automation earlier on.

The quantitative insights from these metrics could be augmented with qualitative evaluation techniques, as demonstrated being effective for theorem provers, e. g., with focus groups [8] (users subjectively express their perception of or opinion on the user interface), with questionnaires [7], or by co-operative evaluation [16] (users verbalize their interactions while using the theorem prover).

6 Related Work

The verification landscape spans a wide variety of approaches from automated theorem provers and reachability analysis tools to interactive theorem provers.

Automated theorem provers (e. g., Vampire [17]) and reachability analysis tools (e. g., SpaceEx [11]) strive for fully automatic verification without user interaction, but their scope is inherently limited in cases that are not semidecidable, such as hybrid systems.

Auto-active verifiers (e. g., Dafny [18, 19], AutoProof [31]) put the model or code first and hide the verification engine, but support user guidance through annotations in the code. The basic idea is to make verification an integral part of (software) development that should be performed in the background by an IDE, much like background compilation. The downside of such an approach is that the verification steps are hidden entirely from the user, which can make it hard to resolve proofs with additional annotations when the verifier is stuck because the proof state and the verifier’s working principles are opaque. The KeY interactive verification debugger [15] combines code annotations with interactive verification in KeY [2, 3] to supplement manual proofs when automated proving fails at some goals.

Interactive theorem provers, such as Coq [21] and Isabelle [23], primarily interact with users through tactic scripts, such as structured proofs in Isabelle/Isar [22]. Their user interfaces (e. g., CoqIDE [21], ProofGeneral [6], jEdit [32]) focus on text editing support for writing tactics and let users inspect the proof state and open goals by placing the cursor in the tactic script. Navigation with cursors introduced a limited form of proof by pointing [5] to fold or unfold equations. KeYmaera X advances proof-by-pointing to transform all or parts of a formula following the shape of an axiom or fact. PeaCoq333http://goto.ucsd.edu/peacoq/ aims to make the proof state more accessible to users by providing a proof tree.

KeYmaera X combines concepts from automated, auto-active, and interactive theorem proving: it comes with fully automated proof search tactics for hybrid systems of limited scope (i. e., when a loop invariant can be found, a symbolic solution of a differential equation can be found to serve as an oracle for differential invariants, and the resulting arithmetic is tractable); it supports annotations for loop invariants and differential invariants, since both serve as model documentation as well as proof guidance; and finally, it allows users to conduct and finish proofs themselves with tactics and a graphical user interface.

7 Conclusion

The user interface of KeYmaera X is based on the principles of familiarity, traceability, tutoring, flexibility, and experimentation. It supports several different user interaction styles to make progress in proofs. The web-based user interface applies proof steps when clicking on formulas in the sequent view, and it batch-runs proof steps by automated search tactics as well as through tactic programming.

Future work includes evaluation in controlled user experiments, as described in the evaluation concept. On the basis of user studies, we expect to gain insights into how to best teach hybrid systems theorem proving, tactic programming, tactic generalization, and proof search. We are working on improved proof exploration, e.g., with timeouts (e. g., allow QE 5s to close; if it does not close within the budgeted time, try something else). Failed proof attempts or expired timeouts need a robust approach to making proofs portable and repeatable.

Acknowledgments

The authors thank Nathan Fulton, Brandon Bohrer, Jan-David Quesel, Ran Ji, and Marcus Völp for their support in implementing KeYmaera X, Sarah Loos, Jean-Baptiste Jeannin, João Martins, Khalil Ghorbal, and Sarah Grebing for feedback and discussions on the user interface, as well as the anonymous reviewers for feedback on the manuscript.

This material is based on research sponsored by DARPA under agreement DARPA FA8750-12-2-0291.

Bibliography33

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1]
2[2] Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager & Peter H. Schmitt (2005): The Ke Y tool . Software and System Modeling 4(1), pp. 32–54, 10.1007/s 10270-004-0058-x . · doi ↗
3[3] Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt & Mattias Ulbrich (2014): The Ke Y Platform for Verification and Analysis of Java Programs . In Dimitra Giannakopoulou & Daniel Kroening, editors: Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17- · doi ↗
4[4] J. Stuart Aitken, Philip D. Gray, Thomas F. Melham & Muffy Thomas (1998): Interactive Theorem Proving: An Empirical Study of User Activity . J. Symb. Comput. 25(2), pp. 263–284, 10.1006/jsco.1997.0175 . · doi ↗
5[5] David Aspinall & Christoph Lüth (2004): Proof General meets Isa Win: Combining Text-Based And Graphical User Interfaces . Electr. Notes Theor. Comput. Sci. 103, pp. 3–26, 10.1016/j.entcs.2004.09.011 . · doi ↗
6[6] David Aspinall, Christoph Lüth & Daniel Winterstein (2007): A Framework for Interactive Proof . In Manuel Kauers, Manfred Kerber, Robert Miner & Wolfgang Windsteiger, editors: Towards Mechanized Math. Assistants, 14th Symp., Calculemus, 6th Int. Conf., MKM, Hagenberg, Austria, June 27-30, 2007, Proc. , LNCS 4573, Springer, pp. 161–175, 10.1007/978-3-540-73086-615 . · doi ↗
7[7] Bernhard Beckert & Sarah Grebing (2012): Evaluating the Usability of Interactive Verification Systems . In Vladimir Klebanov, Bernhard Beckert, Armin Biere & Geoff Sutcliffe, editors: Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, United Kingdom, June 30, 2012 , CEUR Workshop Proceedings 873, CEUR-WS.org, pp. 3–17.
8[8] Bernhard Beckert, Sarah Grebing & Florian Böhl (2014): A Usability Evaluation of Interactive Theorem Provers Using Focus Groups . In Carlos Canal & Akram Idani, editors: Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops: HOFM, SAFOME, Open Cert, Mo K Ma SD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers , LNCS 8938, Springer, pp. 3–19, 10.1007/978-3-319-15201-11 . · doi ↗

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

The KeYmaera X Proof IDE

Abstract

1 Introduction

2 Preliminaries: Differential Dynamic Logic

Syntax and semantics by example.

Manual proof in dL\mathcal{L}L.

Manual proof example.

3 KeYmaera X Proof Automation

Induction step by unfold.

4 KeYmaera X User Interaction

4.1 Familiarity

4.2 Traceability

Visualizing the proof state.

Proof navigation.

4.3 Tutoring

Suggesting possible proof steps.

Tactic extraction.

4.4 Flexibility

4.5 Experimentation

5 Evaluation Concept

6 Related Work

7 Conclusion

Acknowledgments

Manual proof in d $\mathcal{L}$ .