Latest in cs.pl
total 3605took 0.11s
Migrating large codebases to C++ ModulesJun 12 2019ROOT has several features which interact with libraries and require implicit header inclusion. This can be triggered by reading or writing data on disk, or user actions at the prompt. Often, the headers are immutable, and reparsing is redundant. C++ Modules ... More SAFEVM: A Safety Verifier for Ethereum Smart ContractsJun 12 2019Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use ... More Using Category Theory in Modeling Generics in OOP (Outline)Jun 12 2019Modeling generics in object-oriented programming languages such as Java and C# is a challenge. Recently we proposed a new order-theoretic approach to modeling generics. Given the strong relation between order theory and category theory, in this extended ... More Lifestate: Event-Driven Protocols and Callback Control FlowJun 12 2019Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. ... More SPoC: Search-based Pseudocode to CodeJun 12 2019We consider the task of mapping pseudocode to long programs that are functionally correct. Given test cases as a mechanism to validate programs, we search over the space of possible translations of the pseudocode to find a program that passes the validation. ... More Polymorphic Relaxed NoninterferenceJun 11 2019Information-flow security typing statically preserves confidentiality by enforcing noninterference. To address the practical need of selective and flexible declassification of confidential information, several approaches have developed a notion of relaxed ... More The Prolog debugger and declarative programmingJun 11 2019Logic programming is a declarative programming paradigm. Programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it is incompatible ... More Efficient Graph RewritingJun 11 2019Graph transformation is the rule-based modification of graphs, and is a discipline dating back to the 1970s. The declarative nature of graph rewriting rules comes at a cost. In general, to match the left-hand graph of a fixed rule within a host graph ... More Minimal Session Types (Extended Version)Jun 10 2019Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through ... More Minimal Session Types (Extended Version)Jun 10 2019Jun 12 2019Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through ... More Write, Execute, Assess: Program Synthesis with a REPLJun 09 2019We present a neural program synthesis approach integrating components which write, execute, and assess code to navigate the search space of possible programs. We equip the search process with an interpreter or a read-eval-print-loop (REPL), which immediately ... More Datalog DisassemblyJun 07 2019Jun 12 2019Disassembly is fundamental to binary analysis and rewriting. We present a novel disassembly technique that takes a stripped binary and produces reassembleable assembly code. The resulting assembly code has accurate symbolic information providing cross-references ... More Automatic Reparameterisation of Probabilistic ProgramsJun 07 2019Probabilistic programming has emerged as a powerful paradigm in statistics, applied science, and machine learning: by decoupling modelling from inference, it promises to allow modellers to directly reason about the processes generating data. However, ... More Visual BackpropagationJun 06 2019We show how a declarative functional programming specification of backpropagation yields a visual and transparent implementation within spreadsheets. We call our method Visual Backpropagation. This backpropagation implementation exploits array worksheet ... More Unification-based Pointer Analysis without OversharingJun 04 2019Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyses that are moderately precise while scalable to large real-world programs. ... More Bialgebraic Semantics for String DiagramsJun 04 2019Turi and Plotkin's bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental ... More On Modelling the Avoidability of Patterns as CSPJun 03 2019Solving avoidability problems in the area of string combinatorics often requires, in an initial step, the construction, via a computer program, of a very long word that does not contain any word that matches a given pattern. It is well known that this ... More Reference Capabilities for Safe Parallel Array ProgrammingMay 31 2019The array is a fundamental data structure that provides an efficient way to store and retrieve non-sparse data contiguous in memory. Arrays are important for the performance of many memory-intensive applications due to the design of modern memory hierarchies: ... More A Role for Dependent Types in Haskell (Extended version)May 31 2019Modern Haskell supports zero-cost coercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism of roles to prohibit ... More Differential Equation Invariance AxiomatizationMay 31 2019This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic ... More Sub-Turing Islands in the WildMay 29 2019Recently, there has been growing debate as to whether or not static analysis can be truly sound. In spite of this concern, research on techniques seeking to at least partially answer undecidable questions has a long history. However, little attention ... More Fuzzi: A Three-Level Logic for Differential PrivacyMay 29 2019Curators of sensitive datasets sometimes need to know whether queries against the data are differentially private [Dwork et al. 2006]. Two sorts of logics have been proposed for checking this property: (1) type systems and other static analyses, which ... More Data Race Prediction for Inaccurate TracesMay 26 2019Happens-before based data race prediction methods infer from a trace of events a partial order to check if one event happens before another event. If two two write events are unordered, they are in a race. We observe that common tracing methods provide ... More Programming with Applicative-like expressionsMay 26 2019The fact that Applicative type class allows one to express simple parsers in a variable-less combinatorial style is well appreciated among Haskell programmers for its conceptual simplicity, ease of use, and usefulness for semi-automated code generation ... More Type-Driven Automated Learning with LaleMay 24 2019Machine-learning automation tools, ranging from humble grid-search to hyperopt, auto-sklearn, and TPOT, help explore large search spaces of possible pipelines. Unfortunately, each of these tools has a different syntax for specifying its search space, ... More A Customised App to Attract Female Teenagers to CodingMay 24 2019The number of women in IT-related disciplines is far below the number of men, especially in developed countries. Middle-school girls appear to be engaged in coding courses, but when they choose academic majors relevant to their future careers, only few ... More Hypothetical answers to continuous queries over data streamsMay 23 2019Continuous queries over data streams may suffer from blocking operations and/or unbound wait, which may delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes ... More Java Generics: An Order-Theoretic Approach (Detailed Outline)May 23 2019Generics have been added to Java so as to increase the expressiveness of its type system. Generics in Java, however, include some features---such as Java wildcards, $F$-bounded generics, and Java erasure---that have been hard to analyze and reason about ... More Synthesizing Functional Reactive ProgramsMay 23 2019Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a ... More Set Constraints, Pattern Match Analysis, and SMTMay 23 2019Set constraints provide a highly general way to formulate program analyses. However, solving arbitrary boolean combinations of set constraints is NEXPTIME-complete. Moreover, while theoretical algorithms to solve arbitrary set constraints exist, they ... More Reductions for Automated Hypersafety VerificationMay 22 2019We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation is that constructing a proof for a small representative set of the runs ... More Efficient Synthesis with Probabilistic ConstraintsMay 20 2019We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis (DIGITS), which iteratively calls a synthesizer on finite ... More Towards Neural DecompilationMay 20 2019We address the problem of automatic decompilation, converting a program in low-level representation back to a higher-level human-readable programming language. The problem of decompilation is extremely important for security researchers. Finding vulnerabilities ... More Partial Redundancy Elimination using Lazy Code MotionMay 20 2019Partial Redundancy Elimination (PRE) is a compiler optimization that eliminates expressions that are redundant on some but not necessarily all paths through a program. In this project, we implemented a PRE optimization pass in LLVM and measured results ... More Inferring Inductive Invariants from Phase StructuresMay 19 2019Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive verification is highly expressive but requires the user to annotate the system ... More Property Directed Self CompositionMay 19 2019May 26 2019We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the ... More Property Directed Self CompositionMay 19 2019We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the ... More Developing secure Bitcoin contracts with BitMLMay 18 2019We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain ... More Overfitting in Synthesis: Theory and Practice (Extender Version)May 17 2019May 27 2019In syntax-guided synthesis (SyGuS), a synthesizer's goal is to automatically generate a program belonging to a grammar of possible implementations that meets a logical specification. We investigate a common limitation across state-of-the-art SyGuS tools ... More D2d -- XML for AuthorsMay 17 2019D2d is an input format which allows experienced authors to create type correct xml text objects with minimal disturbance of the creative flow of writing. This paper contains the complete specification of the parsing process, including the generation of ... More Inferring Javascript types using Graph Neural NetworksMay 16 2019The recent use of `Big Code' with state-of-the-art deep learning methods offers promising avenues to ease program source code writing and correction. As a first step towards automatic code repair, we implemented a graph neural network model that predicts ... More First-Class SubtypesMay 16 2019First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in ... More Direct Interpretation of Functional Programs for DebuggingMay 16 2019We make another assault on the longstanding problem of debugging. After exploring why debuggers are not used as widely as one might expect, especially in functional programming environments, we define the characteristics of a debugger which make it usable ... More Extending OCaml's 'open'May 16 2019We propose a harmonious extension of OCaml's 'open' construct. OCaml's existing construct 'open M' imports the names exported by the module 'M' into the current scope. At present 'M' is required to be the path to a module. We propose extending 'open' ... More Towards Comparing Programming ParadigmsMay 15 2019Rapid technological progress in computer sciences finds solutions and at the same time creates ever more complex requirements. Due to an evolving complexity todays programming languages provide powerful frameworks which offer standard solutions for recurring ... More Proceedings ML Family / OCaml Users and Developers workshopsMay 15 2019This volume contains the joint post-proceedings of the 2017 editions of the ML Family Workshop and the OCaml Users and Developers Workshop which took place in Oxford, UK, September 2017, and which were colocated with the ICFP 2017 conference. Proving Unrealizability for Syntax-Guided SynthesisMay 14 2019May 23 2019Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish ... More Proving Unrealizability for Syntax-Guided SynthesisMay 14 2019Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish ... More Automated Parameterized Verification of CRDTsMay 14 2019Maintaining multiple replicas of data is crucial to achieving scalability, availability and low latency in distributed applications. Conflict-free Replicated Data Types (CRDTs) are important building blocks in this domain because they are designed to ... More Generic Encodings of Constructor Rewriting SystemsMay 14 2019Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages, with the negation ... More Learning Scalable and Precise Representation of Program SemanticsMay 13 2019Neural program embedding has shown potential in aiding the analysis of large-scale, complicated software. Newly proposed deep neural architectures pride themselves on learning program semantics rather than superficial syntactic features. However, by considering ... More A true concurrent model of smart contracts executionsMay 10 2019One of the key features of modern blockchain platforms is the possibility of executing smart contracts, i.e. computer programs that transfer digital assets between users, according to pre-agreed rules. Crucially, the execution of smart contracts must ... More A Type Theory for Defining Logics and ProofsMay 07 2019We describe a Martin-L\"of-style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) ... More Parsl: Pervasive Parallel Programming in PythonMay 06 2019High-level programming languages such as Python are increasingly used to provide intuitive interfaces to libraries written in lower-level languages and for assembling applications from various components. This migration towards orchestration rather than ... More Parsl: Pervasive Parallel Programming in PythonMay 06 2019May 18 2019High-level programming languages such as Python are increasingly used to provide intuitive interfaces to libraries written in lower-level languages and for assembling applications from various components. This migration towards orchestration rather than ... More Heaps Don't Lie: Countering Unsoundness with Heap SnapshotsMay 06 2019Static analyses aspire to explore all possible executions in order to achieve soundness. Yet, in practice, they fail to capture common dynamic behavior. Enhancing static analyses with dynamic information is a common pattern, with tools such as Tamiflex. ... More Language-integrated provenance by trace analysisMay 06 2019Language-integrated provenance builds on language-integrated query techniques to make provenance information explaining query results readily available to programmers. In previous work we have explored language-integrated approaches to provenance in Links ... More A Denotational Engineering of Programming LanguagesMay 04 2019The book is devoted to two research areas: (1) Designing programming languages along with their denotational models. A denotational model of a language consists of two many-sorted algebras - an algebra of syntax and an algebra of denotations - and a (unique) ... More An experiment with denotational semanticsMay 04 2019The paper is devoted to showing how to systematically design a programming language in 'reverse order', i.e. from denotations to syntax. This construction is developed in an algebraic framework consisting of three many-sorted algebras: of denotations, ... More Typed-based Relaxed Noninterference for FreeMay 02 2019Jun 11 2019Despite the clear need for specifying and enforcing information flow policies, existing tools and theories either fall short of practical languages, fail to encompass the declassification needed for practical requirements, or fail to provide provable ... More Typed-based Relaxed Noninterference for FreeMay 02 2019Despite the clear need for specifying and enforcing information flow policies, existing tools and theories either fall short of practical languages, fail to encompass the declassification needed for practical requirements, or fail to provide provable ... More Dependence-Aware, Unbounded Sound Predictive Race DetectionApr 30 2019Data races are a real problem for parallel software, yet hard to detect. Sound predictive analysis observes a program execution and detects data races that exist in some other, unobserved execution. However, existing predictive analyses miss races because ... More Dependence-Aware, Unbounded Sound Predictive Race DetectionApr 30 2019May 28 2019Data races are a real problem for parallel software, yet hard to detect. Sound predictive analysis observes a program execution and detects data races that exist in some other, unobserved execution. However, existing predictive analyses miss races because ... More Targeted Synthesis for Programming with Data InvariantsApr 30 2019Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult because the ... More A Framework for Debugging Java Programs in a BytecodeApr 29 2019In the domain of Software Engineering, program analysis and understanding has been considered to be a very challenging task since decade, as it demands dedicated time and efforts. The analysis of source code may occasionally be comparatively easier due ... More A Practical Analysis of Rust's Concurrency StoryApr 27 2019Correct concurrent programs are difficult to write; when multiple threads mutate shared data, they may lose writes, corrupt data, or produce erratic program behavior. While many of the data-race issues with concurrency can be avoided by the placing of ... More