PLMW When: Tue 9 Jan 2018 14:30 - 15:00 People: Benjamin C. Pierce

… Writing well is hard for many reasons, but perhaps the hardest of all is what Steven Pinker calls “The Curse of Knowledge” — the difficulty of imagining ourselves inside the mind of someone who does not know something that we do know …

Off the Beaten Track 2018 When: Sat 13 Jan 2018 14:00 - 14:30 People: Annie Cherkaev, Sebastian Musslick, Jonathan Cohen, Vivek Srikumar, Matthew Flatt

… of all valid solutions. …

Off the Beaten Track 2018 When: Sat 13 Jan 2018 11:30 - 12:00 People: Brent Yorgey, Richard A. Eisenberg, Harley D. Eades III

… ", but ought to have all the tools of programming language theory and practice …

When: Sat 13 Jan 2018 14:25 - 14:50 People: Martin Bodin

… Real-world programming languages have subtle behaviours. In particular, their semantics is often associated with various corner cases. Programmers are sometimes unaware of all these corner cases, which can yield to serious bugs …

PADL 2018 When: Mon 8 Jan 2018 14:00 - 14:30 People: Todd Millstein

… Almost all languages today are memory safe, thereby providing simple and strong guarantees to all programs. Yet the concurrency semantics of these “safe” languages causes similar problems as arise in memory-unsafe languages: small program …

PADL 2018 When: Tue 9 Jan 2018 10:30 - 11:00 People: Karl Crary

… that are then instantiated by the programmer with appropriate action code. This results in all code …

PriSC 2018 When: Sat 13 Jan 2018 13:30 - 14:00 People: Anitha Gollamudi, Cédric Fournet

… to standalone C code. However, this does not account for all code running within … and for core libraries. Besides, we cannot expect all enclave applications …

PEPM 2018 When: Mon 8 Jan 2018 14:30 - 15:00 People: David Broman, Jeremy G. Siek

… , statically typed, and dynamically typed variants, all having their pros and cons …-specific modeling languages, all within the domain of physical modeling …

PEPM 2018 When: Tue 9 Jan 2018 15:00 - 15:30 People: Barry Jay

… that support queries of internal program structure. In all these settings …

PEPM 2018 When: Tue 9 Jan 2018 16:40 - 16:50 People: Cyprien Mangin, Matthieu Sozeau

… of all, we describe the splitting tree, the intermediate data structure used …

PriSC 2018 When: Sat 13 Jan 2018 14:00 - 14:30 People: Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Marco Stronati, David Swasey

… preservation of all hyperproperties, seems achievable for simple transformations …

PriSC 2018 When: Sat 13 Jan 2018 11:35 - 11:40 People: William J. Bowman

… cannot express all security invariants we wish to enforce. Dependent types could …

PriSC 2018 When: Sat 13 Jan 2018 16:30 - 17:00 People: Rob Sison

… Domain Desktop Compositor, and instantiated all of the related proofs of security …

PriSC 2018 When: Sat 13 Jan 2018 14:30 - 15:00 People: Guglielmo Fachini, Cătălin Hriţcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach

… . Each component is protected from all the others until it receives an input …

PriSC 2018 When: Sat 13 Jan 2018 09:10 - 10:00 People: Mathias Payer

… into a derived class. A type sanitizer tracks the types of all objects and makes …

Research Papers When: Wed 10 Jan 2018 09:45 - 10:05

… 1-minute overview of all the talks on Day 1. …

Research Papers When: Fri 12 Jan 2018 09:30 - 10:00

… 1-minute overview of all the talks on Day 3. …

Research Papers When: Thu 11 Jan 2018 09:30 - 10:00

… 1-minute overview of all the talks on Day 2. …

CPP 2018 When: Tue 9 Jan 2018 14:00 - 14:30 People: Denis Firsov, Aaron Stump

… products,
primitive heterogeneous equality, and dependent intersections.
All …

CPP 2018 When: Mon 8 Jan 2018 11:30 - 12:00 People: Christian Doczkal, Joachim Bard

… without converse and then extend the proofs to Converse PDL. All results …

PPS 2018 When: Tue 9 Jan 2018 11:30 - 12:00 People: Daniel Selsam

… correctly on all inputs using tools from software verification and formal mathematics. …

PPS 2018 When: Tue 9 Jan 2018 15:00 - 15:30 People: Praveen Narayanan, Chung-chieh Shan

… . The conditioning tool applies uniform reasoning across all three kinds of applications. …

CPP 2018 When: Mon 8 Jan 2018 09:00 - 10:00 People: Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada

…
involves the computation of all eigenvalues of $A$, which
often leads to expensive …

CPP 2018 When: Tue 9 Jan 2018 17:30 - 18:00 People: Jonas Kaiser, Steven Schäfer, Kathrin Stark

… foundation of future versions of the Autosubst Coq library. All developments …

CPP 2018 When: Mon 8 Jan 2018 13:30 - 14:00 People: Conrad Watt

… <p>WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js …

CPP 2018 When: Tue 9 Jan 2018 11:30 - 12:00 People: Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

… : it assumes that all theory modules produce proof objects and it accommodates …

CPP 2018 When: Mon 8 Jan 2018 14:30 - 15:00 People: George Pîrlea, Ilya Sergey

… consensus, and discuss their adequacy.

All results described in this paper …

CPP 2018 When: Mon 8 Jan 2018 16:00 - 16:30 People: Craig McLaughlin, James McKinna, Ian Stark

… to a CIU result formulated with frame stacks.

All this is formalised and proved …

Research Papers When: Wed 10 Jan 2018 14:30 - 14:55 People: John Peter Campora, Sheng Chen, Martin Erwig, Eric Walkingshaw

… as possible, in general, all possible combinations of adding or removing type annotations … this problem by developing migrational typing, which efficiently types all …

Artifact Evaluation People: John Peter Campora, Sheng Chen, Martin Erwig, Eric Walkingshaw

… , in general, all possible combinations of adding or removing type annotations from … this problem by developing \emph{migrational typing}, which efficiently types all possible …

Artifact Evaluation People: Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

… . By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding the DAO or contracts …

Research Papers When: Fri 12 Jan 2018 11:45 - 12:10 People: Shelly Grossman, Ittai Abraham, Guy Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

… and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding …

Research Papers When: Fri 12 Jan 2018 15:50 - 16:15 People: Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal

… formalized all the technical development and results in Coq. …

Artifact Evaluation People: Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal

… formalized all the technical development and results in Coq. …

Artifact Evaluation People: Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

… discovery. So contract verification aims to guarantee all or most … functions, modularity, and statefulness. Our approach tackles all these features … 99.94% of checks statically (all but 28 of 51,713).

Stateful, higher-order …

Research Papers When: Fri 12 Jan 2018 11:20 - 11:45 People: Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

… discovery. So contract verification aims to guarantee all or most … functions, modularity, and statefulness. Our approach tackles all these features … 99.94% of checks statically (all but 28 of 51, 713).

Stateful, higher-order …

Research Papers When: Thu 11 Jan 2018 13:40 - 14:05 People: Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen

… We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its …

Artifact Evaluation People: Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki

… Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts …

Research Papers When: Thu 11 Jan 2018 16:15 - 16:40 People: Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki

… Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define …

Research Papers When: Thu 11 Jan 2018 14:55 - 15:20 People: Stephen Chang, Alex Knauth, Emina Torlak

… 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 …

Artifact Evaluation People: Stephen Chang, Alex Knauth, Emina Torlak

… We present \lcsym, a typed $\lambda$-calculus for \emph{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 …

Research Papers When: Wed 10 Jan 2018 11:45 - 12:10 People: Lukáš Holík, Anthony Widjaja Lin, Petr Janků, Philipp Ruemmer, Tomáš Vojnar

… the importance of incorporating the replace-all operator (i.e. replace all …

Artifact Evaluation People: Lukáš Holík, Petr Janků, Anthony Widjaja Lin, Philipp Ruemmer, Tomáš Vojnar

… the importance of incorporating the replace-all operator (i.e. replace all …

Research Papers When: Thu 11 Jan 2018 11:45 - 12:10 People: Ilya Sergey, James R. Wilcox, Zachary Tatlock

… commit), so all their internal invariants hold, and (b) correctly composing … verification of distributed systems and their clients, all within the mechanized …

Artifact Evaluation People: Ilya Sergey, James R. Wilcox, Zachary Tatlock

… commit), so all their internal invariants hold, and (b) correctly composing … verification of distributed systems and their clients, all within the mechanized …

TutorialFest When: Mon 8 Jan 2018 09:00 - 10:30Mon 8 Jan 2018 11:00 - 12:00 People: Roberto Giacobazzi

… these attacks. Attacks are inhibited by maximising imprecision in all attempts made …

TutorialFest When: Mon 8 Jan 2018 16:00 - 17:00Mon 8 Jan 2018 14:00 - 15:30 People: Zachary Kincaid, Thomas Reps

… converging upon a property that over-approximates all of the reachable states …

Research Papers When: Wed 10 Jan 2018 11:20 - 11:45 People: Taolue Chen, Yan Chen, Matthew Hague, Anthony Widjaja Lin, Zhilin Wu

… either the first occurrence or all occurrences of a ``pattern'' string constant … of the string-replace function (especially the replace-all facility) is increasingly …

Artifact Evaluation People: Jeevana Priya Inala, Rishabh Singh

… the URLs for the webpages containing the desired data for all rows …

Research Papers When: Wed 10 Jan 2018 10:55 - 11:20 People: Jeevana Priya Inala, Rishabh Singh

… generates the URLs for the webpages containing the desired data for all rows …

Research Papers When: Wed 10 Jan 2018 16:40 - 17:05 People: Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell

… before becoming visible to all — but this has not been exploited in production …

Artifact Evaluation People: Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell

… becoming visible to all — but this has not been exploited in production …

Research Papers When: Thu 11 Jan 2018 14:05 - 14:30 People: Dominique Devriese, Marco Patrignani, Frank Piessens

… '' type, i.e., a type where all other types can be injected to and extracted from …

Artifact Evaluation People: Gagandeep Singh, Markus Püschel, Martin Vechev

… domains to benefit from decomposition without re-writing all …

Research Papers When: Fri 12 Jan 2018 14:30 - 14:55 People: Gagandeep Singh, Markus Püschel, Martin Vechev

… of abstract domains to benefit from decomposition without re-writing all …

Research Papers When: Thu 11 Jan 2018 10:55 - 11:20 People: Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

… after satisfying all fairness constraints). However, with both infinitely many …

Artifact Evaluation People: Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

… satisfying all fairness constraints). However, with both infinitely many states …

Research Papers When: Thu 11 Jan 2018 10:55 - 11:20 People: Krishnendu Chatterjee, Andreas Pavlogiannis, Bhavya Choudhary

… demonstrates that the new algorithms significantly outperform all existing methods …

Artifact Evaluation People: Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis

… demonstrates that the new algorithms significantly outperform all existing methods …

Artifact Evaluation People: Nada Amin, Tiark Rompf

… Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass …

Research Papers When: Fri 12 Jan 2018 11:45 - 12:10 People: Nada Amin, Tiark Rompf

… Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass …

Research Papers When: Wed 10 Jan 2018 08:45 - 09:45 People: Derek Dreyer

… .

Unfortunately, syntactic type soundness is a rather weak theorem. First of all, its …