Events (40 results)

Gradually Typed Symbolic Expressions

PEPM 2018 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 People: Barry Jay

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

Building Secure SGX Enclaves using F*, C/C++ and X64

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

Formally Secure Compilation of Unsafe Low-Level Components

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

Robust Hyperproperty Preservation for Secure Compilation

PriSC 2018 People: Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Marco Stronati, David Swasey

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

Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs

PriSC 2018 People: Robert Sison

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

A Coq Formalisation of a Core of R

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 …

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 …

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 …

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

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

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

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:23 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

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 …

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 …

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

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 …

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 …

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 …

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 …

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 … of distributed systems and their clients, all within the mechanized …

String Constraints with Concatenation and Transducers Solved Efficiently

Artifact Evaluation People: Lukas Holik, Petr Janku, Anthony Widjaja Lin, Philipp Ruemmer, Tomas 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 …

String Constraints with Concatenation and Transducers Solved Efficiently

Research Papers When: Wed 10 Jan 2018 11:45 - 12:10 People: Lukas Holik, Anthony Widjaja Lin, Petr Janku, Philipp Ruemmer, Tomas Vojnar

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

Collapsing Towers of Interpreters

Artifact Evaluation People: Nada Amin, Tiark Rompf

… Given a tower of interpreters, i.e. a sequence of interpreters interpreting each other, we aim to collapse this tower into a compiler that removes all interpretive overhead in a single pass. We present a multi-level lambda calculus …

Introduction to Algebraic Program analysis.

TutorialFest 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 People: Roberto Giacobazzi

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

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 interpreters interpreting each other, we aim to collapse this tower into a compiler that removes all interpretive overhead in a single pass. We present a multi-level lambda calculus …

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 …

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 …

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 …

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

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 …

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 …

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 …

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 …

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 …

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 …

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 …

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