ABSTRACT. Probabilistic programs encode randomized algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are "more undecidable" than for ordinary programs. Although this all sounds like a no-go for automated analysis, I will present some non-trivial analyses of probabilistic programs using push-button technology. Our techniques are all based on weakest precondition reasoning. We will address automated techniques for termination detection, run-time analysis, k-induction, and the synthesis of probabilistic loop invariants.

ABSTRACT. Internships in Mauritius

ABSTRACT. Epistemic processes describe the dynamic behaviour of multi-agent systems driven by the knowledge of agents, which perform epistemic actions that may lead to knowledge updates. Executing epistemic processes directly on epistemic states, given in the traditional way by pointed Kripke structures, quickly becomes computationally expensive due to the semantic update constructions. Based on an abstraction to formulae of interest, we introduce a symbolic epistemic state representation and a notion of representable epistemic action with efficient symbolic updates. In contrast to existing work on belief or knowledge bases, our approach can handle epistemic actions modelled by arbitrary action models. We introduce an epistemic process calculus and a propositional dynamic logic for specifying process properties that can be interpreted both on the concrete semantic and the symbolic level. We show that our abstraction technique preserves and reflects dynamic epistemic process properties whenever processes are started in a symbolic state that is an abstraction of a semantic epistemic state.

ABSTRACT. We introduce a simple game of resource-conscious reasoning. In this two-player game, players Proponent and Opponent simultaneously place tokens of positive and negative polarity onto a game board. Proponent wins if she manages to match every negative token with a corresponding positive token.

We study the game using methods from computational complexity and proof theory. Specifically, we show complexity results for various fragments of the game, including PSPACE-completeness of a finite restriction of the game and undecidability of the full game featuring infinite plays. Determinacy, that is the existence of a winning strategy for one of the players, can be shown for the full game. Moreover, we show that the finitary version of the game is axiomatisable and can be faithfully embedded into exponential-free linear logic. The full game satisfies the exponential rules of linear logic, but is not fully captured by it.

ABSTRACT. Choices in the semantics and the signature of a theory are integral in determining how the theory is used and how challenging it is to reason over it. Our interest in this paper lies in the SMT theory of sequences. Various versions of it exist in the literature and in state-of-the-art SMT solvers, but it has not yet been standardized in the SMT-LIB. We reflect on its existing variants, and we define a set of theory design criteria to help determine what makes one variant of a theory better than another. The criteria we define can be used to appraise theory proposals for other theories as well. Based on these criteria, we propose a series of changes to the SMT theory of sequences as a contribution to the discussion regarding its standardization.

ABSTRACT. We introduce a software tool for reasoning about belief change in situations where information is received from reports and observations. Our focus is on the interaction between trust and belief. The software is based on a formal model where the level of trust in a reporting agent increases when they provide accurate reports and it decreases when they provide innaccurate reports. If trust in an agent drops below a given threshold, then their reports no longer impact our beliefs at all. The notion of accuracy is determined by comparing reports to observations, as well as to reports from more trustworthy agents. The emphasis of this paper is not on the formalism; the emphasis is on the development of the prototype system for automatically calculating the result of iterated revision problems involving trust. We present an implemented system that allows users to flexibly specify and solve complex revision problems involving reports from partially trusted sources.

ABSTRACT. We present the CheckMate tool for the automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate’s input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

ABSTRACT. Group polarization, the phenomenon where individuals' opinions become more extreme after interacting, has gaining attention, specially with the rise of social media influencing social, political, and democratic processes. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this paper we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic.Our contribution is to endow PNL with more effective formal reasoning techniques, instead of reasoning about group polarization using Hilbert axiomatic systems. First, we introduce a semantic game for (hybrid) extensions of PNL, which supports a dynamic form of reasoning about concrete network models. We show how this semantic game leads to a provability game, by systemically exploring the truth in all models. This leads to the first Gentzen-style cut-free sequent systems for some variants of PNL. Interestingly enough, using polarization of formulas, the proposed sequent systems can be modularly adapted to consider different frame properties of the underlying model.

ABSTRACT. We present our tool FuncTion-V for the automatic identification of the minimal sets of program variables that an attacker can control to ensure an undesirable program property. FuncTion-V supports program properties expressed in Computation Tree Logic (CTL), and builds upon an abstract interpretation-based static analysis for CTL properties that we extend with an abstraction refinement process. We showcase our tool on benchmarks collected from the literature and SV-COMP 2023.

ABSTRACT. In this paper, we present a general strategy that enables the translation of tableau proofs using different Skolemization rules into machine-checkable proofs. It is part of a framework that enables (i) instantiation of the strategy into algorithms for different set of tableau rules (e.g., different logics) and (ii) easy soundness proof which relies on the local extensibility of user-defined rules. Furthermore, we propose an instantiation of this strategy for first-order tableaux that handles notably δ++ rules, which is, as far as the authors know, the first one in the literature. Additionally, this deskolemization strategy has been implemented in the Goéland automated theorem prover, enabling an export of its proofs in Coq and Lambdapi. Finally, we have evaluated the algorithm performances for δ+ and δ++ rules through the certification of proofs from some categories of the TPTP library.

ABSTRACT. Algorithm certification or program verification have an increasing importance in the current technological landscape, due to the sharp increase in the complexity of software and software using systems and the high potential of adverse effects in case of failure. For instance robots constitute a particular class of systems that can present high risks of such failures. Sorting on the other hand has a growing area of applications, in particular the ones where organizing huge data collections is critical, as for instance in environmental applications.

We present an experiment in formal certification of an original version of the Bubble-Sort algorithm that is functional and tail recursive. The certification is performed in parallel both in Theorema and in Coq, this allows to compare the characteristics and the performance of the two systems. In Theorema the proofs are produced automatically in natural style (similar to human proofs), while in Coq they are based on scripts. However, the background theory, the algorithms, and the proof rules in \tma are composed by the user without any restrictions -- thus error prone, while in Coq one can only use the theories and the proof rules that are rigurously checked by the system, and the algorithms are checked for termination.

The goal of our experiments is to contribute to a better understanding and estimation of the complexity of such certification tasks and to create a basis for further increase of the level of automation in the two systems and for their possible integration.