POPL 2017
Sun 15 - Sat 21 January 2017
Events (30 results)

Detecting All High-Level Dataraces in an RTOS Kernel.

VMCAI When: Tue 17 Jan 2017 16:30 - 17:00 People: Suvam Mukherjee, Arunkumar S, Deepak D'Souza

… for detecting all high-level dataraces in a system library like the kernel API …

Keynote talk: Varieties of Programming Experience

OBT When: Sat 21 Jan 2017 14:00 - 15:00 People: Alan Blackwell

… in all these styles. This talk therefore takes a “synchronic” approach … to all people and all tasks. All of these languages are primarily intended …

The Curse of Knowledge

PLMW When: Tue 17 Jan 2017 16:30 - 17:00 People: Benjamin C. Pierce

… Writing well is hard for many reasons, but perhaps the hardest of all is what 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. We’ll …

Abductive Reasoning in Deductive Verification

PLMW When: Tue 17 Jan 2017 09:30 - 10:00 People: Işıl Dillig

… and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, and PhD) from …

Interactive data representation migration: Exploiting program dependence to aid program transformation

PEPM 2017 When: Mon 16 Jan 2017 16:30 - 17:00 People: Krishna Narasimhan, Julia Lawall, Christoph Reichenbach

… Data representation migration is a program transformation that involves changing the type of a particular data structure, and then updating all of the operations that somehow depend on that data structure. Changing the data representation …

Structuring Abstract Interpreters through State and Value Abstractions

VMCAI When: Tue 17 Jan 2017 14:30 - 15:00 People: David Bühler, Boris Yakobowski, Sandrine Blazy

… We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all

Matching multiplications in Bit-Vector formulas

VMCAI When: Sun 15 Jan 2017 17:00 - 17:30 People: Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

… to reason about. Therefore, it is important that an SMT solver uses all

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

VMCAI When: Sun 15 Jan 2017 14:00 - 14:30 People: Igor Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi

… . Intuitively, this abstraction should maintain all necessary information …

Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions

VMCAI When: Tue 17 Jan 2017 17:00 - 17:30 People: Raphaël Monat, Antoine Miné

… the variables of all threads using polyhedra, which limits its scalability …

Rigorous Floating-point Mixed Precision Tuning

POPL When: Wed 18 Jan 2017 17:20 - 17:45 People: Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Ian Briggs, Marek S. Baranowski, Alexey Solovyev

… Virtually all real-valued computations are carried out using floating-point … such allocations and conservatively meet a given error target across all program … automatically introduces all the requisite precision up/down casting operations. It also …

Deciding equivalence with sums and the empty type

POPL When: Thu 19 Jan 2017 10:30 - 10:55 People: Gabriel Scherer

… -theoretic equality in all finite models. …

Stream Fusion, to Completeness

POPL When: Wed 18 Jan 2017 16:55 - 17:20 People: Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis

… stream libraries are now available for virtually all modern OO and functional languages, from Java to C# to Scala to OCaml to Haskell. In all past work … generality of stream processing and eliminates all overheads, via the use of staging …

On Verifying Causal Consistency

POPL When: Fri 20 Jan 2017 11:20 - 11:45 People: Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza

… at all sites according to their causal precedence.

We address the problem … and bug finding algorithms, and (2) verifying whether all the executions …

The Lean Theorem Prover

Tutorials When: Mon 16 Jan 2017 09:00 - 12:00Mon 16 Jan 2017 14:00 - 17:00 People: Leonardo de Moura, Gabriel Ebner, Jared Roesch, Sebastian Ullrich

… with a series of examples. Participants will be able to execute and modify all examples … extraction, and an introduction to the tactic framework. Again, all the material …

Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability

POPL When: Thu 19 Jan 2017 11:20 - 11:45 People: Qirun Zhang, Zhendong Su

… the interleaved matched-parenthesis language, but is also closed under all set …) time algorithm for solving all-pairs LCL-reachability, which is asymptotically …

Contextual isomorphisms

POPL When: Thu 19 Jan 2017 11:20 - 11:45 People: Paul Blain Levy

… , to a linear isomorphism. As a corollary, in all these cases, every contextual …

Modules, Abstraction, and Parametric Polymorphism

POPL When: Wed 18 Jan 2017 11:45 - 12:10 People: Karl Crary

… that modules are good for data abstraction. All our proofs are formalized …

Fencing off Go: Liveness and Safety for Channel-Based Programming

POPL When: Fri 20 Jan 2017 15:35 - 16:00 People: Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida

… protection against all too common communication mismatches or partial deadlocks …

The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

POPL When: Fri 20 Jan 2017 16:55 - 17:20 People: Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu

… We introduce a Geometry of Interaction model for higher-order quantum computation, and prove adequacy for a full quantum programming language, in which entanglement, duplication, and recursion are all available. Our model comes …

Do be do be do

POPL When: Thu 19 Jan 2017 14:45 - 15:10 People: Sam Lindley, Conor McBride, Craig McLaughlin

… in Frank employs a novel form of effect polymorphism which avoids all mention of effect …

A Promising Semantics for Relaxed-Memory Concurrency

POPL When: Wed 18 Jan 2017 14:20 - 14:45 People: Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer

… propose the first relaxed memory model that (1) accounts for nearly all

Component-Based Synthesis for Complex APIs

POPL When: Fri 20 Jan 2017 10:30 - 10:55 People: Yu Feng, Ruben Martins, Yuepeng Wang, Işıl Dillig, Thomas Reps

… check and pass all test cases provided by the user.

We have implemented …

Interactive Proofs in Higher-Order Concurrent Separation Logic

POPL When: Wed 18 Jan 2017 15:10 - 15:35 People: Robbert Krebbers, Amin Timany, Lars Birkedal

… for introduction and elimination of all connectives of the object logic, and thereby …

Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins

Tutorials When: Mon 16 Jan 2017 09:00 - 12:00Mon 16 Jan 2017 14:00 - 17:00 People: François Bobot, Loïc Correnson, Boris Yakobowski

… :

  • an over-approximation of the possible values for all the memory locations of the program;
  • all the instructions that might lead to an undefined behavior at runtime …

Contract-based Resource Verification for Higher-order Functions with Memoization

POPL When: Thu 19 Jan 2017 10:55 - 11:20 People: Ravichandhran Madhavan, Sumith Kulal, Viktor Kunčak

… evaluations show that, when averaged over all benchmarks, the actual runtime …

Automatically Comparing Memory Consistency Models

POPL When: Wed 18 Jan 2017 14:45 - 15:10 People: John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides

… , and checking compiler mappings. We show that all four tasks are instances of a general …

Fast Polyhedra Abstract Domain

POPL When: Wed 18 Jan 2017 11:45 - 12:10 People: Gagandeep Singh, Markus Püschel, Martin Vechev

… as significant memory gains, on all larger benchmarks.

As a result, we …

Stochastic Invariants for Probabilistic Termination

POPL When: Wed 18 Jan 2017 15:10 - 15:35 People: Krishnendu Chatterjee, Petr Novotný, Djordje Zikelic


considering all behaviors with no information about the probability …

Stateful Manifest Contracts

POPL When: Thu 19 Jan 2017 15:35 - 16:00 People: Taro Sekiyama, Atsushi Igarashi

… '', that is, we define the manifest contract system so that all contracts are checked at run …

LMS-Verify: Abstraction Without Regret for Verified Systems Programming

POPL When: Fri 20 Jan 2017 16:30 - 16:55 People: Nada Amin, Tiark Rompf

… parsing have been documented in all widely-used web servers. …