arXiv subjects

Francesco Ranzato

Publications and source records attributed to Francesco Ranzato.

At least 19 recordsLinked to original sources

arXiv2026

A Program Logic for Abstract (Hyper)Properties

We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program logics parameterised by an abstract domain, encompassing both existing and novel abstractions of properties and hyperproperties. The logic is grounded in a semantic framework where the meaning of commands is first defined on a lattice basis and then extended to the full lattice via additivity. Crucially, nondeterministic choice is interpreted by a monoidal operator that need not be idempotent nor coincide with the lattice join. This flexibility allows the framework to capture collecting semantics, various classes of abstract semantics, and hypersemantics. The APPL proof system is sound, and it is relatively complete whenever the property language is sufficiently expressive. When the property language is restricted to an abstract domain, the result is a sound abstract deduction system based on best correct approximations. Relative completeness with respect to a corresponding abstract semantics is recovered provided the abstract domain is complete, in the sense of abstract interpretation, for the monoidal operator.

cs.LO↗

arXiv2025

Model Checking as Program Verification by Abstract Interpretation (Extended Version)

Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language-called MOKA (for MOdel checking as abstract interpretation of Kleene Algebras)-which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal mu-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.

cs.LO↗

arXiv2023

Computing Reachable Simulations

We study the problem of computing the reachable principals of simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of the decidability and complexity aspects of this problem, which in particular highlights a stark contrast with the already settled case of bisimulation, we design algorithms to solve this problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. In particular, we put forward a symbolic algorithm processing state partitions and, in turn, relations between their blocks, which is suited for processing infinite state systems.

cs.LO↗

arXiv2022

Abstract Interpretation-Based Feature Importance for SVMs

We propose a symbolic representation for support vector machines (SVMs) by means of abstract interpretation, a well-known and successful technique for designing and implementing static program analyses. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure, called abstract feature importance (AFI), that does not depend in any way on a given dataset of the accuracy of the SVM and is very fast to compute, and (2) for verifying stability, notably individual fairness, of SVMs and producing concrete counterexamples when the verification fails. We implemented our approach and we empirically demonstrated its effectiveness on SVMs based on linear and non-linear (polynomial and radial basis function) kernels. Our experimental results show that, independently of the accuracy of the SVM, our AFI measure correlates much more strongly with the stability of the SVM to feature perturbations than feature importance measures widely available in machine learning software such as permutation feature importance. It thus gives better insight into the trustworthiness of SVMs.

cs.LG↗

arXiv2022

Local Completeness Logic on Kleene Algebra with Tests

Local Completeness Logic (LCL) has been put forward as a program logic for proving both the correctness and incorrectness of program specifications. LCL is an abstract logic, parameterized by an abstract domain that allows combining over- and under-approximations of program behaviors. It turns out that LCL instantiated to the trivial singleton abstraction boils down to O'Hearn incorrectness logic, which allows us to prove the presence of program bugs. It has been recently proved that suitable extensions of Kleene algebra with tests (KAT) allow representing both O'Hearn incorrectness and Hoare correctness program logics within the same equational framework. In this work, we generalize this result by showing how KATs extended either with a modal diamond operator or with a top element are able to represent the local completeness logic LCL. This is achieved by studying how these extended KATs can be endowed with an abstract domain so as to define the validity of correctness/incorrectness LCL triples and to show that the LCL proof system is logically sound and, under some hypotheses, complete.

cs.LO↗

arXiv2021

Intensional Kleene and Rice Theorems for Abstract Program Semantics

Classical results in computability theory, notably Rice's theorem, focus on the extensional content of programs, namely, on the partial recursive functions that programs compute. Later and more recent work investigated intensional generalisations of such results that take into account the way in which functions are computed, thus affected by the specific programs computing them. In this paper, we single out a novel class of program semantics based on abstract domains of program properties that are able to capture nonextensional aspects of program computations, such as their asymptotic complexity or logical invariants, and allow us to generalise some foundational computability results such as Rice's Theorem and Kleene's Second Recursion Theorem to these semantics. In particular, it turns out that for this class of abstract program semantics, any nontrivial abstract property is undecidable and every decidable over-approximation necessarily includes an infinite set of false positives which covers all the values of the semantic abstract domain.

cs.LO↗

arXiv2021

Complete Abstractions for Checking Language Inclusion

We study the language inclusion problem $L_1 \subseteq L_2$ where $L_1$ is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of $L_1$, obtained by overapproximating the Kleene iterates of its least fixpoint characterization, is included in $L_2$. We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words "greater than or equal to" a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms like the so-called antichain algorithms. Finally, we provide an equivalent language inclusion checking algorithm based on a greatest fixpoint computation that relies on quotients of languages and, to the best of our knowledge, was not previously known.

cs.FL↗

arXiv2021

Fair Training of Decision Tree Classifiers

We study the problem of formally verifying individual fairness of decision tree ensembles, as well as training tree models which maximize both accuracy and individual fairness. In our approach, fairness verification and fairness-aware training both rely on a notion of stability of a classification model, which is a variant of standard robustness under input perturbations used in adversarial machine learning. Our verification and training methods leverage abstract interpretation, a well established technique for static program analysis which is able to automatically infer assertions about stability properties of decision trees. By relying on a tool for adversarial training of decision trees, our fairness-aware learning method has been implemented and experimentally evaluated on the reference datasets used to assess fairness properties. The experimental results show that our approach is able to train tree models exhibiting a high degree of individual fairness w.r.t. the natural state-of-the-art CART trees and random forests. Moreover, as a by-product, these fair decision trees turn out to be significantly compact, thus enhancing the interpretability of their fairness properties.

cs.LG↗

arXiv2020

Genetic Adversarial Training of Decision Trees

We put forward a novel learning methodology for ensembles of decision trees based on a genetic algorithm which is able to train a decision tree for maximizing both its accuracy and its robustness to adversarial perturbations. This learning algorithm internally leverages a complete formal verification technique for robustness properties of decision trees based on abstract interpretation, a well known static program analysis technique. We implemented this genetic adversarial training algorithm in a tool called Meta-Silvae (MS) and we experimentally evaluated it on some reference datasets used in adversarial training. The experimental results show that MS is able to train robust models that compete with and often improve on the current state-of-the-art of adversarial training of decision trees while being much more compact and therefore interpretable and efficient tree models.

cs.LG↗

arXiv2020

Decidability and Synthesis of Abstract Inductive Invariants

Decidability and synthesis of inductive invariants ranging in a given domain play an important role in many software and hardware verification systems. We consider here inductive invariants belonging to an abstract domain $A$ as defined in abstract interpretation, namely, ensuring the existence of the best approximation in $A$ of any system property. In this setting, we study the decidability of the existence of abstract inductive invariants in $A$ of transition systems and their corresponding algorithmic synthesis. Our model relies on some general results which relate the existence of abstract inductive invariants with least fixed points of best correct approximations in $A$ of the transfer functions of transition systems and their completeness properties. This approach allows us to derive decidability and synthesis results for abstract inductive invariants which are applied to the well-known Kildall's constant propagation and Karr's affine equalities abstract domains. Moreover, we show that a recent general algorithm for synthesizing inductive invariants in domains of logical formulae can be systematically derived from our results and generalized to a range of algorithms for computing abstract inductive invariants.

cs.PL↗

arXiv2019

Robustness Verification of Support Vector Machines

We study the problem of formally verifying the robustness to adversarial examples of support vector machines (SVMs), a major machine learning model for classification and regression tasks. Following a recent stream of works on formal robustness verification of (deep) neural networks, our approach relies on a sound abstract version of a given SVM classifier to be used for checking its robustness. This methodology is parametric on a given numerical abstraction of real values and, analogously to the case of neural networks, needs neither abstract least upper bounds nor widening operators on this abstraction. The standard interval domain provides a simple instantiation of our abstraction technique, which is enhanced with the domain of reduced affine forms, which is an efficient abstraction of the zonotope abstract domain. This robustness verification technique has been fully implemented and experimentally evaluated on SVMs based on linear and nonlinear (polynomial and radial basis function) kernels, which have been trained on the popular MNIST dataset of images and on the recent and more challenging Fashion-MNIST dataset. The experimental results of our prototype SVM robustness verifier appear to be encouraging: this automated verification is fast, scalable and shows significantly high percentages of provable robustness on the test set of MNIST, in particular compared to the analogous provable robustness of neural networks.

cs.LG↗

arXiv2017

A new characterization of complete Heyting and co-Heyting algebras

We give a new order-theoretic characterization of a complete Heyting and co-Heyting algebra $C$. This result provides an unexpected relationship with the field of Nash equilibria, being based on the so-called Veinott ordering relation on subcomplete sublattices of $C$, which is crucially used in Topkis' theorem for studying the order-theoretic stucture of Nash equilibria of supermodular games.

cs.LO↗

arXiv2017

A Constructive Framework for Galois Connections

Abstract interpretation-based static analyses rely on abstract domains of program properties, such as intervals or congruences for integer variables. Galois connections (GCs) between posets provide the most widespread and useful formal tool for mathematically specifying abstract domains. Recently, Darais and Van Horn [2016] put forward a notion of constructive Galois connection for unordered sets (rather than posets), which allows to define abstract domains in a so-called mechanized and calculational proof style and therefore enables the use of proof assistants like Coq and Agda for automatically extracting verified algorithms of static analysis. We show here that constructive GCs are isomorphic, in a precise and comprehensive meaning including sound abstract functions, to so-called partitioning GCs--an already known class of GCs which allows to cast standard set partitions as an abstract domain. Darais and Van Horn [2016] also provide a notion of constructive GC for posets, which we prove to be isomorphic to plain GCs and therefore lose their constructive attribute. Drawing on these findings, we put forward and advocate the use of purely partitioning GCs, a novel class of constructive abstract domains for a mechanized approach to abstract interpretation. We show that this class of abstract domains allows us to represent a set partition with more flexibility while retaining a constructive approach to Galois connections.

cs.PL↗

arXiv2015

An Abstract Interpretation-based Model of Tracing Just-In-Time Compilation

Tracing just-in-time compilation is a popular compilation technique for the efficient implementation of dynamic languages, which is commonly used for JavaScript, Python and PHP. We provide a formal model of tracing JIT compilation of programs using abstract interpretation. Hot path detection corresponds to an abstraction of the trace semantics of the program. The optimization phase corresponds to a transform of the original program that preserves its trace semantics up to an observation modeled by some abstraction. We provide a generic framework to express dynamic optimizations and prove them correct. We instantiate it to prove the correctness of dynamic type specialization and constant variable folding. We show that our framework is more general than the model of tracing compilation introduced by Guo and Palsberg [2011] based on operational bisimulations.

cs.PL↗

arXiv2015

Abstract Interpretation of Supermodular Games

Supermodular games find significant applications in a variety of models, especially in operations research and economic applications of noncooperative game theory, and feature pure strategy Nash equilibria characterized as fixed points of multivalued functions on complete lattices. Pure strategy Nash equilibria of supermodular games are here approximated by resorting to the theory of abstract interpretation, a well established and known framework used for designing static analyses of programming languages. This is obtained by extending the theory of abstract interpretation in order to handle approximations of multivalued functions and by providing some methods for abstracting supermodular games, in order to obtain approximate Nash equilibria which are shown to be correct within the abstract interpretation framework.

cs.GT↗

arXiv2013

An Efficient Simulation Algorithm on Kripke Structures

A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let Sigma denote the state space, -> the transition relation and Psim the partition of Sigma induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is |Psim|^2, other algorithms are devised to attain the best time complexity O(|Psim||->|). We present a novel simulation algorithm which is both space and time efficient: it runs in O(|Psim|^2 log|Psim| + |Sigma|log|Sigma|) space and O(|Psim||->|log|Sigma|) time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity.

cs.LO↗

arXiv2013

Correctness Kernels of Abstract Interpretations

In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that approximate some concrete system behaviors under analysis. It may happen that an abstract domain contains redundant information for the specific purpose of approximating a given concrete semantic function. This paper introduces the notion of correctness kernel of abstract interpretations, a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that in abstract model checking correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that this simplification preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.

cs.PL↗

arXiv2009

Computing Stuttering Simulations

Stuttering bisimulation is a well-known behavioral equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorder induces a coarser behavioral equivalence that preserves the existential fragment ECTL-{X,G}, namely ECTL without the next-time X and globally G operators. While stuttering bisimulation equivalence can be computed by the well-known Groote and Vaandrager's [1990] algorithm, to the best of our knowledge, no algorithm for computing the stuttering simulation preorder and equivalence is available. This paper presents such an algorithm for finite state systems.

cs.LO↗