diff options
| -rw-r--r-- | all.tex | 25 | ||||
| -rw-r--r-- | glossary.tex | 25 | ||||
| -rw-r--r-- | ref.bib | 237 | ||||
| -rw-r--r-- | shell.nix | 7 |
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; }) ]; } |