|
[9]
|
Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala.
Verifying Software Emulation of an Unsupported Hardware
Instruction.
March 2024.
[ PDF |
code ]
|
|
[8]
|
Samuel Gruetter.
Counterexamples for Coq Conjectures.
CoqPL'19, January 2019.
[ PDF |
code ]
|
|
[7]
|
Samuel Gruetter and Toby C. Murray.
VST-Flow: Fine-grained low-level reasoning about real-world
C code.
Technical report, University of Melbourne, September 2017.
[ PDF |
code ]
|
|
[6]
|
Samuel Gruetter.
Improving the Coq proof automation tactics of the Verified
Software Toolchain, based on a case study on verifying a C
implementation of the AES encryption algorithm.
MSc thesis, EPFL/Princeton University, April 2017.
[ PDF |
code ]
|
|
[5]
|
Samuel Gruetter.
Connecting Scala to DOT.
MSc semester project, EPFL, June 2016.
[ PDF |
code ]
|
|
[4]
|
Samuel Gruetter.
Dependent Object Types With Existential Quantification Over
Objects.
Research report, EPFL, July 2015.
[ PDF |
code ]
|
|
[3]
|
Samuel Gruetter.
Improving Leon's Termination Checker.
Project report, EPFL, June 2015.
[ PDF |
code ]
|
|
[2]
|
Samuel Gruetter.
Machine-checked typesafety proofs.
MSc semester project, EPFL, June 2014.
[ PDF |
code ]
|
|
[1]
|
Samuel Gruetter.
Explorations of type systems.
BSc semester project, EPFL, June 2013.
[ PDF |
code ]
|