Search events for 'all'
The Curse of Knowledge
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 …
SweetPea: A Language for Designing Experiments
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. …
Explaining Type Errors
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 …
A Coq Formalisation of a Core of R
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 …
INVITED TALK: ``Safe'' Languages Require Sequential Consistency
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 …
Hygienic Source-Code Generation Using Functors
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 …
Gradually Typed Symbolic Expressions
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 …
Recursive Programs in Normal Form (Short Paper)
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 …
Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
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 …
Building Secure SGX Enclaves using F*, C/C++ and X64
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 …
Robust Hyperproperty Preservation for Secure Compilation
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 …
Formally Secure Compilation of Unsafe Low-Level Components
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 …
Short talk: Dependently Typed Assembly for Secure Linking
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 …
Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
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 …
Lightning Overview - Day 1
Research Papers When: Wed 10 Jan 2018 09:45 - 10:05
… 1-minute overview of all the talks on Day 1. …
Lightning Overview - Day 3
Research Papers When: Fri 12 Jan 2018 09:30 - 10:00
… 1-minute overview of all the talks on Day 3. …
Lightning Overview - Day 2
Research Papers When: Thu 11 Jan 2018 09:30 - 10:00
… 1-minute overview of all the talks on Day 2. …
Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
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 …
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP 2018 When: Tue 9 Jan 2018 14:00 - 14:30 People: Denis Firsov, Aaron Stump
… products,
primitive heterogeneous equality, and dependent intersections.
All …
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
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 …
Formal Methods For Probabilistic Programming
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. …
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
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 …
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
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 …
More support for symbolic disintegration
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. …
Mechanising and Verifying the WebAssembly Specification
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 …
Proofs in Conflict-Driven Theory Combination
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 …
Mechanising Blockchain Consensus
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 …
Triangulating Context Lemmas
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 …
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
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 …
Online Detection of Effectively Callback Free Objects with Applications to Smart 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 …
Migrating Gradual Types
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 …
Migrating Gradual Types
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 …
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
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. …
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Artifact Evaluation People: Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
… formalized all the technical development and results in Coq. …
Soft Contract Verification for Higher-order Stateful Programs
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 …
Soft Contract Verification for Higher-order Stateful Programs
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 …
Symbolic Types for Lenient Symbolic Execution
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 …
Symbolic Types for Lenient Symbolic Execution
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 …
Simplicitly: Foundations and Applications of Implicit Function Types
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 …
Simplicitly: Foundations and Applications of Implicit Function Types
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 …
A new proof rule for almost-sure termination
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 …
String Constraints with Concatenation and Transducers Solved Efficiently
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 …
String Constraints with Concatenation and Transducers Solved Efficiently
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 …
Programming and Proving with Distributed Protocols
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 …
Programming and Proving with Distributed Protocols
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 …
Introduction to Algebraic Program analysis.
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 …
Code Obfuscation - A Hacking view on program analysis and understanding.
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 …
What's Decidable About String Constraints with ReplaceAll Function?
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 …
WebRelate: Integrating Web Data with Spreadsheets using Examples
Artifact Evaluation People: Jeevana Priya Inala, Rishabh Singh
… the URLs for the webpages containing the desired data for all rows …
WebRelate: Integrating Web Data with Spreadsheets using Examples
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 …
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
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 …
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
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 …
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Artifact Evaluation People: Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis
… demonstrates that the new algorithms significantly outperform all existing methods …
Optimal Dyck Reachability for Data-dependence and Alias Analysis
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 …
Reducing Liveness to Safety in First-Order Logic
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 …
Reducing Liveness to Safety in First-Order Logic
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 …
Collapsing Towers of Interpreters
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 …
A Practical Construction for Decomposing Numerical Abstract Domains
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 …
Collapsing Towers of Interpreters
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 …
A Practical Construction for Decomposing Numerical Abstract Domains
Artifact Evaluation People: Gagandeep Singh, Markus Püschel, Martin Vechev
… domains to benefit from decomposition without re-writing all …
Parametricity versus the Universal Type
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 …
Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can)
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 …