title = {{{VST}}-{{Floyd}}: {{A Separation Logic Tool}} to {{Verify Correctness}} of {{C Programs}}},
  volume = {61},
  issn = {0168-7433, 1573-0670},
  shorttitle = {{{VST}}-{{Floyd}}},
  doi = {10.1007/s10817-018-9457-5},
  abstract = {The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert C light. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.},
  language = {en},
  number = {1-4},
  urldate = {2018-07-12},
  journal = {Journal of Automated Reasoning},
  url = {},
  author = {Cao, Qinxiang and Beringer, Lennart and Gruetter, Samuel and Dodds, Josiah and Appel, Andrew W.},
  month = jun,
  year = {2018},
  pages = {367-422}
  title = {The {{Essence}} of {{Dependent Object Types}}},
  doi = {10.1007/978-3-319-30936-1_14},
  abstract = {Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-$<$: of dependent functions, it adds records, intersections and recursion to arrive at DOT, a calculus for dependent object types. The paper shows an encoding of System F with subtyping in D-$<$: and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it. Amin, Nada; Gr\"utter, Karl Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro},
  language = {en},
  urldate = {2018-11-28},
  journal = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
  url = {},
  author = {Amin, Nada and Gruetter, Samuel and Odersky, Martin and Rompf, Tiark and Stucki, Sandro},
  year = {2016},
  pages = {249-272}
  title = {Watch Them {{Fight}}! {{Creativity Task Tournaments}} of the {{Swiss Olympiad}} in {{Informatics}}},
  volume = {10},
  issn = {18227732, 23358955},
  doi = {10.15388/ioi.2016.05},
  abstract = {As part of the qualification process for the Swiss Olympiad in Informatics, the contestants are each year confronted with one ``Creativity Task''. Unlike typical problems in programming competitions, creativity tasks usually do not have an optimal solution, and are often adaptations of popular board or computer games. After receiving all submissions, a tournament is organized, where the students can watch how their programs play interactively against each other, and points are awarded to the authors according to the tournament ranking.},
  language = {en},
  number = {1},
  urldate = {2018-11-28},
  journal = {Olympiads in Informatics},
  url = {},
  author = {Gruetter, Samuel and Graf, Daniel and Schmid, Benjamin},
  month = jul,
  year = {2016},
  pages = {73-85}
  address = {Dallas, Texas, USA},
  title = {Short {{Paper}}: {{Towards Information Flow Reasoning}} about {{Real}}-{{World C Code}}},
  isbn = {978-1-4503-5099-0},
  shorttitle = {Short {{Paper}}},
  doi = {10.1145/3139337.3139345},
  abstract = {Strangely, despite much recent success proving information flow control (IFC) security for C programs, little work has investigated how to prove IFC security directly against C code, as opposed to over an abstract specification. We consider what a suitable IFC logic for C might look like, and propose a suitable continuation-passing style IFC security definition for C code. We discuss our ongoing work implementing these ideas in the context of an existing full-featured, sound program verification framework for C, the Verified Software Toolchain, supported by the verified C complier CompCert.},
  language = {en},
  urldate = {2018-11-28},
  booktitle = {Proceedings of the 2017 {{Workshop}} on {{Programming Languages}} and {{Analysis}} for {{Security}}  - {{PLAS}} '17},
  publisher = {{ACM Press}},
  url = {},
  author = {Gruetter, Samuel and Murray, Toby},
  year = {2017},
  pages = {43-48}