ABSTRACT. Heap and data structures represent one of the biggest challenges when applying model checking to the analysis of software programs: in order to verify (unbounded) safety of a program, it is typically necessary to formulate quantified inductive invariants that state properties about an unbounded number of heap locations. Methods like Craig interpolation, which are commonly used to infer invariants in model checking, are often ineffective when heap is involved. To address this challenge, we introduce a set of new proof and program transformation rules for verifying object-oriented programs with the help of space invariants, which (implicitly) give rise to quantified invariants. Leveraging advances in Horn solving, we show how space invariants can be derived fully automatically, and how the framework can be used to effectively verify safety of Java programs.

ABSTRACT. Proof by coupling is a powerful proof technique for proving probabilistic properties like stochastic dominance and rapid mixing of Markov chains, arising in a variety of fields. Couplings have also proved to be a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational properties, such as uniformity and conditional independence. Specifically, we demonstrate that the program logic pRHL---whose proofs correspond to proofs by coupling---can be used in combination with self-composition for proving such facts. We formally verify our main examples using the EasyCrypt proof assistant.

ABSTRACT. In this paper we show that the fully boxed fragment of first-order LTL (which contains only the temporal connective [] (Box) and every atom, every operation but [], and every quantifier is guarded with []) is not recursively enumerable. To obtain incompleteness for this weak fragment we associate to its formulas a corresponding Gödel logic, G_down (an infinitely valued Gödel logic with only one accumulation point of truth values at 0). By embedding the theory of two equivalence relations on finite sets, we show with one proof that the monadic fragments of G_down and G_up (infinitely valued Gödel logic with only one accumulation point of truth values at 1, also the intersection of all finitely valued Gödel logics) with two predicate symbols are not recursively enumerable.

We use arguments from first-order LTL to demonstrate that the complement of the 1-satisfiable formulas of G_down is not recursively enumerable. This is in contrast to the fact that the same fragment for G_up is decidable.

ABSTRACT. We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. We prove a general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions and then adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

ABSTRACT. It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we propose such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL and simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the notion that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of linear logics featuring different axioms for the modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.

ABSTRACT. Linear Temporal Logic (LTL) is a de-facto standard formalism for expressing properties of systems and temporal constraints in Formal Verification, Artificial Intelligence, and other areas. The problem of LTL satisfiability is thus prominently important to check the consistency of these temporal specifications. Although adding past operators to LTL does not increase its expressive power, recently the interest for explicitly handling the past in temporal logics has increased because of the clarity and succinctness that those operators provide. In this work, a recently proposed one-pass tree-shaped tableau system for LTL is extended to support past operators. The modularity of the required changes provides evidence for the claimed ease of extensibility of this tableau system.

ABSTRACT. Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.

We justify here CoqMT's type-checking algorithm by showing strong normalization as well as the Church-Rosser property of beta-reductions augmented with CoqMT's weak and strong T-elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.

ABSTRACT. The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security critical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified kernels currently leave the TLB as an assumption.

In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency and abstract the functional details of the MMU for reasoning about executions in the presence of cached address translation.

ABSTRACT. In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered.

In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular $n$ implies that there does not exist a solution to the problem. We formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability, thereby reducing our dependency on previous work.