arXiv subjects

François Bobot

Publications and source records attributed to François Bobot.

7 recordsLinked to original sources

arXiv2026

The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification

The formal specification and verification of machine learning programs saw remarkable progress in less than a decade, leading to a profusion of tools. However, diversity may lead to fragmentation, resulting in tools that are difficult to compare, except for very specific benchmarks. Furthermore, this progress is heavily geared towards the specification and verification of a certain class of property, that is, local robustness properties. But while provers are becoming more and more efficient at solving local robustness properties, even slightly more complex properties, involving multiple neural networks for example, cannot be expressed in the input languages of winners of the International Competition of Verification of Neural Networks VNN-Comp. In this tool paper, we present CAISAR, an open-source platform dedicated to machine learning specification and verification. We present its specification language, suitable for modelling complex properties on neural networks, support vector machines and boosted trees. We show on concrete use-cases how specifications written in this language are automatically translated to queries to state-of-the-art provers, notably by using automated graph editing techniques, making it possible to use their off-the-shelf versions. The artifact to reproduce the paper claims is available at the following DOI: https://doi.org/10.5281/zenodo.15209510

cs.SE↗

arXiv2024

An SMT Theory for n-Indexed Sequences

The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory.

cs.LO↗

arXiv2024

On SMT Theory Design: The Case of Sequences

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.

cs.LO↗

arXiv2022

CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness

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 machine learning verification tools which, individually, are not able to efficiently handle all problems but, collectively, can cover a growing number of properties. Our aim is to assist, on the one hand, the V\&V process by reducing the burden of choosing the methodology tailored to a given verification problem, and on the other hand the tools developers by factorizing useful features-visualization, report generation, property description-in one platform. CAISAR will soon be available at https://git.frama-c.com/pub/caisar.

cs.AI↗

arXiv2020

A Deductive Verification Framework for Circuit-building Quantum Programs

While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.

cs.PL↗

arXiv2019

Deductive Proof of Ethereum Smart Contracts Using Why3

A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.

cs.PL↗

arXiv2017

CDCL-inspired Word-level Learning for Bit-vector Constraint Solving

The theory of quantifier-free bit-vectors (QF_BV) is of paramount importance in software verification. The standard approach for satisfiability checking reduces the bit-vector problem to a Boolean problem, leveraging the powerful SAT solving techniques and their conflict-driven clause learning (CDCL) mechanisms. Yet, this bit-level approach loses the structure of the initial bit-vector problem. We propose a conflict-driven, word-level, combinable constraints learning for the theory of quantifier-free bit-vectors. This work paves the way to truly word-level decision procedures for bit-vectors, taking full advantage of word-level propagations recently designed in CP and SMT communities.

cs.LO↗