diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md
new file mode 100644
index 00000000000..05df421b0c9
--- /dev/null
+++ b/doc/assets/xml_spec.md
@@ -0,0 +1,443 @@
+XML Specification for CBMC Traces
+=================================
+
+Traces of GOTO programs consist of *steps*, i.e. steps are elements of
+the XML object.
+
+Trace Step Types
+----------------
+
+- assignment
+
+- assume
+
+- assert
+
+- goto instruction
+
+- function call
+
+- function return
+
+- output
+
+- input
+
+- declaration
+
+- dead statement
+
+- spawn statement
+
+- memory barrier
+
+unused:
+
+- constraint
+
+- location
+
+- shared read
+
+- shared write
+
+- atomic begin
+
+- atomic end
+
+Source Location
+---------------
+
+Every trace step optionally contains the source location as an element.
+
+**Attributes** (all are optional):
+
+- `working-directory`: string of the full path
+
+- `file`: name of the file containing this location
+
+- `line`: non-negative integer
+
+- `column`: non-negative integer
+
+- `function`: name of the function this line belongs to
+
+**Example**:
+
+``` {.xml}
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+```
+
+Trace Steps in XML
+------------------
+
+The attributes `hidden, thread, step_nr` are common to all trace steps.
+
+``` {.xml}
+
+
+
+
+
+```
+
+Assert (element name: `failure`)
+
+**Attributes**:
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+- `reason`: comment (string)
+
+- `property`: property ID (irep\_idt)
+
+**Example**:
+
+``` {.xml}
+
+
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+```
+
+Assignment, Declaration (element name: `assignment`)
+
+**Attributes**:\
+if the lhs symbol is known
+
+- `mode`: {C, Java, ...}
+
+- `identifier`: string (symbol name)
+
+- `base_name`: string (e.g. "counter")
+
+- `display_name`: string (e.g. "main::1::counter")
+
+always present
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+- `assignment_type`: {actual\_parameter, state}
+
+**Elements**:\
+if the lhs symbol is known
+
+- `type`: C type (e.g. "signed int")
+
+always present
+
+- `full_lhs`: original lhs expression (after dereferencing)
+
+- `full_lhs_value`: a constant with the new value
+
+**Example**:
+
+``` {.xml}
+
+
+ signed int
+ b
+ -1879048192
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+Input (element name: `input`)
+
+**Attributes**:
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+**Elements**:
+
+- `input_id`: IO id (the variable name)
+
+for each IO argument
+
+- `value`: the (correctly typed) value the input is initialised with
+
+- `value_expression`: the internal representation of the value
+
+**Example**:
+
+``` {.xml}
+
+ i
+ -2147145201
+
+
+ -2147145201
+
+
+
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+Output (element name: `output`)
+
+**Attributes**:
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+**Elements**:
+
+- `text`: formatted list of IO arguments
+
+for each IO argument
+
+- `text`: The textual representation of the output
+
+- `location`: The original source location of the output
+
+- `value`: the (correctly typed) value of the object that is being
+ output
+
+- `value_expression`: the internal representation of the value
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+Function Call (element name: `function_call`)\
+Function Return (element name: `function_return`)
+
+**Attributes**:
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+**Elements**:
+
+- `function`: compound element containing the following\
+ Attributes:
+
+ - `display_name`: language specific pretty name
+
+ - `identifier`: the internal unique identifier
+
+ Elements:
+
+ - `location`: source location of the called function
+
+ - `function`: The function that is being called/returned from.
+
+**Example**:
+
+``` {.xml}
+
+
+
+
+
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+All Other Steps (element name: `location-only`)
+
+Only included if the source location exists and differs from the
+previous one.\
+**Attributes**:
+
+- `hidden`: boolean attribute
+
+- `thread`: thread number (positive integer)
+
+- `step_nr`: number in the trace (positive integer)
+
+**Elements**:
+
+- `location`: location of the called function
+
+**Example**:
+
+``` {.xml}
+
+
+
+```
+
+**XSD**:
+
+``` {.xml}
+
+
+
+
+
+
+
+
+```
+
+Full Trace XSD
+--------------
+
+``` {.xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+Notes
+-----
+
+The path from the input C code to XML trace goes through the following
+steps:\
+`C` → `GOTO` → `SSA` → `GOTO Trace` → `XML Trace`
+
+#### SSA to GOTO Trace
+
+SSA steps are sorted by clocks and the following steps are skipped: PHI,
+GUARD assignments; shared-read, shared-write, constraint, spawn,
+atomic-begin, atomic-end.
diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex
new file mode 100644
index 00000000000..8789c58e962
--- /dev/null
+++ b/doc/assets/xml_spec.tex
@@ -0,0 +1,421 @@
+\documentclass[12pt]{article}
+\usepackage{a4wide}
+\usepackage{minted}
+
+\begin{document}
+
+\section{XML Specification for CBMC Traces}
+
+Traces of GOTO programs consist of \emph{steps}, i.e. steps are elements of the
+XML object.
+
+\subsection{Trace Step Types}
+
+\begin{itemize}
+\item assignment
+\item assume
+\item assert
+\item goto instruction
+\item function call
+\item function return
+\item output
+\item input
+\item declaration
+\item dead statement
+\item spawn statement
+\item memory barrier
+\end{itemize}
+
+unused:
+\begin{itemize}
+\item constraint
+\item location
+\item shared read
+\item shared write
+\item atomic begin
+\item atomic end
+\end{itemize}
+
+\subsection{Source Location}
+
+\noindent Every trace step optionally contains the source location as an
+element.
+
+\noindent\textbf{Attributes} (all are optional):
+\begin{itemize}
+\item \texttt{working-directory}: string of the full path
+\item \texttt{file}: name of the file containing this location
+\item \texttt{line}: non-negative integer
+\item \texttt{column}: non-negative integer
+\item \texttt{function}: name of the function this line belongs to
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+\subsection{Trace Steps in XML}
+
+\noindent The attributes \texttt{hidden, thread, step\_nr} are common to all trace steps.
+
+\begin{minted}{xml}
+
+
+
+
+
+\end{minted}
+
+\begin{center}
+{\Large Assert} (element name: \texttt{failure})
+\end{center}
+
+\noindent\textbf{Attributes}:
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\item \texttt{reason}: comment (string)
+\item \texttt{property}: property ID (irep\_idt)
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+
+\begin{center}
+{\Large Assignment, Declaration} (element name: \texttt{assignment})
+\end{center}
+
+\noindent\textbf{Attributes}:\\
+if the lhs symbol is known
+\begin{itemize}
+\item \texttt{mode}: \{C, Java, …\}
+\item \texttt{identifier}: string (symbol name)
+\item \texttt{base\_name}: string (e.g. ``counter'')
+\item \texttt{display\_name}: string (e.g. ``main::1::counter'')
+\end{itemize}
+always present
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\item \texttt{assignment\_type}: \{actual\_parameter, state\}
+\end{itemize}
+
+\noindent\textbf{Elements}:\\
+if the lhs symbol is known
+\begin{itemize}
+\item \texttt{type}: C type (e.g. ``signed int'')
+\end{itemize}
+always present
+\begin{itemize}
+\item \texttt{full\_lhs}: original lhs expression (after dereferencing)
+\item \texttt{full\_lhs\_value}: a constant with the new value
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+
+ signed int
+ b
+ -1879048192
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+
+\begin{center}
+{\Large Input} (element name: \texttt{input})
+\end{center}
+
+\noindent\textbf{Attributes}:
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\end{itemize}
+
+\noindent\textbf{Elements}:
+\begin{itemize}
+\item \texttt{input\_id}: IO id (the variable name)
+\end{itemize}
+for each IO argument
+\begin{itemize}
+\item \texttt{value}: the (correctly typed) value the input is initialised with
+\item \texttt{value\_expression}: the internal representation of the value
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+ i
+ -2147145201
+
+
+ -2147145201
+
+
+
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+
+\begin{center}
+ {\Large Output} (element name: \texttt{output})
+\end{center}
+
+\noindent\textbf{Attributes}:
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\end{itemize}
+
+\noindent\textbf{Elements}:
+\begin{itemize}
+\item \texttt{text}: formatted list of IO arguments
+\end{itemize}
+for each IO argument
+\begin{itemize}
+\item \texttt{text}: The textual representation of the output
+\item \texttt{location}: The original source location of the output
+\item \texttt{value}: the (correctly typed) value of the object that is being output
+\item \texttt{value\_expression}: the internal representation of the value
+\end{itemize}
+
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+
+\begin{center}
+ {\Large Function Call} (element name: \texttt{function\_call})\\
+ {\Large Function Return} (element name: \texttt{function\_return})
+\end{center}
+
+\noindent\textbf{Attributes}:
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\end{itemize}
+
+\noindent\textbf{Elements}:
+\begin{itemize}
+\item \texttt{function}: compound element containing the following\\
+ Attributes:
+ \begin{itemize}
+ \item \texttt{display\_name}: language specific pretty name
+ \item \texttt{identifier}: the internal unique identifier
+ \end{itemize}
+ Elements:
+ \begin{itemize}
+ \item \texttt{location}: source location of the called function
+ \item \texttt{function}: The function that is being called/returned from.
+ \end{itemize}
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+
+
+
+
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+
+\begin{center}
+ {\Large All Other Steps} (element name: \texttt{location-only})
+\end{center}
+
+\noindent Only included if the source location exists and differs from the previous one.\\
+
+\noindent\textbf{Attributes}:
+\begin{itemize}
+\item \texttt{hidden}: boolean attribute
+\item \texttt{thread}: thread number (positive integer)
+\item \texttt{step\_nr}: number in the trace (positive integer)
+\end{itemize}
+
+\noindent\textbf{Elements}:
+\begin{itemize}
+\item \texttt{location}: location of the called function
+\end{itemize}
+
+\noindent\textbf{Example}:
+\begin{minted}{xml}
+
+
+
+\end{minted}
+
+\noindent\textbf{XSD}:
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+\end{minted}
+
+\subsection{Full Trace XSD}
+
+\begin{minted}{xml}
+
+
+
+
+
+
+
+
+
+
+
+
+
+\end{minted}
+
+\subsection{Notes}
+
+The path from the input C code to XML trace goes through the following steps:\\
+
+\texttt{C} → \texttt{GOTO} → \texttt{SSA} → \texttt{GOTO Trace} → \texttt{XML Trace}
+
+\paragraph{SSA to GOTO Trace}
+
+SSA steps are sorted by clocks and the following steps are skipped: PHI, GUARD
+assignments; shared-read, shared-write, constraint, spawn, atomic-begin,
+atomic-end.
+
+\end{document}
diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd
new file mode 100644
index 00000000000..1255c524022
--- /dev/null
+++ b/doc/assets/xml_spec.xsd
@@ -0,0 +1,180 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md
index 133f01cebb1..10a6660523d 100644
--- a/doc/cprover-manual/cbmc-tutorial.md
+++ b/doc/cprover-manual/cbmc-tutorial.md
@@ -130,6 +130,18 @@ access. If you add a branch to the example that requires that `argc>=3`,
the bug is fixed and CBMC will report that the proofs of all properties
have been successful.
+To simplify further processing of counterexample traces, CBMC supports XML as a
+possible output format.
+
+```
+ cbmc file1.c --trace --xml-ui
+```
+
+The specification of the XML trace output can be found here: [XML
+Specification](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/assets/xml_spec.tex)
+and can be build by `pdflatex -shell-escape xml_spec.tex`. Alternatively, you
+view it in Markdown [here](../../../assets/xml_spec).
+
### Verifying Modules
In the example above, we used a program that starts with a `main`