Commit 8d34b17a authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

aplas: refs to DRYAD and HIP

parent 442ffbfc
......@@ -7,7 +7,7 @@
\mypar{Implementation.}
The decision procedures presented are implemented as an extension of the
\cspen\ solver~\cite{GuCW16},
\cspen\ solver. %~\cite{GuCW16},
called \cspenp, available at~\cite{CompSpenSite}.
%Let us briefly recall some information about {\cspen}.
{\cspen} is written in C++ and includes several decision procedures
......
......@@ -6,7 +6,8 @@ has a big impact on the verification or static analysis of programs
manipulating the dynamic memory. Performant tools have been developed
based on this formalism, among which we cite
\textsc{Infer}~\cite{DBLP:journals/cacm/DistefanoFLO19} for static analysis
and \textsc{VeriFast}~\cite{verifast} for deductive verification.
and \textsc{VeriFast}~\cite{verifast}, \textsc{DRYAD}~\cite{DBLP:conf/pldi/PekQM14
} or \textsc{Hip}~\cite{DBLP:conf/atva/HeQLC09} for deductive verification.
The \emph{symbolic heap} (SH) fragment
of separation logic has been introduced in~\cite{BerdineCO04}
......@@ -60,12 +61,15 @@ is decidable.
However, the ASL fragment or its above extensions are not expressive enough
to specify the heap list data structure.
Although other fragments of separation logic has been used
in the static analysis of memory allocators~\cite{CalcagnoDOHY06}
or in their deductive verification~\cite{Chlipala11,MartiAY06},
the decidability of verification problem has not been studied
because these tools either employed sound heuristics or
interactive theorem provers.
%A special instance where all chunks have the same size
%has been used in the deductive verification of
% an implementation of the array list collection~\cite{CauderlierS18},
......
@inproceedings{DBLP:conf/atva/HeQLC09,
author = {Guanhua He and
Shengchao Qin and
Chenguang Luo and
Wei{-}Ngan Chin},
editor = {Zhiming Liu and
Anders P. Ravn},
title = {Memory Usage Verification Using Hip/Sleek},
booktitle = {Automated Technology for Verification and Analysis, 7th International
Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5799},
pages = {166--181},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04761-9\_14},
doi = {10.1007/978-3-642-04761-9\_14},
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
biburl = {https://dblp.org/rec/conf/atva/HeQLC09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/PekQM14,
author = {Edgar Pek and
Xiaokang Qiu and
P. Madhusudan},
editor = {Michael F. P. O'Boyle and
Keshav Pingali},
title = {Natural proofs for data structure manipulation in {C} using separation
logic},
booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
{PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
pages = {440--451},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2594291.2594325},
doi = {10.1145/2594291.2594325},
timestamp = {Sun, 25 Oct 2020 22:43:27 +0100},
biburl = {https://dblp.org/rec/conf/pldi/PekQM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/Le21,
author = {Quang Loc Le},
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment