arXiv subjects

Andrea Gilot

Publications and source records attributed to Andrea Gilot.

3 recordsLinked to original sources

arXiv2026

Verifying Floating-Point Programs in Stainless

We extend the Stainless deductive verifier with floating-point support, providing the first automated verification support for floating-point numbers for a subset of Scala that includes polymorphism, recursion and higher-order functions. We follow the recent approach in the KeY verifier to axiomatise reasoning about mathematical functions, but go further by supporting all functions from Scala's math API, and by verifying the correctness of the axioms against the actual implementation in Stainless itself. We validate Stainless' floating-point support on a new set of benchmarks sampled from real-world code from GitHub, showing that it can verify specifications about, e.g., ranges of output or absence of special values for most supported functions, or produce counter-examples when the specifications do not hold.

cs.PL↗

arXiv2025

Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages

Reasoning about floating-point arithmetic is notoriously hard. While static and dynamic analysis techniques or program repair have made significant progress, more work is still needed to make them relevant to real-world code. On the critical path to that goal is understanding what real-world floating-point code looks like. To close that knowledge gap, this paper presents the first large-scale empirical study of floating-point arithmetic usage across public GitHub repositories. We focus on statically typed languages to allow our study to scale to millions of repositories. We follow state-of the art mining practices including random sampling and filtering based on only intrinsic properties to avoid bias, and identify floating-point usage by searching for keywords in the source code, and programming language constructs (e.g., loops) by parsing the code. Our evaluation supports the claim often made in papers that floating-point arithmetic is widely used. Comparing statistics such as size and usage of certain constructs and functions, we find that benchmarks used in literature to evaluate automated reasoning techniques for floating-point arithmetic are in certain aspects representative of 'real-world' code, but not in all. We publish a dataset of 10 million real-world floating-point functions extracted from our study. We demonstrate in a case study how it may be used to identify new floating-point benchmarks and help future techniques for floating-point arithmetic to be designed and evaluated to match actual users' expectations.

cs.PL↗

arXiv2024

Mechanized HOL Reasoning in Set Theory

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory. HOL proof steps are implemented as proof producing tactics in Lisa, and the types are interpreted as sets, with function (or arrow) types coinciding with set-theoretic function spaces. The embedded HOL proofs, as opposed to being a layer over the existing proofs, are interoperable with the existing library. This yields a form of soft type system supporting top-level polymorphism and ADTs over set theory, and offer tools to reason about functions in set theory.

cs.LO↗