Testing a Formally Verified Compiler (TAP 2023 - TAP Research Papers)

Who

David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel

Track

TAP 2023 Research Papers

Time Zone

The program is currently displayed in (GMT+01:00) London.

Use conference time zone: (GMT+01:00) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 18 Jul 2023 14:30 - 15:00 at Oak - TAP Session 2: Low-level code verification Chair(s): Julien Signoles

Abstract

This short paper reports on how we combine tests and formal proofs while developing extensions to the CompCert formally verified compiler. The paper illustrates that even a formally verified software may still need extensive testing.

Link to Preprint

https://hal.science/hal-04096390/

DOI

https://doi.org/10.1007/978-3-031-38828-6_3

David MonniauxPresenter

CNRS/VERIMAG

France

Léo Gourdin

Université Grenoble Alpes, Verimag

France

Sylvain Boulmé

Grenoble Alps University / CNRS / Grenoble INP / VERIMAG

France

Olivier Lebeltel

Université Grenoble Alpes, CNRS, Verimag

France

Time Zone

The program is currently displayed in (GMT+01:00) London.

Use conference time zone: (GMT+01:00) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Tue 18 Jul
Displayed time zone: London change

13:30 - 15:00	TAP Session 2: Low-level code verificationResearch Papers at Oak Chair(s): Julien Signoles Université Paris-Saclay, CEA, List Remote Participants: Zoom Link

13:30 30m Talk		BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries Research Papers P: Daniel Engel Open University Of The Netherlands, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech DOI Pre-print File Attached
14:00 30m Talk		Low-level Reachability Analysis based on Formal Logic Research Papers P: Nico Naus Virginia Tech, Freek Verbeek Open University of the Netherlands, The Netherlands, Marc Schoolderman Radboud University Nijmegen, Binoy Ravindran Virginia Tech DOI Pre-print
14:30 30m Talk		Testing a Formally Verified Compiler Research Papers P: David Monniaux CNRS/VERIMAG, Léo Gourdin Université Grenoble Alpes, Verimag, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Olivier Lebeltel Université Grenoble Alpes, CNRS, Verimag DOI Pre-print