Related papers: Model-Checking the Higher-Dimensional Modal mu-Cal…
Fixpoints are an important ingredient in semantics, abstract interpretation and program logics. Their addition to a logic can add considerable expressive power. One general issue is how to define proof systems for such logics. Here we…
We investigate the possibility of a semantic account of the execution time (i.e. the number of \beta_v-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value {\lambda}-calculus. For…
Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two…
In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification,…
Rewriting logic and its implementation Maude are a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled…
Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the…
We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value lambda-calculus. For this…
A comprehensive verification of parallel software imposes three crucial requirements on the procedure that implements it. Apart from accepting real code as program input and temporal formulae as specification input, the verification should…
Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system, under the assumption that agents in the system choose strategies that form a game-theoretic equilibrium.…
In this paper, we generalize modal $\mu$-calculus to the non-distributive (lattice-based) modal $\mu$-calculus and formalize some scenarios regarding categorization using it. We also provide a game semantics for the developed logic. The…
Model checking is a technique to automatically assess whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its requirements is essential for the user to understand the…
The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a…
Symbolic model checking by using BDDs has greatly improved the applicability of model checking. Nevertheless, BDD based symbolic model checking can still be very memory and time consuming. One main reason is the complex transition relation…
This paper presents a proof-theoretic analysis of the modal $\mu$-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal $\mu$-calculus, using methods from linear logic and its exponential modalities.…
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and…
Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic…
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite…
We study a variant of the modal $\mu$-calculus based on the constructive modal logic $\mathsf{CK}$. We define game semantics for the constructive $\mu$-calculus and prove its equivalence to the birelational Kripke semantics. We then use the…
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity…
Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a…