Skip to content
Snippets Groups Projects
Commit 1e3fd58e authored by Daniel Plagge's avatar Daniel Plagge
Browse files

added reference to Stefan Hallerstede's proof obligation paper

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15974 1434b563-b632-4741-aa49-43a3a8374d2e
parent cd331c87
No related branches found
No related tags found
No related merge requests found
...@@ -223,8 +223,13 @@ Those interested in more general guidelines on how to develop and structure form ...@@ -223,8 +223,13 @@ Those interested in more general guidelines on how to develop and structure form
\subsection{Proofs for the Working Engineer (2008)} \subsection{Proofs for the Working Engineer (2008)}
In his dissertation at the ETH Zurich Fahrad Mehta describes how theorem proving In his dissertation at the ETH Zurich Fahrad Mehta describes how theorem proving
can be a practical tool for an engineer and presented the ideas that are used can be a practical tool for software engineers and presents the ideas that are used
in building the fundament of Rodin. in building Rodin's infrastructure.
\subsection{The Proof Obligation Generator (2005)}
In this technical report (ETH Zürich) Stefan Hallerstede describes which proof obligations
(see Section~\ref{generated_proof_obligations}) are generated for a model
and gives a justification why these are correct.
\section{Conventions} \section{Conventions}
\label{conventions} \label{conventions}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment