Latest in cs.pl

total 3605took 0.11s
Modeling and Verifying Cyber-Physical Systems with Hybrid Active ObjectsJun 13 2019Formal modeling of cyber-physical systems (CPS) is hard, because they pose the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal specification and verification languages for CPS are designed on top of their ... More
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
Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version)Jun 12 2019Jun 13 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
Assessing Performance Implications of Deep Copy Operations via MicrobenchmarkingJun 03 2019Jun 11 2019As scientific frameworks become sophisticated, so do their data structures. Current data structures are no longer simple in design and they have been progressively complicated. The typical trend in designing data structures in scientific applications ... More
Assessing Performance Implications of Deep Copy Operations via MicrobenchmarkingJun 03 2019As scientific frameworks become sophisticated, so do their data structures. Current data structures are no longer simple in design and they have been progressively complicated. The typical trend in designing data structures in scientific applications ... More
A scheme for dynamically integrating C library functions into a $λ$Prolog implementationJun 03 2019The Teyjus system realizes the higher-order logic programming language$\lambda$Prolog by compiling programs into bytecode for an abstract machine and executing this translated form using a simulator for the machine. Teyjus supports a number of builtin ... 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
A Survey of Asynchronous Programming Using Coroutines in the Internet of Things and Embedded SystemsJun 02 2019Many Internet of Things and embedded projects are event-driven, and therefore require asynchronous and concurrent programming. Current proposals for C++20 suggest that coroutines will have native language support. It is timely to survey the current use ... More
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress)May 31 2019We present "interaction trees" (ITrees), a general-purpose data structure in Coq for formalizing the behaviors of recursive programs that interact with their environment. ITrees are built of uninterpreted events and their continuations---a coinductive ... 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
On the Interaction of Object-Oriented Design Patterns and Programming LanguagesMay 31 2019Design patterns are distilled from many real systems to catalog common programming practice. However, some object-oriented design patterns are distorted or overly complicated because of the lack of supporting programming language constructs or mechanisms. ... 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
Understanding and Extending Incremental Determinization for 2QBFMay 31 2019Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determinization as a set of inference rules to help understand the design space ... More
How Often Do Single-Statement Bugs Occur? The ManySStuBs4J DatasetMay 30 2019Program repair is an important but difficult software engineering problem. One way to achieve a "sweet spot" of low false positive rates, while maintaining high enough recall to be usable, is to focus on repairing classes of simple bugs, such as bugs ... 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
Categorization of Program Regions for Agile Compilation using Machine Learning and Hardware SupportMay 29 2019A compiler processes the code written in a high level language and produces machine executable code. The compiler writers often face the challenge of keeping the compilation times reasonable. That is because aggressive optimization passes which potentially ... More
An Experiment with a User Manual of a Programming Language Based on a Denotational SemanticsMay 28 2019Denotational models should provide an opportunity for the revision of current practices seen in the manuals of programming languages. New styles should on one hand base on denotational models but on the other - do not assume that today readers are acquainted ... 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
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)May 24 2019We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines ... 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
A Quick Introduction to Functional Verification of Array-Intensive ProgramsMay 22 2019Array-intensive programs are often amenable to parallelization across many cores on a single machine as well as scaling across multiple machines and hence are well explored, especially in the domain of high-performance computing. These programs typically ... More
Verification Artifacts in Cooperative Verification: Survey and Unifying Component FrameworkMay 21 2019The goal of cooperative verification is to combine verification approaches in such a way that they work together to verify a system model. In particular, cooperative verifiers provide exchangeable information (verification artifacts) to other verifiers ... 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
Statistical Assertions for Validating Patterns and Finding Bugs in Quantum ProgramsMay 20 2019In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have ... 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
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable LogicsMay 19 2019Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only ... 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
Safe and Chaotic Compilation for Hidden Deterministic Hardware AliasingMay 19 2019Hardware aliasing occurs when the same logical address can access different physical memory locations. This is a problem for software on some embedded systems and more generally when hardware becomes faulty in irretrievable locations, such as on a Mars ... More
A Case Study: Exploiting Neural Machine Translation to Translate CUDA to OpenCLMay 18 2019The sequence-to-sequence (seq2seq) model for neural machine translation has significantly improved the accuracy of language translation. There have been new efforts to use this seq2seq model for program language translation or program comparisons. In ... 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
Simple and Effective Relation-Based Approaches To XPath and XSLT Type Checking (Technical Report, Bad Honnef 2015)May 17 2019XPath is a language for addressing parts of an XML document. We give an abstract interpretation of XPath expressions in terms of relations on document node types. Node-set-related XPath language constructs are mapped straightforwardly onto basic, well-understood ... 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
Implementing a Library for Probabilistic Programming using Non-strict Non-determinismMay 17 2019This paper presents PFLP, a library for probabilistic programming in the functional logic programming language Curry. It demonstrates how the concepts of a functional logic programming language support the implementation of a library for probabilistic ... 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
Effects Without Monads: Non-determinism -- Back to the Meta LanguageMay 16 2019We reflect on programming with complicated effects, recalling an undeservingly forgotten alternative to monadic programming and checking to see how well it can actually work in modern functional languages. We adopt and argue the position of factoring ... 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
Loop Summarization with Rational Vector Addition Systems (extended version)May 16 2019This paper presents a technique for computing numerical loop summaries. The method works first synthesizing a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then using the (polytime computable) reachability ... 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
Software System Design based on Patterns for Newton-Type MethodsMay 12 2019A wide range of engineering applications uses optimisation techniques as part of their solution process. The researcher uses specialized software that implements well-known optimisation techniques to solve his problem. However, when it comes to develop ... 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
Automatic Programming of Cellular Automata and Artificial Neural Networks Guided by PhilosophyMay 10 2019Many computer models such as cellular automata have been developed and successfully applied. However, in some cases these models might be restrictive on the possible solutions or their solution is difficult to interpret. To overcome this problem, we outline ... More
Dynamic Verification with Observational Equivalence of C/C++ ConcurrencyMay 10 2019Program executions under relaxed memory model (rmm) semantics are significantly more difficult to analyze; the rmm semantics result in out of order execution of program events leading to an explosion of state-space. Dynamic partial order reduction (DPOR) ... More
Research Note: An Open Source Bluespec CompilerMay 08 2019In this Research Note we report on an open-source compiler for the Bluespec hardware description language.
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
Programming Unikernels in the Large via Functor Driven DevelopmentMay 07 2019Compiling applications as unikernels allows them to be tailored to diverse execution environments. Dependency on a monolithic operating system is replaced with linkage against libraries that provide specific services. Doing so in practice has revealed ... 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
A Semi-Automatic Approach for Syntax Error Reporting and Recovery in Parsing Expression GrammarsMay 06 2019Error recovery is an essential feature for a parser that should be plugged in Integrated Development Environments (IDEs), which must build Abstract Syntax Trees (ASTs) even for syntactically invalid programs in order to offer features such as automated ... 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
TryLinks: An interactive tutorial system for a cross-tier Web programming languageMay 06 2019Links is a web programming language under development in Edinburgh aimed at simplifying web development. Conventional multi-tier applications involve programming in several languages for different layers, and the mismatches between these layers and abstractions ... More
SIF: A Framework for Solidity Code Instrumentation and AnalysisMay 05 2019Solidity is an object-oriented and high-level language for writing smart contracts which are used to execute, verify and enforce credible transactions on permissionless blockchains. In the last few years, analysis of vulnerabilities in smart contracts ... 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
A Type System for First-Class Layers with Inheritance, Subtyping, and SwappingMay 04 2019Context-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers---modules to describe context-dependent behavioral variations of a software system---and their dynamic ... 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
Next-Paradigm Programming Languages: What Will They Look Like and What Changes Will They Bring?May 01 2019The dream of programming language design is to bring about orders-of-magnitude productivity improvements in software development tasks. Designers can endlessly debate on how this dream can be realized and on how close we are to its realization. Instead, ... More
Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)Apr 30 2019We present Behavioral Program Logic (BPL), a dynamic logic for trace properties that incorporates concepts from behavioral types and allows reasoning about non-functional properties within a sequent calculus. BPL uses behavioral modalities [s |- {\tau} ... 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