diff options
| author | Nguyễn Gia Phong <cnx@loang.net> | 2023-10-28 15:57:52 +0900 |
|---|---|---|
| committer | Nguyễn Gia Phong <cnx@loang.net> | 2023-10-28 20:02:06 +0900 |
| commit | 29ec67340c03fb15dce465381737b96e12ef764b (patch) | |
| tree | 31a07da1af8c4fa05f64e2fb52a3bfcdbdab3c5c /praelimen.tex | |
| download | thesis-29ec67340c03fb15dce465381737b96e12ef764b.tar.gz | |
Draft skeleton
Diffstat (limited to 'praelimen.tex')
| -rw-r--r-- | praelimen.tex | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/praelimen.tex b/praelimen.tex new file mode 100644 index 0000000..e2dfea3 --- /dev/null +++ b/praelimen.tex @@ -0,0 +1,7 @@ +\section{Preliminaries} +Our \gls{difftest} generation is based on the symbolic executor +\textsc{klee}'s architecture, which at a high level is an interpreter loop. +At each iteration, it selects a symbolic process, also known as a \gls{state}, +in whose context an instruction is then executed. + +% TODO: base symb exec algo |