Related papers: Nested Hoare Triples and Frame Rules for Higher-or…

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their…

We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories…

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the…

Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalability, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by…

We describe a program logic for weak memory (also known as relaxed memory). The logic is based on Hoare logic within a thread, and rely/guarantee between threads. It is presented via examples, giving proofs of many weak-memory litmus tests.…

We derive multiple program logics, including correctness, incorrectness, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. We introduce an internal language for…

A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal…

Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated…

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed…

We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms,…

We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences of events that arise during the execution. The idea is similar to session types or process-like behavioral…

This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs create and delete components and/or interactions (connectors) while the system components change state…

We introduce the first cut-free nested sequent systems for first-order modal logics that admit increasing, decreasing, constant, and empty domains along with so-called general path conditions and seriality. We obtain such systems by means…

A general framework is proposed for integration of rules and external first order theories. It is based on the well-founded semantics of normal logic programs and inspired by ideas of Constraint Logic Programming (CLP) and constructive…

We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction…

Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that…

We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with…

Inspired by the trend on unifying theories of programming, this paper shows how the algebraic treatment of standard data dependency theory equips relational data with functional types and an associated type system which is useful for type…

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives…

Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists…