5 papers
Reformalization of the Jordan Curve Theorem
Simon Guilloud, Sankalp Gambhir, Samuel Chassot
We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant.…
SVSHI: Secure and Verified Smart Home Infrastructure
Andrea Veneziano, Samuel Chassot
Smart infrastructures uses are growing and with them the need for dependability and correctness. To provide better correctness guarantees and bring formal verification into the equ…
Development of a NIC driver in C#
Samuel Chassot
Drivers have a special status among the developer community that sees them as mysterious and inaccessible. We think their extensive communication with the hardware and their need o…
Verifying a Realistic Mutable Hash Table
Samuel Chassot, Viktor Kunčak
In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a re…
Few-Shot Unsupervised Image-to-Image Translation on complex scenes
Luca Barras, Samuel Chassot, Daniel Filipe Nunes Silva
Unsupervised image-to-image translation methods have received a lot of attention in the last few years. Multiple techniques emerged tackling the initial challenge from different pe…