Prettify

4 files changed, 227 insertions, 67 deletions

diff --git a/all.tex b/all.tex
index ba7aeed..bc39715 100644
--- a/all.tex
+++ b/all.tex
@@ -1,24 +1,29 @@
 \documentclass[11pt, a4paper, onecolumn, oneside]{report}
 \usepackage[vietnamese,english]{babel}
+\usepackage[hidelinks]{hyperref}
 \usepackage{mathptmx}
 \RequirePackage[top=3cm, bottom=1in, left=1in, right=1in]{geometry}
 \linespread{1.3}
 
 \usepackage{algorithm}
-\usepackage{algpseudocode}
+\usepackage[noend]{algpseudocode}
+\usepackage{alltt}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{booktabs}
 \usepackage{caption}
 \usepackage{cases}
 \usepackage{cite}
+\usepackage{enumitem}
 \usepackage{fancyhdr}
-\usepackage{glossaries}
 \usepackage{graphicx}
-\usepackage[hidelinks]{hyperref}
+\usepackage{glossaries}
 \usepackage{pdfpages}
+\usepackage[skip=-1ex]{subcaption}
 \usepackage{tikz}
 \usepackage{tocloft}
+\usepackage{varwidth}
+\usepackage{xcolor}
 
 \usetikzlibrary{arrows}
 \usetikzlibrary{decorations.pathmorphing}
@@ -34,6 +39,9 @@
 \renewcommand{\thesection}{\Roman{section}}
 \renewcommand{\thesubsection}{\arabic{section}.\arabic{subsection}}
 \renewcommand{\thefigure}{\arabic{figure}}
+\renewcommand{\thefootnote}{\fnsymbol{footnote}}
+\renewcommand{\algorithmicrequire}{\textbf{Input:}}
+\renewcommand{\algorithmicensure}{\textbf{Output:}}
 \newcommand{\qed}{\hfill\blacksquare}
 
 \newcounter{lemma}
@@ -45,13 +53,17 @@
 \newtheorem{theorem}{\bf Theorem}
 \newtheorem{proof}{\bf Proof}
 \DeclareMathOperator*{\argmax}{arg\,max}
+\DeclareCaptionLabelFormat{none}{\!}
 
 \newcommand{\name}{Symbolic Execution Groundwork\\
-                   for Differential Testing of Patch Pools}
+                   for Distinguishing Automatically Generated Patches}
 \newcommand{\cnx}{\foreignlanguage{vietnamese}{Nguyễn Gia Phong}}
 \newcommand{\cse}{Department of Computer Science and Engineering}
 \newcommand{\unist}{Ulsan National Institute of Science and Technology}
+\newcommand{\klee}{\textsc{klee}}
+\newcommand{\psychic}{\textsc{Psychic}}
 \newcommand{\blankpage}{\hbox{}\thispagestyle{empty}\clearpage}
+\newcommand{\doi}[1]{\href{https://oadoi.org/#1}{doi:#1}}
 
 \fancyhf{}
 \renewcommand{\headrulewidth}{0pt}
@@ -83,10 +95,11 @@
 \thispagestyle{empty}
 \clearpage
 \renewcommand{\listfigurename}{\hfill\Large List of Figures\hfill}
-\listoffigures{}
+{\captionsetup{subrefformat=none}\listoffigures{}}
 \thispagestyle{empty}
 \clearpage
-\renewcommand{\glossaryname}{\hfill\Large Technical Terms\hfill\hfill}
+\renewcommand{\glossaryname}{\hfill\Large Technical Terms
+                             and Abbreviations\hfill\hfill}
 \printnoidxglossaries
 \thispagestyle{empty}
 \clearpage
diff --git a/glossary.tex b/glossary.tex
index 8f43f5f..1134321 100644
--- a/glossary.tex
+++ b/glossary.tex
@@ -1,18 +1,21 @@
 \makenoidxglossaries
 \newglossaryentry{difftest}{name={differential test},
-  description={Is an input and a collection of outputs of two or more programs
+  description={is an input and a collection of outputs of two or more programs
     of the same purpose, such that each output is pairwise different}}
 \newglossaryentry{state}{name=state,
-  description={Or \emph{symbolic process}, includes a register file,
-    a stack frame, an address space for heap and global variables,
-    a program counter and path conditions.  Stack, heap and global variables
-    here are all symbolic expressions.  For our algorithm, the state
-    additionally contain the identifier of its program revision}}
-\newglossaryentry{pstates}{name={parallel states},
-  description={Two states are parallel if and only if their program counter
-    points to the same instruction\footnote{They do not necessarily
-    share the same program counter however.} and the conjunction
-    of their path conditions is satisfiable}}
+  description={or \emph{symbolic process}, includes a program counter,
+    an execution environment (a register file, a stack frame,
+    and an address space for heap and global variables), and path constraints.
+    Variables in an execution environment are all symbolic expressions}}
+\newglossaryentry{symout}{name={symbolic output},
+  description={is an output or intermediate value of a program
+    under symbolic execution that reflects behaviors of the program
+    relevant to the analysis}}
+\newacronym{apr}{APR}{automated program repair}
+\newacronym{ir}{IR}{intermediate representation}
+\newacronym{sat}{SAT}{satisfiability}
+\newacronym{smt}{SMT}{satisfiability modulo theories}
+\newacronym{ffi}{FFI}{foreign function interface}
 \newglossaryentry{searcher}{name=searcher,
   description={Is what keeps track of states to be executed,
     along with the information for scheduling them to optimize resources
diff --git a/ref.bib b/ref.bib
index 4d4598d..5703043 100644
--- a/ref.bib
+++ b/ref.bib
@@ -1,24 +1,56 @@
+@article{entropy,
+  author = {Claude Elwood Shannon},
+  journal = {The Bell System Technical Journal},
+  title = {A mathematical theory of communication},
+  year = 1948,
+  volume = {27},
+  number = {3},
+  pages = {379-423},
+  note = {\doi{10.1002/j.1538-7305.1948.tb01338.x}}}
+
+@inproceedings{k-sat,
+  author = {Russell Impagliazzo and Ramamohan Paturi},
+  booktitle = {Proc. IEEE Conf. Comput. Complex. (CCC)},
+  title = {Complexity of {k-SAT}},
+  year = 1999,
+  pages = {237--240},
+  note = {\doi{10.1109/CCC.1999.766282}}}
+
 @inproceedings{klee,
-  author = {Cristian {Cadar} and Daniel {Dunbar} and Dawson {Engler}},
-  title = {{KLEE}: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs},
+  author = {Cristian Cadar and Daniel Dunbar and Dawson Engler},
+  title = {{KLEE}: Unassisted and Automatic Generation of High-Coverage Tests
+           for Complex Systems Programs},
   booktitle = {USENIX Symp. Oper. Syst. Des. and Implement. (OSDI)},
   year = 2008,
-  url = {https://www.usenix.org/conference/osdi-08/klee-unassisted-and-automatic-generation-high-coverage-tests-complex-systems},
   month = dec,
-  doi = {10.5555/1855741.1855756}}
+  url = {https://www.usenix.org/conference/osdi-08/klee-unassisted-and-automatic-generation-high-coverage-tests-complex-systems}}
+
+@manual{klee-docs,
+  title = {\klee{} documentation},
+  organization = {{the \textsc{klee} team}},
+  url = {https://klee.github.io/docs}}
 
 @inproceedings{join-split,
-  author = {Trevor {Hansen} and Peter {Schachte} and Harald {S{\o}ndergaard}},
+  author = {Trevor Hansen and Peter Schachte and Harald S{\o}ndergaard},
   title = {State Joining and Splitting for the Symbolic Execution of Binaries},
   booktitle = {Runtime Verification},
   year = 2009,
   publisher = {Springer Berlin Heidelberg},
-  address = {Berlin, Heidelberg},
   pages = {76--92},
   doi = {10.1007/978-3-642-04694-0_6}}
 
+@inproceedings{smt,
+  author = {Leonardo de Moura and Nikolaj Bj{\o}rner},
+  title = {Satisfiability Modulo Theories: An Appetizer},
+  booktitle = {Formal Methods: Foundations and Applications},
+  year = 2009,
+  publisher = {Springer Berlin Heidelberg},
+  pages = {23--36},
+  isbn = {978-3-642-10452-7},
+  note = {\doi{10.1007/978-3-642-10452-7\_3}}}
+
 @inproceedings{rsc,
-  author = {{Qi} Dawei and {Nguyen} D.T. Hoang and Abhik {Roychoudhury}},
+  author = {Qi, Dawei and Nguyen, D.T. Hoang and Abhik Roychoudhury},
   title = {Path Exploration Based on Symbolic Output},
   year = 2011,
   isbn = {9781450304436},
@@ -32,7 +64,8 @@
   series = {ESEC/FSE '11}}
 
 @article{merge,
-  author = {Volodymyr {Kuznetsov} and Johannes {Kinder} and Stefan {Bucur} and George {Candea}},
+  author = {Volodymyr Kuznetsov and Johannes Kinder
+            and Stefan Bucur and George Candea},
   title = {Efficient State Merging in Symbolic Execution},
   year = 2012,
   publisher = {Association for Computing Machinery},
@@ -46,38 +79,76 @@
   month = jun,
   pages = {193--204},
   numpages = 12,
-  keywords = {verification, symbolic execution, bounded software model checking, state merging, testing}}
+  keywords = {verification, symbolic execution, bounded software model checking,
+              state merging, testing}}
 
 @inproceedings{cgs,
-  author = {{Seo} Hyunmin and {Kim} Sunghun},
-  title = {How We Get There: A Context-Guided Search Strategy in Concolic Testing},
+  author = {Seo, Hyunmin and Kim, Sunghun},
+  title = {How We Get There:
+           A Context-Guided Search Strategy in Concolic Testing},
   year = 2014,
   isbn = {9781450330565},
   publisher = {Association for Computing Machinery},
   url = {https://doi.org/10.1145/2635868.2635872},
   doi = {10.1145/2635868.2635872},
-  booktitle = {Proc. ACM SIGSOFT Int. Symp. Found. Softw. Eng.},
+  booktitle = {Proc. ACM SIGSOFT Int. Symp. Found. Softw. Eng. (FSE)},
   pages = {413-424},
   numpages = 12,
-  keywords = {symbolic execution, search strategies, Concolic testing},
-  series = {FSE 2014}}
+  keywords = {symbolic execution, search strategies, Concolic testing}}
+
+@article{introclass,
+  author = {Claire {Le Goues} and Neal Holtschulte and Edward K. Smith
+            and Yuriy Brun and Premkumar Devanbu and Stephanie Forrest
+            and Westley Weimer},
+  title = {The {ManyBugs} and {IntroClass} Benchmarks
+           for Automated Repair of {C} Programs},
+  journal = {IEEE Trans. Softw. Eng. (TSE)},
+  year = 2015,
+  issn = {0098-5589},
+  volume = {41},
+  number = {12},
+  month = dec,
+  pages = {1236--1256},
+  note = {\doi{10.1109/TSE.2015.2454513}}}
 
 @inproceedings{overfit,
-  author = {Edward K. {Smith} and Earl T. {Barr} and Claire {Le Goues} and Yuriy {Brun}},
-  title = {Is the Cure Worse than the Disease? Overfitting in Automated Program Repair},
+  author = {Edward K. Smith and Earl T. Barr
+            and Claire {Le Goues} and Yuriy Brun},
+  title = {Is the Cure Worse than the Disease?
+           Overfitting in Automated Program Repair},
   year = 2015,
   isbn = {9781450336758},
   publisher = {Association for Computing Machinery},
   url = {https://doi.org/10.1145/2786805.2786825},
   doi = {10.1145/2786805.2786825},
-  booktitle = {Proc. Joint Meet. Found. Softw. Eng.},
+  booktitle = {Proc. Joint Meet. Found. Softw. Eng. (FSE)},
   pages = {532--543},
   numpages = 12,
-  keywords = {GenProg, TrpAutoRepair, independent evaluation, IntroClass, empirical evaluation, automated program repair},
-  series = {ESEC/FSE 2015}}
+  keywords = {GenProg, TrpAutoRepair, independent evaluation, IntroClass,
+              empirical evaluation, automated program repair}}
+
+@inproceedings{parallel,
+  author = {Emil Rakadjiev and Shimosawa, Taku
+            and Mine, Hiroshi and Oshima, Satoshi},
+  booktitle = {IEEE Trustcom/BigDataSE/ISPA},
+  title = {Parallel SMT Solving and Concurrent Symbolic Execution},
+  year = 2015,
+  volume = 3,
+  pages = {17--26},
+  doi = {10.1109/Trustcom.2015.608}}
+
+@inproceedings{angelix,
+  author={Sergey Mechtaev and Yi, Jooyong and Abhik Roychoudhury},
+  booktitle = {Proc. ACM/IEEE Int. Conf. Softw. Eng. (ICSE)},
+  title = {Angelix: Scalable Multiline Program Patch Synthesis
+           via Symbolic Analysis},
+  year = 2016,
+  pages = {691--701},
+  note = {\doi{10.1145/2884781.2884807}}}
 
 @article{repairnator,
-  author = {Martin {Monperrus} and Simon {Urli} and Thomas {Durieux} and Matias {Martinez} and Benoit {Baudry} and Lionel {Seinturier}},
+  author = {Martin Monperrus and Simon Urli and Thomas Durieux
+            and Matias Martinez and Benoit Baudry and Lionel Seinturier},
   title = {Repairnator Patches Programs Automatically},
   year = 2019,
   publisher = {Association for Computing Machinery},
@@ -89,79 +160,94 @@
   articleno = 2,
   numpages = 12}
 
+@inproceedings{dbgbench,
+  author = {Marcel B\"{o}hme and Ezekiel Olamide Soremekun
+            and Sudipta Chattopadhyay and Emamurho Ugherughe
+            and Andreas Zeller},
+  title = {Where is the Bug and How is it Fixed?
+           {An} Experiment with Practitioners},
+  booktitle = {Proc. Joint Meet. Eur. Softw. Eng. Conf.
+               and ACM Symp. Found. Softw. Eng. (ESEC/FSE)},
+  year = 2017,
+  note = {\doi{10.1145/3106237.3106255}}}
+
 @article{shadow,
-  author = {Tomasz {Kuchta} and Hristina {Palikareva} and Cristian {Cadar}},
+  author = {Tomasz Kuchta and Hristina Palikareva and Cristian Cadar},
   title = {Shadow Symbolic Execution for Testing Software Patches},
   year = 2018,
   publisher = {Association for Computing Machinery},
   volume = 27,
   number = 3,
   issn = {1049-331X},
-  url = {https://doi.org/10.1145/3208952},
-  doi = {10.1145/3208952},
-  journal = {ACM Trans. Softw. Eng. Methodol.},
+  note = {\doi{10.1145/3208952}},
+  journal = {ACM Trans. Softw. Eng. Methodol. (TOSEM)},
   month = sep,
   articleno = 10,
   numpages = 32,
   keywords = {regression bugs, cross-version checks, Symbolic patch testing}}
 
 @inproceedings{homi,
-  author = {{Cha} Sooyoung and {Oh} Hakjoo},
-  title = {Making Symbolic Execution Promising by Learning Aggressive State-Pruning Strategy},
+  author = {Cha, Sooyoung and Oh, Hakjoo},
+  title = {Making Symbolic Execution Promising
+           by Learning Aggressive State-Pruning Strategy},
   year = 2020,
   isbn = {9781450370431},
   publisher = {Association for Computing Machinery},
   url = {https://doi.org/10.1145/3368089.3409755},
   doi = {10.1145/3368089.3409755},
-  booktitle = {Proc. ACM Joint Meet. Eur. Softw. Eng. Conf. and Symp. Found. Softw. Eng.},
+  booktitle = {Proc. Joint Meet. Eur. Softw. Eng. Conf.
+               and ACM Symp. Found. Softw. Eng. (ESEC/FSE)},
   pages = {147--158},
   numpages = 12,
-  keywords = {Online Learning, Dynamic Symbolic Execution},
-  series = {ESEC/FSE 2020}}
+  keywords = {Online Learning, Dynamic Symbolic Execution}}
 
 @inproceedings{hydiff,
-  author = {Yannic {Noller} and Corina S. {P\u{a}s\u{a}reanu} and Marcel {B\"{o}hme} and {Sun} Youcheng and {Nguyen} Hoang Lam and Lars {Grunske}},
+  author = {Yannic Noller and Corina S. P\u{a}s\u{a}reanu and Marcel B\"{o}hme
+            and Sun, Youcheng and Nguyen, Hoang Lam and Lars Grunske},
   title = {HyDiff: Hybrid Differential Software Analysis},
   year = 2020,
   isbn = {9781450371216},
   publisher = {Association for Computing Machinery},
   url = {https://doi.org/10.1145/3377811.3380363},
   doi = {10.1145/3377811.3380363},
-  booktitle = {Proc. ACM/IEEE Int. Conf. Softw. Eng.},
+  booktitle = {Proc. ACM/IEEE Int. Conf. Softw. Eng. (ICSE)},
   pages = {1273--1285},
   numpages = 13,
-  keywords = {fuzzing, symbolic execution, differential program analysis},
-  series = {ICSE '20}}
+  keywords = {fuzzing, symbolic execution, differential program analysis}}
 
 @inproceedings{ddset,
-  author = {Rahul {Gopinath} and Alexander {Kampmann} and Nikolas {Havrikov} and Ezekiel O. {Soremekun} and Andreas {Zeller}},
+  author = {Rahul Gopinath and Alexander Kampmann and Nikolas Havrikov
+            and Ezekiel O. Soremekun and Andreas Zeller},
   title = {Abstracting Failure-Inducing Inputs},
   year = 2020,
   isbn = {9781450380089},
   publisher = {Association for Computing Machinery},
   url = {https://doi.org/10.1145/3395363.3397349},
   doi = {10.1145/3395363.3397349},
-  booktitle = {Proc. ACM SIGSOFT Int. Symp. Softw. Test. and Analysis},
+  booktitle = {Proc. ACM SIGSOFT Int. Symp. Softw. Test. and Analysis (ISSTA)},
   pages = {237--248},
   numpages = 12,
-  keywords = {failure-inducing inputs, debugging, error diagnosis, grammars},
-  series = {ISSTA 2020}}
+  keywords = {failure-inducing inputs, debugging, error diagnosis, grammars}}
 
 @inproceedings{test-based,
-  author = {{Liu} Kui and {Wang} Shangwen and Anil {Koyuncu} and {Kim} Kisub and Tegawend\'{e} F. {Bissyand\'{e}} and {Kim} Dongsun and {Wu} Peng and Jacques {Klein} and {Mao} Xiaoguang and Yves {Le Traon}},
-  title = {On the Efficiency of Test Suite Based Program Repair: A Systematic Assessment of 16 Automated Repair Systems for Java Programs},
+  author = {Liu, Kui and Wang, Shangwen and Anil Koyuncu and Kim, Kisub
+            and Tegawend\'{e} F. Bissyand\'{e} and Kim, Dongsun and Wu, Peng
+            and Jacques Klein and Mao, Xiaoguang and Le Traon, Yves},
+  title = {On the Efficiency of Test Suite Based Program Repair:
+           A Systematic Assessment of 16 Automated Repair Systems for Java Programs},
   year = 2020,
   isbn = {9781450371216},
   publisher = {Association for Computing Machinery},
   doi = {10.1145/3377811.3380338},
-  booktitle = {Proc. ACM/IEEE Int. Conf. Softw. Eng.},
+  booktitle = {Proc. ACM/IEEE Int. Conf. Softw. Eng. (ICSE)},
   pages = {615--627},
   numpages = 13,
-  keywords = {patch generation, program repair, empirical assessment, efficiency},
-  series = {ICSE '20}}
+  keywords = {patch generation, program repair,
+              empirical assessment, efficiency}}
 
 @article{apr,
-  author = {Claire {Le Goues} and M. {Pradel} and Abhik {Roychoudhury} and S. {Chandra}},
+  author = {Claire {Le Goues} and M. Pradel
+            and Abhik Roychoudhury and S. Chandra},
   journal = {IEEE Software},
   title = {Automatic Program Repair},
   year = 2021,
@@ -171,15 +257,72 @@
   pages = {22--27},
   doi = {10.1109/MS.2021.3072577},
   publisher = {IEEE Computer Society},
-  address = {Los Alamitos, CA, USA},
   month = jul}
 
+@inproceedings{cpr,
+  author = {Ridwan Salihin Shariffdeen and Yannic Noller
+            and Lars Grunske and Abhik Roychoudhury},
+  title = {Concolic Program Repair},
+  year = 2021,
+  note = {\doi{10.1145/3453483.3454051}},
+  booktitle = {Proc. ACM SIGPLAN Int. Conf.
+               Program. Lang. Des. and Implement. (PLDI)},
+  pages = {390--405},
+  numpages = 16,
+  keywords = {program repair, program synthesis,
+              symbolic execution, patch overfitting}}
+
 @article{paradyse,
-  author = {{Cha} Sooyoung and {Hong} Seongjoon and {Bak} Jiseong and {Kim} Jingyoung and {Lee} Junhee and {Oh} Hakjoo},
-  journal = {IEEE Trans. Softw. Eng.},
-  title = {Enhancing Dynamic Symbolic Execution by Automatically Learning Search Heuristics}, 
+  author = {Cha, Sooyoung and Hong, Seongjoon and Bak, Jiseong
+            and Kim, Jingyoung and Lee, Junhee and Oh, Hakjoo},
+  journal = {IEEE Trans. Softw. Eng. (TSE)},
+  title = {Enhancing Dynamic Symbolic Execution
+           by Automatically Learning Search Heuristics},
   year = 2022,
   volume = 48,
   number = 9,
   pages = {3640--3663},
   doi = {10.1109/TSE.2021.3101870}}
+
+@article{trident,
+  author = {Nikhil Parasaram and Earl T. Barr and Sergey Mechtaev},
+  journal = {IEEE Trans. Softw. Eng. (TSE)},
+  title = {Trident: Controlling Side Effects in Automated Program Repair},
+  year = 2022,
+  pages = {4717-4732},
+  note = {\doi{10.1109/TSE.2021.3124323}}}
+
+@inbook{bc,
+  title = {{LLVM} 13.0.1 documentation},
+  month = feb,
+  year = 2022,
+  author = {{LLVM Project}},
+  chapter = {LLVM Bitcode File Format},
+  url = {https://releases.llvm.org/13.0.1/docs/BitCodeFormat.html}}
+
+@inproceedings{semclone,
+  author = {Kazusa Takemoto and Shingo Takada},
+  title = {Applying Symbolic Execution to Semantic Code Clone Detection},
+  booktitle = {Int. Conf. Softw. Eng. and Knowl. Eng. (SEKE)},
+  pages = {118--122},
+  publisher = {{KSI} Research Inc.},
+  year = 2023,
+  note = {\doi{https://doi.org/10.18293/SEKE2023-070}}}
+
+@inbook{unidiff,
+  author = {David MacKenzie and Paul Eggert and Richard Stallman},
+  title = {Comparing and Merging Files
+           for Diffutils 3.10 and \texttt{patch} 2.5.4},
+  publisher = {GNU Project},
+  chapter = {\texttt{diff} Output Formats},
+  pages = {13},
+  month = jan,
+  year = 2023,
+  url = {https://www.gnu.org/software/diffutils/manual/html_node/Detailed-Unified.html}}
+
+@online{msv,
+  author = {Kim, Youngjae},
+  title = {{MSV}},
+  publisher = {Suresoft},
+  url = {https://github.com/Suresoft-GLaDOS/MSV}}
+  url =
diff --git a/shell.nix b/shell.nix
index 7edb879..935766e 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,8 +1,9 @@
 with import <nixpkgs> { };
 mkShell {
   packages = [ (texlive.combine {
-    inherit (texlive) scheme-basic algorithms algorithmicx amsmath
-      babel-vietnamese booktabs caption cases cite fancyhdr float glossaries
-      hyperref pdflscape pdfpages pgf psnfss rsfs times tocloft vntex;
+    inherit (texlive) latexmk scheme-basic
+      algorithms algorithmicx amsmath babel-vietnamese booktabs biblatex
+      caption cases cite enumitem fancyhdr float glossaries hyperref ieeetran
+      pdflscape pdfpages pgf psnfss rsfs times tocloft varwidth vntex xcolor;
   }) ];
 }