ETH Zurich Systems Group
STF H 313
Stampfenbachstrasse 114
8092 Zürich
Switzerland
I am a postdoc working with Prof. Timothy (Mothy) Roscoe’s group, in the Systems Group of the Department of Computer Science at ETH Zürich.
I did my PhD at MIT CSAIL with Prof. Adam Chlipala’s group, working on machine-checked end‑to‑end proofs about software-hardware stacks for simple bare-metal embedded systems.
Now, as a postdoc in Mothy’s group, I am excited to learn about real operating systems and to apply formal methods to systems research.
Trouble combining undefined behavior and nondeterminism? ➔ Try omnisemantics!
While working on Bedrock2, my colleague Andres Erbsen and me came up with a style of programming language semantics that we think works much better in the presence of undefined behavior and nondeterminism than using traditional smallstep or bigstep operational semantics would. A little later, our advisor Adam Chlipala chatted with Arthur Charguéraud and they found out that he had discovered the same style of semantics as well, but was using it for functional languages, while we were using it for imperative languages. Together, we wrote a paper about it, or if you prefer just a short introduction, you can also check out this blog post.
Past Projects
- I was visiting Dr. Toby Murray at the University of Melbourne for 10 weeks to work on information flow control proofs for C
- For a six months master thesis internship, I was working with Prof. Andrew Appel’s group at Princeton, improving the proof automation tactics of their Verified Software Toolchain, and using it to verify the AES encryption implementation of mbed TLS
- During my master’s at EPFL, I was working with Prof. Martin Odersky’s Scala lab on the Dependent Object Types project, a formalization of the core of Scala’s type system, writing proofs on paper and using the proof assistants Twelf and Coq
- For a class project at EPFL, I contributed to the function termination checker of Leon, a tool for verification and synthesis of Scala programs by Prof. Viktor Kuncak’s group
- While working at the Scala lab, I contributed to dotty, a new Scala compiler serving as a research platform to investigate new language concepts and compiler technologies for Scala
- For my bachelor thesis, I designed, explored and implemented a simple structurally typed language in PLT redex
Publications
[10] |
Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala.
Verifying Software Emulation of an Unsupported Hardware
Instruction.
15th International Conference on Interactive Theorem Proving
(ITP 2024), 309, September 2024. [ DOI | PDF | code ] |
[9] |
Samuel Gruetter, Viktor Fukala, and Adam Chlipala.
Live Verification in an Interactive Proof Assistant.
Proceedings of the ACM on Programming Languages, 8(PLDI), June
2024. [ DOI | PDF | code ] |
[8] |
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter,
Clément Pit-Claudel, and Adam Chlipala.
Foundational Integration Verification of a Cryptographic
Server.
Proceedings of the ACM on Programming Languages, 8(PLDI), June
2024. [ DOI | PDF | code ] |
[7] |
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh,
Andy Wright, and Adam Chlipala.
Flexible Instruction-Set Semantics via Abstract Monads
(Experience Report).
Proceedings of the ACM on Programming Languages, 7(ICFP),
August 2023. [ DOI | PDF | code ] |
[6] |
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter.
Omnisemantics: Smooth Handling of Nondeterminism.
ACM Transactions on Programming Languages and Systems, 45(1),
March 2023. [ DOI | PDF | code ] |
[5] |
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala.
Integration Verification Across Software and Hardware for a
Simple Embedded System.
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, June 2021. [ DOI | PDF | code ] |
[4] |
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W.
Appel.
VST-Floyd: A Separation Logic Tool to Verify Correctness
of C Programs.
Journal of Automated Reasoning, 61(1-4), June 2018. [ DOI | PDF | code ] |
[3] |
Samuel Gruetter and Toby Murray.
Short Paper: Towards Information Flow Reasoning about
Real-World C Code.
PLAS '17: Proceedings of the 2017 Workshop on Programming
Languages and Analysis for Security, October 2017. [ DOI | PDF | code ] |
[2] |
Samuel Gruetter, Daniel Graf, and Benjamin Schmid.
Watch them Fight! Creativity Task Tournaments of the Swiss
Olympiad in Informatics.
Olympiads in Informatics, 10(1), July 2016. [ DOI | PDF | code ] |
[1] |
Nada Amin, Samuel Gruetter, Martin Odersky, Tiark Rompf, and Sandro Stucki.
The Essence of Dependent Object Types.
A List of Successes That Can Change the World: Essays Dedicated
to Philip Wadler on the Occasion of His 60th Birthday, Lecture Notes in
Computer Science LNTCS, volume 9600, March 2016. [ DOI | PDF | code ] |
Preprints, Theses, Reports
[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 ] |
Education
- September 2024: PhD in Computer Science at MIT with Prof. Adam Chlipala’s Programming Languages and Verification Group
- April 2017: MSc in Computer Science from EPFL in Lausanne, Switzerland
- July 2013: BSc in Computer Science from EPFL
Industry Experience
- Summer 2021: At Google Research, worked on the Silver Oak Project, using Bedrock2 to formally verify drivers for peripherals used in the OpenTitan root of trust, and connected software correctness proofs to hardware correctness proofs
- Summer 2019: Worked with Rustan Leino at Amazon’s Automated Reasoning Group on a prototype rewrite of Amazon’s S3 Encryption Client in Dafny, a verification-aware programming language. Wrote and proved specifications for software interacting with real-world systems such as Amazon’s S3 storage service
- Fall 2015: 6 months Software Engineering Internship at Netcetera AG, Berne, working in a scrum team, developing a Web Application with a Java/Oracle DB/Spring backend and an AngularJS/TypeScript frontend
- Summer 2012: Java Internship at Accenture in Bangalore (India), developed a web interface with JSF/Enterprise JavaBeans monitoring hundreds of servers and databases