| [9] | Samuel Gruetter.
 Techniques for Foundational End-to-End Verification of
  Systems Stacks.
 PhD thesis, MIT, September 2024. [ PDF ]
 | 
| [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 ]
 |