diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-24 19:20:39 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-24 19:20:39 +0000 |
| commit | 7e73eca042a5470763ff5ec785b395af8c526a55 (patch) | |
| tree | 84ea39620738c791895fbd4a011323bcab03cc3d | |
| parent | bc25a4379c36e16eedea1ad3d4484b6af26c1650 (diff) | |
| download | latte21_hlstpc-7e73eca042a5470763ff5ec785b395af8c526a55.tar.gz latte21_hlstpc-7e73eca042a5470763ff5ec785b395af8c526a55.zip | |
Add references
| -rw-r--r-- | references.bib | 14 |
1 files changed, 14 insertions, 0 deletions
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} +} |