Commit 0a27e6e5 authored by ehilin02's avatar ehilin02
Browse files

minor changes in related works

parent a7c7440b
......@@ -66,7 +66,7 @@ The static analysis of memory allocators using separation logic was the focus of
several works starting with the pioneering work of~\cite{CalcagnoDOHY06}.
For example, \cite{LiuR15} defined an abstract domain for the analysis of array properties and applies it to the Minix 1.1 memory allocator, which uses chunks of fixed size. Also, \cite{FangS16} employed an extension of SL with data words and overlapping separating conjunction to analyze free list memory allocators.
In these analyzers, the decidability of verification problem has not been studied
because these tools employ sound heuristics to decide satisfiability or entailment problems.
because these tools employ sound heuristics to solve satisfiability or entailment problems.
Deductive verification of memory allocators has been considered in
several works~\cite{Chlipala11,MartiAY06,AppelN20}.
......@@ -74,7 +74,7 @@ For example, \cite{Chlipala11} presents a Coq library based on SL that
allows to abstract the low level details of the memory organization
in order to obtain an almost-automatic verification
of an malloc implementation using heap and free lists. However, the
abstraction proposed can not deal with the coalescing of chunks in the heap lists.
abstraction proposed cannot deal with the coalescing of chunks in the heap lists.
Our logic fragment \slah{} is less general, but allows to reason about the coalescing operation.
Separation logic is also used in~\cite{AppelN20} to verify the functional correctness
of an malloc implementation Verified Software Toolchain within the Coq proof assistant.
......@@ -83,7 +83,7 @@ of an malloc implementation Verified Software Toolchain within the Coq proof ass
% an implementation of the array list collection~\cite{CauderlierS18},
%but required an interactive prover \textsc{VeriFast} and user-provided
%lemma.
Our work provides insights on strategies for automatizing these deductive verification based work.
Our work provides insights on strategies for automating these deductive-verification based work.
......
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