VLDB 2026 Research / reviewers in the wild / expert
Andrea Gilot
dblp:372/4059
· DBLP profile ↗
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
| Year | Publication | Venue | Position |
|---|---|---|---|
| 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 LanguagesabstractReasoning 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 |
ITP | 3 |