Delay-Bounded Scheduling Without Delay!

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.

Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)

Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.

Two Treatments of Definite Descriptions in Intuitionist Negative Free Logic

Sentences containing definite descriptions, expressions of the form `The F', can be formalised using a binary quantier that forms a formula out of two predicates, where ℩x[F;G] is read as `The F is G'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system INF℩ of intuitionist negative free logic extended by such a quantier, which was presented in [4], INF℩ is first compared to a system of Tennant's and an axiomatic treatment of a term forming ℩ operator within intuitionist negative free logic. Both systems are shown to be equivalent to the subsystem of INF℩ in which the G of ℩x[F;G] is restricted to identity. INF℩ is then compared to an intuitionist version of a system of Lambert's which in addition to the term forming operator has an operator for predicate abstraction for indicating scope distinctions. The two systems will be shown to be equivalent through a translation between their respective languages. Advantages of the present approach over the alternatives are indicated in the discussion.

Ǝ-closure and Alternatives

This remark considers the interaction of Alternative Semantics (AS) with various binding operations—centrally, Predicate Abstraction (PA) and Ǝ-closure; less centrally, intensionalization. Contra Griffiths’s (2019) theory of ellipsis, I argue that it is technically problematic to appeal to the inherent incompatibility of PA and AS, while assuming the compatibility of Ǝ-closure and AS. I show that the formal pressures that characterize the interaction of PA and alternatives apply equally to Ǝ-closure and alternatives, and that it is accordingly impossible to define a true Ǝ-closure operation within what might be termed “standard” AS. A well-behaved AS reflex of Ǝ-closure can only be defined in compositional settings where a well-behaved AS reflex of PA is definable too. I consider various technical and empirical consequences of these points for Griffiths’s theory of ellipsis, and for linguistic theory more generally.