Evaluation

MoAT was compared with state-of-the-art tools for verifying LTL properties of infinite state systems. In total, MoAT solved the most benchmarks and was the fastest tool.

Setup

We considered the same benchmarks and similar LTL properties as the evaluation of LTL-VerP. This benchmark set consists of 318 C programs from the Software Verification Competition (SV-COMP) and the Termination Competition (TermComp). To run MoAT on these programs, we translated them into ITSs.

All tools were run inside an Ubuntu Docker container on a machine with an AMD Ryzen 7 3700X octa-core CPU and 8 GB of RAM, with a timeout of 60 s per example as in TermComp. In MoAT’s backend, KoAT was used for the “Yes” answers and LoAT was used for answering “No”.

For each tool that supports several configurations, we selected the configuration recommended by the authors. For nuXmv we used the IC3 engines. Note that the published LTL-VerP results were obtained by evaluating a large number of parameter configurations and selecting the best-performing one per benchmark instance, whereas our experiments apply the single configuration identified by its authors as the overall best setting (linear templates for ranking functions). Its performance here is therefore not directly comparable to the numbers reported in that paper.

LTL properties

Here, x refers to the variable which is first when sorting the variable names alphabetically, and l_term is the terminal location.

Reach-Avoid

(F at(l_term)) ∧ (G (x ≥ 0))

Holds if the terminal location is reached and a negative value of x is avoided.

Overflow

F (x < −64 ∨ x > 63)

Holds if x overflows.

Recurrence

G F (x ≥ 0)

Holds if a non-negative value of x is reached infinitely often.

Progress

G (x < −5 → F (x > 0))

Holds if a value of x less than −5 eventually becomes positive.

Results

Evaluation on LTL formulas: number of benchmarks solved per tool and property class
Prop.	MoAT			MuVal			nuXmv			Ultimate			LTL-VerP
	Yes	No	Total	Yes	No	Total	Yes	No	Total	Yes	No	Total	Yes	No	Total
RA	65	239	304	44	241	285	5	221	226	54	164	218	9	191	200
OV	16	295	311	15	298	313	7	297	304	16	270	286	11	35	46
RC	107	198	305	108	199	307	101	193	294	98	153	251	89	41	130
PR	103	199	302	106	201	307	104	193	297	99	153	252	82	54	136
Total	1222			1212			1121			1007			512
Avg. T	1.11 s			5.02 s			7.26 s			8.90 s			33.81 s
Avg.+ T	0.78 s			2.52 s			0.80 s			3.07 s			4.76 s

“Avg. T” is the average runtime of all runs; “Avg.+ T” is the average runtime of the successful runs, both in seconds.

While MuVal was slightly better than MoAT in some categories, in total MoAT solved the most benchmarks and achieved near-complete coverage (> 96 %) across all categories. MoAT was also the fastest tool, with an average runtime of 1.11 s per example.