Commit fef23d9b authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

details on experiments

parent ab02ec2e
......@@ -128,17 +128,16 @@ To the best of our knowledge, there have not been solvers that are capable of so
\begin{table}[htbp]
\vspace{-2eX}
\caption{Experimental results, where the time is in seconds}
\caption{Experimental results, time measured in seconds}
\label{tab-exp}
\vspace{-4eX}
\vspace{-2eX}
\begin{center}
%\small
\setlength{\tabcolsep}{1eX}
\renewcommand{\arraystretch}{1.2}
\begin{tabular}{| c | c | c | c | c | c |}
\hline
% & & Benchmark& \multicolumn{3}{c}{Time (in seconds)} \\\
Benchmark suite & $\#$instances & Timeout & Avg. time (s) & Min. time (s) & Max. time (s) \\
Benchmark suite & $\#$instances & Timeout & Avg. time & Min. time & Max. time \\
\hline
\hline
MEM-SAT & 38 & 0 & 0.05 & 0.03 &0.12 \\
......@@ -159,10 +158,9 @@ To the best of our knowledge, there have not been solvers that are capable of so
\vspace{-6eX}
\end{table}
As expected, solving entailment instances is more expensive
than solving satisfiability instances.
As expected, solving entailment instances is more expensive than solving satisfiability instances.
We recall from Section~\ref{sec:ent} that the procedure for entailment queries satisfiability of several formulas.
\cspenp\ efficiently solves the benchmark instances originated from programs,
\cspenp\ efficiently solves the benchmark instances originated from program's verification,
namely MEM-SAT and MEM-ENT, with the average time in 0.05 and 3.05 seconds respectively.
% ESOP 21 Reviewer 3: In the evaluation, since many examples are automatically generated, it would be interesting to see what happens as the size of the example is increased. Of course, one understands the worst-case complexity from the theoretical sections, but whether performance degrades quickly in practice is less obvious given that this is a real implementation of the work which includes some heuristics for improving performance in practice.
......@@ -170,12 +168,10 @@ namely MEM-SAT and MEM-ENT, with the average time in 0.05 and 3.05 seconds respe
Table~\ref{tab-exp} shows that some entailment instances
are challenging for \cspenp. %\todo{speed if size increase}
For instance, the maximum time in MEM-ENT suite is
9.98, and there are 7 timeout instances in RANDOM-ENT suite.
%In order to pinpoint the potential reasons behind the long running time,
%we inspected these two entailment instances manually and find that
By inspected these challenging instances, we found that
(i) they require splitting some $\hls{}$ atoms in the antecedent,
which is potentially time-consuming,
9.98, and there are 7 timeout instances in RANDOM-ENT suite (5 examples in less than 1 min, and 2 example in more than 2 min).
By inspecting these challenging instances, we found that
(i) they require splitting some spatial atoms ($\blk{}$ or $\hls{}$) in the antecedent,
which is potentially time-consuming, and
(ii) they correspond to valid entailment problems
where \cspenp\ has to explore all the total preorders,
which is time-consuming.
......
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