Thu 11 Jan 2018 14:55 - 15:20 at Watercourt - Outside the box Chair(s): Lars Birkedal

We present \lcsym, a typed $\lambda$-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base occurrence typing system with symbolic types and mutable state, making it a suitable model for both functional and imperative symbolically executed languages. Naively allowing mutation in this mixed setting introduces soundness issues, however, so we further add concreteness polymorphism, which restores soundness without rejecting too many valid programs. To show that our calculus is a useful model for a real language, we implemented Typed Rosette, a typed extension of the solver-aided Rosette language. We evaluate Typed Rosette by porting a large code base, demonstrating that our type system accommodates a wide variety of symbolically executed programs.

Thu 11 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:40 - 15:20: Research Papers - Outside the box at Watercourt
Chair(s): Lars BirkedalAarhus University
POPL-2018-papers13:40 - 14:05
Siddharth KrishnaNew York University, Dennis ShashaNew York University, Thomas WiesNew York University
POPL-2018-papers14:05 - 14:30
Dominique DevrieseKU Leuven, Marco PatrignaniSaarland University, CISPA, Frank PiessensKU Leuven
POPL-2018-papers14:30 - 14:55
Pierre ClairambaultCNRS & ENS Lyon, Charles GrelloisINRIA Sophia Antipolis & Aix-Marseille Université, Andrzej MurawskiUniversity of Oxford
POPL-2018-papers14:55 - 15:20
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Emina TorlakUniversity of Washington