Samuel Gruetter: Publications
| ITP’24 | Gruetter, Samuel; Bourgeat, Thomas; Chlipala, Adam. Verifying Software Emulation of an Unsupported Hardware Instruction. 15th International Conference on Interactive Theorem Proving (ITP 2024), September 2024. [DOI | PDF | code] |
| PLDI’24 | Erbsen, Andres; Philipoom, Jade; Jamner, Dustin; Lin, Ashley; Gruetter, Samuel; Pit-Claudel, Clément; Chlipala, Adam. Foundational Integration Verification of a Cryptographic Server. Proceedings of the ACM on Programming Languages (PLDI), June 2024. [DOI | PDF | code] |
| PLDI’24 | Gruetter, Samuel; Fukala, Viktor; Chlipala, Adam. Live Verification in an Interactive Proof Assistant. Proceedings of the ACM on Programming Languages (PLDI), June 2024. [DOI | PDF | code] |
| ICFP’23 | Bourgeat, Thomas; Clester, Ian; Erbsen, Andres; Gruetter, Samuel; Singh, Pratap; Wright, Andy; Chlipala, Adam. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the ACM on Programming Languages (ICFP), August 2023. [DOI | PDF | code] |
| TOPLAS’23 | Charguéraud, Arthur; Chlipala, Adam; Erbsen, Andres; Gruetter, Samuel. Omnisemantics: Smooth Handling of Nondeterminism. ACM Transactions on Programming Languages and Systems (1), March 2023. [DOI | PDF | code] |
| PLDI’21 | Erbsen, Andres; Gruetter, Samuel; Choi, Joonwon; Wood, Clark; Chlipala, Adam. 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] |
| JAR’18 | Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning (1-4), June 2018. [DOI | PDF | code] |
| PLAS’17 | Gruetter, Samuel; Murray, Toby. 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] |
| IOI’16 | Gruetter, Samuel; Graf, Daniel; Schmid, Benjamin. Watch them Fight! Creativity Task Tournaments of the Swiss Olympiad in Informatics. Olympiads in Informatics (1), July 2016. [DOI | PDF | code] |
| WF’16 | Amin, Nada; Gruetter, Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro. 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 (WadlerFest) (Lecture Notes in Computer Science LNTCS, volume 9600), March 2016. [DOI | PDF | code] |