Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C with unboundedly many Context Switches: (Competition Contribution)

We describe a new CSeq module for the verification of multi-threadedC programs with dynamic thread creation. This module implements a variationof the lazy sequentialization algorithm implemented in Lazy-CSeq. The mainnovelty is that we do not bound here the number of round-robin schedules in anexecution and the loops that do not contain a thread creation statement are notunwound (and thus unboundedly many iterations can be considered). As in Lazy-CSeq the number of thread creations per run is bounded as well as the depth ofrecursive calls. For the experiments we use CPAChecker as backen