| VST-Floyd: A separation logic tool to verify correctness of C programs Q Cao, L Beringer, S Gruetter, J Dodds, AW Appel Journal of Automated Reasoning 61, 367-422, 2018 | 121 | 2018 |
| The essence of dependent object types N Amin, S Grütter, M Odersky, T Rompf, S Stucki A List of Successes That Can Change the World: Essays Dedicated to Philip …, 2016 | 120 | 2016 |
| Integration verification across software and hardware for a simple embedded system A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 56 | 2021 |
| A multipurpose formal risc-v specification T Bourgeat, I Clester, A Erbsen, S Gruetter, A Wright, A Chlipala arXiv preprint arXiv:2104.00762, 2021 | 14 | 2021 |
| Omnisemantics: Smooth handling of nondeterminism A Charguéraud, A Chlipala, A Erbsen, S Gruetter ACM Transactions on Programming Languages and Systems 45 (1), 1-43, 2023 | 11 | 2023 |
| Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI’21 (2021) A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala | 8 | 2021 |
| Flexible instruction-set semantics via abstract monads (experience report) T Bourgeat, I Clester, A Erbsen, S Gruetter, P Singh, A Wright, A Chlipala Proceedings of the ACM on Programming Languages 7 (ICFP), 108-124, 2023 | 7 | 2023 |
| VST-Floyd: A separation logic tool to verify correctness of C programs. JAR 61, 1-4 (2018), 367–422 Q Cao, L Beringer, S Gruetter, J Dodds, AW Appel | 7 | 2018 |
| 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 S Grütter Princeton University, 2017 | 4* | 2017 |
| Foundational Integration Verification of a Cryptographic Server A Erbsen, J Philipoom, D Jamner, A Lin, S Gruetter, C Pit-Claudel, ... Proceedings of the ACM on Programming Languages 8 (PLDI), 1704-1729, 2024 | 3 | 2024 |
| Flexible Instruction-Set Semantics via Type Classes T Bourgeat, I Clester, A Erbsen, S Gruetter, P Singh, A Wright, A Chlipala arXiv preprint arXiv:2104.00762, 2021 | 2 | 2021 |
| Short paper: Towards information flow reasoning about real-world C code S Gruetter, T Murray Proceedings of the 2017 Workshop on Programming Languages and Analysis for …, 2017 | 2 | 2017 |
| Live Verification in an Interactive Proof Assistant S Gruetter, V Fukala, A Chlipala Proceedings of the ACM on Programming Languages 8 (PLDI), 1535-1558, 2024 | 1 | 2024 |
| Proving That a System with Software Trap Handlers for Unimplemented Instructions Behaves as If They Were Implemented in Hardware S Gruetter, T Bourgeat, A Chlipala Technical Report. https://samuelgruetter. net/assets/softmul. pdf, 2023 | 1 | 2023 |
| VST-Flow: Fine-grained low-level reasoning about real-world C code S Gruetter, T Murray arXiv preprint arXiv:1709.05243, 2017 | 1 | 2017 |
| Watch them fight! Creativity task tournaments of the Swiss Olympiad in Informatics S Grütter, D Graf, B Schmid Olympiads in Informatics 10, 73-85, 2016 | 1 | 2016 |
| Verifying Software Emulation of an Unsupported Hardware Instruction S Gruetter, T Bourgeat, A Chlipala 15th International Conference on Interactive Theorem Proving (ITP 2024), 2024 | | 2024 |
| Foundational Integration Verification of a Cryptographic Server J PHILIPOOM, D JAMNER, A LIN, S GRUETTER, C PIT-CLAUDEL, ... | | 2024 |
| Techniques for Foundational End-to-End Verification of Systems Stacks S Gruetter MASSACHUSETTS INSTITUTE OF TECHNOLOGY, 1888 | | 1888 |
| CPS Semantics: Smoother Nondeterminism in Operational Semantics A Charguéraud, A Chlipala, A Erbsen, S Gruetter | | |
