Yernaux, Gonzague Vanhoof, Wim

Anti-unification in logic programming refers to the process of capturing common syntactic structure among given goals, computing a single new goal that is more general called a generalization of the given goals. Finding an arbitrary common generalization for two goals is trivial, but looking for those common generalizations that are either as large...

Chatterjee, Krishnendu Goharshady, Amir Meggendorfer, Tobias Žikelić, Ðorđe

We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p ∈ [0, 1], we aim for certificates proving that the program terminates with probability at least 1 − p. The basic idea of our approach is to find a term...

Amat, Nicolas Zilio, Silvano Dal Hujsa, Thomas

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing...

Chardonnet, Kostia Valiron, Benoît Vilmart, Renaud

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual stand...

Heijltjes, Willem Hughes, Dominic Straßburger, Lutz

We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simplytyped lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representa...

Govind, R. Herbreteau, Frédéric Srivathsan, B. Walukiewicz, Igor

A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is ...

Bourgaux, Camille Bourhis, Pierre Peterfreund, Liat Thomazo, Michaël

Data provenance consists in bookkeeping meta information during query evaluation, in order to enrich query results with their trust level, likelihood, evaluation cost, and more. The framework of semiring provenance abstracts from the specific kind of meta information that annotates the data. While the definition of semiring provenance is uncontrove...

Thibault, Joan

Various classical problems in computer science can be formulated as ConstraintSolving Problems (CSP), consisting in a query on a conjunction of constraints. Typical instancesof such queries are satisfiability (with or without witness), optimization under constraints, modelenumeration, model counting and canonicalization. Constraint systems can be C...

Gouëzel, Sébastien

We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive set theory. The interplay between these domains is transparent thanks to the highly integrated develop...

Alberti, Michele Bobot, François Chihani, Zakaria Girard-Satabin, Julien Lemesle, Augustin

We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art ...