Andrea Gilot

dblp:372/4059 · DBLP profile ↗
← Back
3ranked-venue papers
2as first author
3since 2021 · last 2026
0009-0006-4463-9414ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 2 first-author · 2 since 2021Theory of computation · 1 · 1 since 2021
YearPublicationVenuePosition
2026 Verifying Floating-Point Programs in Stainless
Andrea Gilot, Axel Bergström, Eva Darulova
TACAS (2)1
2026 Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages
abstract
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.
Andrea Gilot, Tobias Wrigstad, Eva Darulova
Proc. ACM Program. Lang.1
2024 Mechanized HOL Reasoning in Set Theory
Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak
ITP3