diff options
Diffstat (limited to 'technique.tex')
-rw-r--r-- | technique.tex | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/technique.tex b/technique.tex index 470449f..af1fa92 100644 --- a/technique.tex +++ b/technique.tex @@ -333,6 +333,9 @@ If the path constraints of both states are \gls{sat} with at least one difference in outputs, a \gls{difftest} can be generated from the \gls{smt} model. +Halt states are reached naturally at the program's termination or an error. +The latter category also includes sanitizer traps for \gls{ub}. + \begin{algorithm} \caption{\Gls{difftest} generation}\label{diffgen} \begin{algorithmic}[1] @@ -379,8 +382,6 @@ from the \gls{smt} model. \subsection{Decision tree construction} From each \gls{difftest}, a set of clusters of revisions with the same output is constructed. We then superimpose these clustering sets to create -hierarchical clusterings or a decision tree. A minimal tree, i.e~a tree -with the shortest height, is found through exhaustively search though -all subsets of set of clustering sets. - -TODO: analyse complexity +hierarchical clusterings or a decision tree. A minimal tree, i.e.~a tree +with the shortest height, is found by searching through the subsets +of set of clustering sets. |