Formal Verification of a Constant-Time Preserving C Compiler

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

DOI

  • Gilles Barthe
  • ,
  • Sandrine Blazy
  • ,
  • Benjamin Grégoire
  • ,
  • Rémi Hutin
  • ,
  • Vincent Laporte
  • ,
  • David Pichardie
  • ,
  • Alix Trieu
Original languageEnglish
Article number7
JournalProceedings of the ACM on Programming Languages
Volume4
IssuePOPL
Number of pages30
DOIs
Publication statusPublished - 2020
EventThe 47th ACM SIGPLAN Symposium on Principles of Programming Languages - New Orleans, United States
Duration: 22 Jan 202024 Jan 2020
Conference number: 2020
https://popl20.sigplan.org/

Conference

ConferenceThe 47th ACM SIGPLAN Symposium on Principles of Programming Languages
Number2020
CountryUnited States
CityNew Orleans
Period22/01/202024/01/2020
Internet address

    Research areas

  • CompCert compiler, timing side-channels, verified compilation

See relations at Aarhus University Citationformats

ID: 176035995