From 7e73eca042a5470763ff5ec785b395af8c526a55 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 Mar 2021 19:20:39 +0000 Subject: Add references --- references.bib | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/references.bib b/references.bib index 3e2ed3d..024f053 100644 --- a/references.bib +++ b/references.bib @@ -346,3 +346,17 @@ url = {https://github.com/project-oak/silveroak}, abstract = "The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context, on a weakly-consistent-shared-memory machine.", isbn = "978-3-642-19718-5" } + +@article{barthe20_formal_c, + doi = {10.1145/3371075}, + url = {https://doi.org/10.1145/3371075}, + year = {2020}, + month = jan, + publisher = {Association for Computing Machinery ({ACM})}, + volume = {4}, + number = {{POPL}}, + pages = {1--30}, + author = {Gilles Barthe and Sandrine Blazy and Benjamin Gr{\'{e}}goire and R{\'{e}}mi Hutin and Vincent Laporte and David Pichardie and Alix Trieu}, + title = {Formal verification of a constant-time preserving C compiler}, + journal = {Proceedings of the {ACM} on Programming Languages} +} -- cgit