From 210ddf92aab09acc796b2a7fe34ba3bd983cbd62 Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong Date: Mon, 11 Dec 2023 13:34:41 +0900 Subject: Finish content --- technique.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'technique.tex') 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. -- cgit 1.4.1