\definepapersize[stellingen][width=160mm, height=230mm]
\setuppapersize[stellingen]
\mainlanguage[nl]

%\showframe
\setuplayout
  [width=middle,
   height=middle,
   header=0mm,
   footer=0mm]
\setuppagenumbering[state=stop, alternative=singlesided]

\definefontfeature[default][default][expansion=quality,protrusion=quality,onum=yes,kern=yes,liga=yes]
\setupalign[hz,hanging]
\setupcolors[state=stop]

\definefontfamily[mainfamily] [rm] [TeX Gyre Pagella]
\definefontfamily[mainfamily] [mm] [Neo Euler] [rscale=0.95]
\definefontfamily[mainfamily] [tt] [Latin Modern Mono][rscale=1.03]
\setupbodyfont[mainfamily,11pt]

\setuphead[chapter][sectionsegments=chapter, command=\MyChapter, header=empty]
\define[2]\MyChapter{\midaligned{#2}}

\setupindenting[no]
\setupwhitespace[big]


\starttext

\startchapter
  [title={Stellingen}]

\startalignment[center]
Behorend bij het proefschrift \quotation{\en Nominal Techniques and Black \break Box Testing for Automata Learning\nl} van Joshua Moerman
\stopalignment

\mainlanguage[en]
\startitemize[n]
\item
Bisimulations are not only useful for comparing white box systems.
They can also be used in black box testing for proving completeness of test suites.
By using bisimuations, we obtain simple and general proofs.

\item
It is well possible to learn a big, industrial piece of software using active automata learning.
A remaining bottleneck is how to find counterexamples.

\item
All the ingredients for a test generation methods such as W-method can be constructed in $\mathcal{O}(n \log n)$ time for state machines of size $n$.
From these ingredients, the test suite can be directly enumerated.

\item
Nominal sets provide good semantics for register automata.
From these semantics we see that the {\tt L}$^{\ast}$ algorithm seamlessly generalises to register automata.

\item
When computing with nominal sets, enumeration can outperform solvers, especially in situation with few variables.

\item
By restricting the expressiveness of an automaton model, we can obtain smaller automata and hence learn them more efficiently.
For example, data structures can be modelled as register automata which only read fresh values.

\item
A finite state machine is defined as a $5\frac{4}{5}$-tuple (study of several papers in FSM-based testing literature).

\item
Adjunctions don't lift themselves.

\item
Although people often think that testing is not a formal method, testing of finite state machines can be done in a sound and complete manner.

\item
Big data is a solved problem.
A much more relevant and much harder problem is that of learning from small data.

\stopitemize
\stopchapter
\stoptext