Latest in

total 2596took 0.12s
Optimizing and Evaluating Transient Gradual TypingFeb 20 2019Gradual typing enables programmers to combine static and dynamic typing in the same language. However, ensuring a sound interaction between the static and dynamic parts can incur significant runtime cost. In this paper, we perform a detailed performance ... More
A Dependently Typed Library for Static Information-Flow Control in IdrisFeb 18 2019Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through ... More
Compiled Obfuscation for Data Structures in Encrypted ComputingFeb 16 2019Encrypted computing is an emerging technology based on a processor that `works encrypted', taking encrypted inputs to encrypted outputs while data remains in encrypted form throughout. It aims to secure user data against possible insider attacks by the ... More
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-CalculusFeb 16 2019We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms ... More
Resource-Aware Session Types for Digital ContractsFeb 16 2019Programming digital contracts comes with unique challenges, which include describing and enforcing protocols of interaction, controlling resource usage, and tracking linear assets. This article presents the type-theoretic foundation of Nomos, a programming ... More
Robustness of Neural Networks: A Probabilistic and Practical ApproachFeb 15 2019Neural networks are becoming increasingly prevalent in software, and it is therefore important to be able to verify their behavior. Because verifying the correctness of neural networks is extremely challenging, it is common to focus on the verification ... More
Types by Need (Extended Version)Feb 15 2019A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the ... More
A static higher-order dependency pair frameworkFeb 15 2019We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, ... More
Formal Foundations of Serverless ComputingFeb 15 2019Feb 18 2019A robust, large-scale web service can be difficult to engineer. When demand spikes, it must configure new machines and manage load-balancing; when demand falls, it must shut down idle machines to reduce costs; and when a machine crashes, it must quickly ... More
Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL (Extended Version)Feb 14 2019Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its variants simultaneously in a single run by exploiting the similarities ... More
We should Stop Claiming Generality in our Domain-Specific Language PapersFeb 14 2019Our community believes that new domain-specific languages should be as general as possible to increase their impact. However, I argue in this essay that we should stop claiming generality for new domain-specific languages. More general domain-specific ... More
Redundant Loads: A Software Inefficiency IndicatorFeb 14 2019Modern software packages have become increasingly complex with millions of lines of code and references to many external libraries. Redundant operations are a common performance limiter in these code bases. Missed compiler optimization opportunities, ... More
Checking Observational Purity of ProceduresFeb 14 2019Verifying whether a procedure is observationally pure is useful in many software engineering scenarios. An observationally pure procedure always returns the same value for the same argument, and thus mimics a mathematical function. The problem is challenging ... More
Introducing Yet Another REversible LanguageFeb 14 2019Yarel is a core reversible programming language that implements a class of permutations, defined recursively, which are primitive recursive complete. The current release of Yarel syntax and operational semantics, implemented by compiling Yarel to Java, ... More
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and DetailsFeb 14 2019We propose a calling convention for capability machines with local capabilities. The calling convention ensures local-state encapsulation and well-bracketed control flow. We use the calling convention in a hand-full of program examples and prove that ... More
HyPLC: Hybrid Programmable Logic Controller Program Translation for VerificationFeb 14 2019Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such ... More
Spectre is here to stay: An analysis of side-channels and speculative executionFeb 14 2019The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages. This paper explores speculative side-channel attacks and their implications for programming ... More
Differentials and distances in probabilistic coherence spacesFeb 13 2019In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute ... More
Proving Expected Sensitivity of Probabilistic Programs with Randomized Execution TimeFeb 13 2019The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. Previous ... More
Mesh: Compacting Memory Management for C/C++ ApplicationsFeb 13 2019Programs written in C/C++ can suffer from serious memory fragmentation, leading to low utilization of memory, degraded performance, and application failure due to memory exhaustion. This paper introduces Mesh, a plug-in replacement for malloc that, for ... More
Mesh: Compacting Memory Management for C/C++ ApplicationsFeb 13 2019Feb 16 2019Programs written in C/C++ can suffer from serious memory fragmentation, leading to low utilization of memory, degraded performance, and application failure due to memory exhaustion. This paper introduces Mesh, a plug-in replacement for malloc that, for ... More
Cost Analysis of Nondeterministic Probabilistic ProgramsFeb 12 2019We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. Previous approaches for this problem could only handle nonnegative bounded ... More
Program Equivalence for Algebraic Effects via ModalitiesFeb 12 2019This dissertation is concerned with the study of program equivalence and algebraic effects as they arise in the theory of programming languages. Algebraic effects represent impure behaviour in a functional programming language, such as input and output, ... More
Polynomial Invariant Generation for Non-deterministic Recursive ProgramsFeb 12 2019We present a sound and complete method to generate inductive invariants consisting of polynomial inequalities for programs with polynomial updates. Our method is based on Positivstellensaetze and an algorithm of Grigor'ev and Vorobjov for solving systems ... More
Revec: Program Rejuvenation through RevectorizationFeb 07 2019Modern microprocessors are equipped with Single Instruction Multiple Data (SIMD) or vector instructions which expose data level parallelism at a fine granularity. Programmers exploit this parallelism by using low-level vector intrinsics in their code. ... More
On Quasi Ordinal Diagram SystemsFeb 06 2019The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we discuss possible ... More
Fearless Concurrency? Understanding Concurrent Programming Safety in Real-World Rust SoftwareFeb 05 2019Rust is a popular programming language in building various low-level software in recent years. It aims to provide safe concurrency when implementing multi-threaded software through a suite of compiler checking rules. Unfortunately, there is limited understanding ... More
Event Loops as First-Class Values: A Case Study in Pedagogic Language DesignFeb 02 2019The World model is an existing functional input-output mechanism for event-driven programming. It is used in numerous popular textbooks and curricular settings. The World model conflates two different tasks -- the definition of an event processor and ... More
Fine-Grain Checkpointing with In-Cache-Line LoggingFeb 02 2019Non-Volatile Memory offers the possibility of implementing high-performance, durable data structures. However, achieving performance comparable to well-designed data structures in non-persistent (transient) memory is difficult, primarily because of the ... More
Separating Use and Reuse to Improve BothFeb 01 2019Context: Trait composition has inspired new research in the area of code reuse for object oriented (OO) languages. One of the main advantages of this kind of composition is that it makes possible to separate subtyping from subclassing; which is good for ... More
ParaSail: A Pointer-Free Pervasively-Parallel Language for Irregular ComputationsFeb 01 2019ParaSail is a language specifically designed to simplify the construction of programs that make full, safe use of parallel hardware even while manipulating potentially irregular data structures. As parallel hardware has proliferated, there has been an ... More
Distributed Reactive Programming for Reactive Distributed SystemsFeb 01 2019Context: The term reactivity is popular in two areas of research: programming languages and distributed systems. On one hand, reactive programming is a paradigm which provides programmers with the means to declaratively write event-driven applications. ... More
ExceLint: Automatically Finding Spreadsheet Formula ErrorsJan 30 2019Spreadsheets are one of the most widely used programming environments, and are widely deployed in domains like finance where errors can have catastrophic consequences. We present a static analysis specifically designed to find spreadsheet formula errors. ... More
Noise-Adaptive Compiler Mappings for Noisy Intermediate-Scale Quantum ComputersJan 30 2019A massive gap exists between current quantum computing (QC) prototypes, and the size and scale required for many proposed QC algorithms. Current QC implementations are prone to noise and variability which affect their reliability, and yet with less than ... More
Egyptian multiplication and some of its ramificationsJan 30 2019Fast exponentiation with an integer exponent relies on squaring of the base being compensated by halving the exponent when even. Likewise one can raise to a fractional power where doubling the exponent is compensated by taking the square root of the base. ... More
Abstract I/O SpecificationJan 29 2019We recently proposed an approach for the specification and modular formal verification of the interactive (I/O) behavior of programs, based on an embedding of Petri nets into separation logic. While this approach is scalable and modular in terms of the ... More
Verifying Asynchronous Interactions via Communicating Session AutomataJan 28 2019The relationship between communicating automata and session types is the cornerstone of many diverse theories and tools, including type checking, code generation, and runtime verification. A serious limitation of session types is that, while endpoint ... More
Program algebra for Turing-machine programsJan 25 2019This note presents an algebraic theory of instruction sequences with instructions for Turing tapes as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and the ... More
The Size-Change Principle for Mixed Inductive and Coinductive typesJan 23 2019This paper describes how to use Lee, Jones and Ben Amram's size-change principle to check correctness of arbitrary recursive definitions in an ML / Haskell like programming language. The main point is that the size-change principle isn't only used to ... More
Kantorovich Continuity of Probabilistic ProgramsJan 19 2019The Kantorovich metric is a canonical lifting of a distance from sets to distributions over this set. The metric also arises naturally when proving continuity properties of probabilistic programs. For instance, algorithmic stability of machine learning ... More
Static Analysis for Asynchronous JavaScript ProgramsJan 11 2019Asynchrony has become an inherent element of JavaScript, as an effort to improve the scalability and performance of modern web applications. To this end, JavaScript provides programmers with a wide range of constructs and features for developing code ... More
Keeping CALM: When Distributed Consistency is EasyJan 07 2019Jan 26 2019A key concern in modern distributed systems is to avoid the cost of coordination while maintaining consistent semantics. Until recently, there was no answer to the question of when coordination is actually required. In this paper we present an informal ... More
Sundials/ML: Connecting OCaml to the Sundials Numeric SolversDec 31 2018This paper describes the design and implementation of a comprehensive OCaml interface to the Sundials library of numeric solvers for ordinary differential equations, differential algebraic equations, and non-linear equations. The interface provides a ... More
Correct by constructionDec 21 2018Matrix code allows one to discover algorithms and to render them in code that is both compilable and is correct by construction. In this way the difficulty of verifying existing code is avoided. The method is especially important for logically dense code ... More
Whittemore: An embedded domain specific language for causal programmingDec 21 2018This paper introduces Whittemore, a language for causal programming. Causal programming is based on the theory of structural causal models and consists of two primary operations: identification, which finds formulas that compute causal queries, and estimation, ... More
Property-based testing for Spark StreamingDec 20 2018Stream processing has reached the mainstream in the last years, as a new generation of open source distributed stream processing systems, designed for scaling horizontally on commodity hardware, has brought the capability for processing high volume and ... More
Automatic Alignment of Sequential Monte Carlo Inference in Higher-Order Probabilistic ProgramsDec 18 2018Probabilistic programming is a programming paradigm for expressing flexible probabilistic models. Implementations of probabilistic programming languages employ a variety of inference algorithms, where sequential Monte Carlo methods are commonly used. ... More
In Praise of Sequence (Co-)Algebra and its implementation in HaskellDec 14 2018What is Sequence Algebra? This is a question that any teacher or student of mathematics or computer science can engage with. Sequences are in Calculus, Combinatorics, Statistics and Computation. They are foundational, a step up from number arithmetic. ... More
CSS Minification via Constraint Solving (Technical Report)Dec 07 2018Minification is a widely-accepted technique which aims at reducing the size of the code transmitted over the web. We study the problem of minifying Cascading Style Sheets (CSS) --- the de facto language for styling web documents. Traditionally, CSS minifiers ... More
JANUS: Fast and Flexible Deep Learning via Symbolic Graph Execution of Imperative ProgramsDec 04 2018The rapid evolution of deep neural networks is demanding deep learning (DL) frameworks not only to satisfy the traditional requirement of quickly executing large computations, but also to support straightforward programming models for quickly implementing ... More
Ann: A domain-specific language for the effective design and validation of Java annotationsDec 02 2018This paper describes a new modelling language for the effective design and validation of Java annotations. Since their inclusion in the 5th edition of Java, annotations have grown from a useful tool for the addition of meta-data to play a central role ... More
Exploiting Pointer Analysis in Memory Models for Deductive VerificationNov 29 2018Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer analysis ... More
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked ServerNov 29 2018We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) ... More
Adventures in Formalisation: Financial Contracts, Modules, and Two-Level Type TheoryNov 28 2018We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language for financial ... More
Experience Report on Formally Verifying Parts of OpenJDK's API with KeYNov 27 2018Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, however, to develop verification tools aiding industrial software developers ... More
Sound Approximation of Programs with Elementary FunctionsNov 26 2018Elementary function calls are a common feature in numerical programs. While their implementions in library functions are highly optimized, their computation is nonetheless very expensive compared to plain arithmetic. Full accuracy is, however, not always ... More
GASTAP: A Gas Analyzer for Smart ContractsNov 22 2018Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption ... More
Effect Handling for Composable Program Transformations in Edward2Nov 15 2018Algebraic effects and handlers have emerged in the programming languages community as a convenient, modular abstraction for controlling computational effects. They have found several applications including concurrent programming, meta programming, and ... More
Newton: A Language for Describing PhysicsNov 12 2018This article introduces Newton, a specification language for notating the analytic form, units of measure, and sensor signal properties for physical-object-specific invariants and general physical laws. We designed Newton to provide a means for hardware ... More
A Program Logic for First-Order Encapsulated WebAssemblyNov 08 2018WebAssembly (Wasm) is the first new programming language in over 20 years to be natively supported on the web. A small-step semantics of Wasm was formally introduced by Haas et al. 2017 and mechanised in Isabelle by Watt 2018. In this report, we introduce ... More
On the extreme power of nonstandard programming languagesNov 07 2018Nov 18 2018Suenaga and Hasuo introduced a nonstandard programming language ${\bf While}^{{\bf dt}}$ which models hybrid systems. We demonstrate why ${\bf While}^{{\bf dt}}$ is not suitable for modeling actual computations.
GPU Acceleration of an Established Solar MHD Code using OpenACCNov 06 2018GPU accelerators have had a notable impact on high-performance computing across many disciplines. They provide high performance with low cost/power, and therefore have become a primary compute resource on many of the largest supercomputers. Here, we implement ... More
Gradual Type Theory (Extended Version)Nov 06 2018Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning ... More
Fast and exact analysis for LRU cachesNov 05 2018Dec 20 2018For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently ... More
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and DeterministicNov 02 2018Stan is a probabilistic programming language that has been increasingly used for real-world scalable projects. However, to make practical inference possible, the language sacrifices some of its usability by adopting a block syntax, which lacks compositionality ... More
Making root cause analysis feasible for large code bases: a solution approach for a climate modelOct 31 2018Feb 11 2019For large-scale simulation codes with huge and complex code bases, where bit-for-bit comparisons are too restrictive, finding the source of statistically significant discrepancies (e.g., from a previous version, alternative hardware or supporting software ... More
Synthesizing Symmetric LensesOct 26 2018Lenses are programs that can be run both "front to back" and "back to front," allowing data and updates to be transformed in two directions. Since their introduction, lenses have been extensively studied and applied. Recent work has also demonstrated ... More
AutoParallel: A Python module for automatic parallelization and distributed execution of affine loop nestsOct 26 2018The last improvements in programming languages, programming models, and frameworks have focused on abstracting the users from many programming issues. Among others, recent programming frameworks include simpler syntax, automatic memory management and ... More
All-Path Reachability LogicOct 25 2018This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path ... More
Decoupling Lock-Free Data Structures from Memory Reclamation for Static AnalysisOct 25 2018Nov 09 2018Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously ... More
Pyro: Deep Universal Probabilistic ProgrammingOct 18 2018Pyro is a probabilistic programming language built on Python as a platform for developing advanced probabilistic models in AI research. To scale to large datasets and high-dimensional models, Pyro uses stochastic variational inference algorithms and probability ... More
Asynchronous Execution of Python Code on Task Based Runtime SystemsOct 17 2018Oct 22 2018Despite advancements in the areas of parallel and distributed computing, the complexity of programming on High Performance Computing (HPC) resources has deterred many domain experts, especially in the areas of machine learning and artificial intelligence ... More
AutoGraph: Imperative-style Coding with Graph-based PerformanceOct 16 2018There is a perceived trade-off between machine learning code that is easy to write, and machine learning code that is scalable or fast to execute. In machine learning, imperative style libraries like Autograd and PyTorch are easy to write, but suffer ... More
Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScriptOct 10 2018Dec 11 2018Existing support for regular expressions in automated test generation or verification tools is lacking. Common aspects of regular expression engines found in mainstream programming languages, such as backreferences or greedy matching, are commonly ignored ... More
Deriving sorting algorithms via abductive logic program transformationOct 04 2018Logic program transformation by the unfold/fold method ad- vocates the writing of correct logic programs via the application of some rules to a naive program. This work focuses on how to overcome subgoal- introduction difficulties in synthesizing efficient ... More
Pre-proceedings of the 26th International Workshop on Functional and Logic Programming (WFLP 2018)Oct 01 2018This volume constitutes the pre-proceedings of the 26th International Workshop on Functional and Logic Programming (WFLP 2018). It is formed of those papers selected by the program committee for presentation at the workshop. After discussion at the workshop, ... More
Relay: A New IR for Machine Learning FrameworksSep 26 2018Machine learning powers diverse services in industry including search, translation, recommendation systems, and security. The scale and importance of these models require that they be efficient, expressive, and portable across an array of heterogeneous ... More
Scenic: Language-Based Scene GenerationSep 25 2018Synthetic data has proved increasingly useful in both training and testing machine learning models such as neural networks. The major problem in synthetic data generation is producing meaningful data that is not simply random but reflects properties of ... More
Exploiting Errors for Efficiency: A Survey from Circuits to AlgorithmsSep 16 2018When a computational task tolerates a relaxation of its specification or when an algorithm tolerates the effects of noise in its execution, hardware, programming languages, and system software can trade deviations from correct behavior for lower resource ... More
Description, Implementation, and Evaluation of a Generic Design for Tabled CLPSep 15 2018Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and in some cases more efficient than LP, CLP or LP + tabling. Previous designs of TCLP systems did not fully use entailment ... More
Bounded Symbolic Execution for Runtime Error Detection of Erlang ProgramsSep 13 2018Dynamically typed languages, like Erlang, allow developers to quickly write programs without explicitly providing any type information on expressions or function definitions. However, this feature makes those languages less reliable than statically typed ... More
Faster Variational Execution with Transparent Bytecode TransformationSep 11 2018Variational execution is a novel dynamic analysis technique for exploring highly configurable systems and accurately tracking information flow. It is able to efficiently analyze many configurations by aggressively sharing redundancies of program executions. ... More
TeSSLa: Temporal Stream-based Specification LanguageAug 31 2018Runtime verification is concerned with monitoring program traces. In particular, stream runtime verification (SRV) takes the program trace as input streams and incrementally derives output streams. SRV can check logical properties and compute temporal ... More
When You Should Use Lists in Haskell (Mostly, You Should Not)Aug 24 2018We comment on the over-use of lists in functional programming. With this respect, we review history of Haskell and some of its libraries, and hint at current developments.
Transpiling Programmable Computable Functions to Answer Set ProgramsAug 23 2018Programming Computable Functions (PCF) is a simplified programming language which provides the theoretical basis of modern functional programming languages. Answer set programming (ASP) is a programming paradigm focused on solving search problems. In ... More
Measuring Coverage of Prolog Programs Using Mutation TestingAug 23 2018Testing is an important aspect in professional software development, both to avoid and identify bugs as well as to increase maintainability. However, increasing the number of tests beyond a reasonable amount hinders development progress. To decide on ... More
Rock bottom, the world, the sky: Catrobat, an extremely large-scale and long-term visual coding project relying purely on smartphonesAug 20 2018Most of the 700 million teenagers everywhere in the world already have their own smartphones, but comparatively few of them have access to PCs, laptops, OLPCs, Chromebooks, or tablets. The free open source non-profit project Catrobat allows users to create ... More
Compiling Control as Offline Partial DeductionAug 16 2018Nov 30 2018We present a new approach to a technique known as compiling control, whose aim is to compile away special mechanisms for non-standard atom selection in logic programs. It has previously been conjectured that compiling control could be implemented as an ... More
Multivariant Assertion-based Guidance in Abstract InterpretationAug 15 2018Dec 17 2018Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always producing useful results. Automatic techniques have been studied to prevent ... More
Homeomorphic Embedding modulo Combinations of Associativity and Commutativity AxiomsAug 15 2018Nov 28 2018The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted ... More
Multiparty Classical ChoreographiesAug 15 2018Dec 02 2018We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that ... More
A prototype-based approach to object reclassificationAug 13 2018We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by Cardelli as a self-inflicted operation. We present a sound type system ... More
CT-Wasm: Type-Driven Secure Cryptography for the Web EcosystemAug 03 2018Dec 17 2018A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ... More
Sparse Matrix Code Dependence Analysis Simplification at Compile TimeJul 27 2018Analyzing array-based computations to determine data dependences is useful for many applications including automatic parallelization, race detection, computation and communication overlap, verification, and shape analysis. For sparse matrix codes, array ... More
Exploratory and Live, Programming and Coding: A Literature Study Comparing Perspectives on LivenessJul 23 2018Various programming tools, languages, and environments give programmers the impression of changing a program while it is running. This experience of liveness has been discussed for over two decades and a broad spectrum of research on this topic exists. ... More
Specification Mining for Smart Contracts with Automatic Abstraction TuningJul 20 2018Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and ... More
Overcoming Language Dichotomies: Toward Effective Program Comprehension for Mobile App DevelopmentJul 18 2018Mobile devices and platforms have become an established target for modern software developers due to performant hardware and a large and growing user base numbering in the billions. Despite their popularity, the software development process for mobile ... More
Genetic algorithms in ForthJul 17 2018A method for automatically finding a program (bytecode) realizing the given algorithm is developed. The algorithm is specified as a set of tests (input\_data) $ \rightarrow $ (output\_data). Genetic methods made it possible to find the implementation ... More
Competitive Parallelism: Getting Your Priorities RightJul 10 2018Multi-threaded programs have traditionally fallen into one of two domains: cooperative and competitive. These two domains have traditionally remained mostly disjoint, with cooperative threading used for increasing throughput in compute-intensive applications ... More
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing LeaksJul 09 2018The timing characteristics of cache, a high-speed storage between the fast CPU and the slowmemory, may reveal sensitive information of a program, thus allowing an adversary to conduct side-channel attacks. Existing methods for detecting timing leaks either ... More