Accelerated bounded model checking with LoAT

Science of Computer Programming, vol. 253, pp. 103497

Abstract

LoAT is a fully automated verification tool that can prove (un)satisfiability of linear Constrained Horn Clauses, as well as non-termination and lower bounds on the worst-case runtime complexity of transition systems. Recently, we introduced Accelerated Bounded Model Checking (ABMC), a novel model checking technique that combines acceleration techniques with Bounded Model Checking (BMC), and implemented it in LoAT . Acceleration techniques compute “shortcuts” that “compress” many execution steps into a single one, and thus ABMC is capable of finding deep counterexamples that are challenging for BMC, as finding them with BMC requires a large bound.

Authors 2

1. Florian Frohn corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Jürgen Giesl Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany