Search events for 'all'
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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. …