%
% Fill only lines marked with dots  
% 
%
%
\documentclass[10pt,a4paper,twoside]{article}
\usepackage{latexsym,amssymb}
\usepackage{amssymb,amsmath}
\usepackage{graphicx}
\usepackage{color}
\usepackage{fancyhdr}
\pagestyle{fancy}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  PLEASE, ONLY IN ENGLISH                                         %
%  PLEASE, ONLY ONE PAGE                                           %
%  PLEASE, USE LATEX2E                                             %
%                                                                  %
%  PLEASE, DO NOT DEFINE NEW COMMANDS                              %
%  USE NEWTHEOREMS BELOW, PLEASE, IF YOU WRITE THEOREMS AND SUCH   % %                                                                  %
%  PLEASE, CONTROL THE SIZE OF YOUR ABSTRACT BEFORE YOU SEND IT    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newtheorem{thm}{Theorem}
\newtheorem{defi}[thm]{Definition}
\newtheorem{axi}[thm]{Axiom}
\newtheorem{clm}[thm]{Claim}
\newtheorem{col}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{con}[thm]{Conjecture}
\newtheorem{hyp}[thm]{Hypothesis}
\newtheorem{rem}[thm]{Remark}
\newcommand{\proof}{\noindent{\bf Proof:}\hspace{0.2cm}}
\setcounter{thm}{0}
\newcommand{\N}{{\mathbb N}}
\newcommand{\R}{{\mathbb R}}
\newcommand{\W}{W_0^{1,p}(\Omega)}
\newcommand{\eps}{{\varepsilon}}
\newcommand{\ds}{\displaystyle}

\newcommand{\F}{\mathcal F}
\newcommand{\E}{\mathscr E}
\newcommand{\J}{\mathscr{J}}
\newcommand{\Pl}{(\mathscr{P})}
\newcommand{\CC}{\mathbb C}
\newcommand{\into}{\int\limits_{\Omega}}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\textwidth 15.0cm
\textheight 22.0cm
\oddsidemargin 0.4cm
\evensidemargin 0.4cm
\topmargin  0.0cm

\frenchspacing

\headwidth=\textwidth 	
\fancyhead[HCO]{8th Int. Conf. on Mathematics and Informatics,
	September 9-10, 2021, T\^argu Mure\c s, Romania}
\lhead{}\rhead{}
\fancyfoot{}
%


\begin{document}

\begin{center}{\Large\bf
Targeted static fault localization in Erlang programs
}\end{center}
%
\begin{center}{\large\bf\noindent
Zsófia Erdei, Melinda T\'oth, Istv\'an Boz\'o
}\\[2mm]
%%
ELTE, E\"otv\"os Lor\'and University
%%
\\[1mm]\texttt{
%%	
zsanart@inf.elte.hu, toth\_m@inf.elte.hu, bozo\_i@inf.elte.hu
%%
}\end{center}
%

\vspace*{7mm}
%
Static source code analysis techniques may help the programmers in various tasks: code comprehension, testing, debugging, etc. They often need to reproduce executions that result in faulty behaviour. Program analysis techniques with symbolic execution can help to solve this task. In this paper we propose a method to select an appropriate execution path from the static control-flow graph that may lead to a given runtime error in Erlang software. We build our tool on the RefactorErl static analyser framework.

Fault localization is the act of identifying the locations of faults in a program. Even when bugs in software are discovered due to some faulty behavior (e.g. a runtime error occurs), finding the location of the fault is a non-trivial task. Error detection mechanisms are vital for building highly reliable systems. Fault localization is one of the most time consuming, and expensive part of software development and maintenance. Given the size and complexity of large-scale software systems today, manual fault localization becomes more and more futile, so effective automatic methods are needed.

In a concrete execution, a program is evaluated on a specific input and a single control-flow path is explored. Symbolic execution~\cite{symbolic,survey_symbolic} uses unknown symbolic variables in evaluation, allowing to simultaneously explore multiple paths that a program could take under different inputs. We can use symbolic execution to help us in fault localization. We target to find an execution path in the program, the "error path", that may result in a runtime error in a given point of the program. Thus we build a direct symbolic execution engine for a given execution path in the Erlang programs based on the RefactorErl framework~\cite{refactorerl1}. We are using the  SMT solver of Z3~\cite{z3} to solve the constraints that we gather during our analysis. 
 

We can use symbolic execution to help us in fault localization. We target to find an execution path in the program, the "error path", that may result in a runtime error in a given point of the program. Thus we build a direct symbolic execution engine for a given execution path in the Erlang programs based on the RefactorErl framework~\cite{refactorerl1}. We are using the  SMT solver of Z3~\cite{z3} to solve the constraints that we gather during our analysis. 

%%

%
%
\bibliographystyle{unsrt}
%\bibliographystyle{ACM-Reference-Format}
\bibliography{bib.bib}

\end{document}


