Latest in cs.pl

total 3336took 0.17s
Compiling for Encrypted Computing: Obfuscation but Not in NameApr 20 2019Encrypted computing is the emerging science and technology of processors that take encrypted inputs to encrypted outputs via encrypted intermediates (at nearly conventional speeds). The aim is to make user data in general-purpose computing secure against ... More
Optimizing Quantum Programs against Decoherence: Delaying Qubits into Quantum SuperpositionApr 18 2019Quantum computing technology has reached a second renaissance in the last decade. However, in the NISQ era pointed out by John Preskill in 2018, quantum noise and decoherence, which affect the accuracy and execution effect of quantum programs, cannot ... More
Quantitative Expressiveness of Instruction Sequence Classes for Computation on Single Bit RegistersApr 18 2019The number of instructions of an instruction sequence is taken for its logical SLOC, and is abbreviated with LLOC. A notion of quantitative expressiveness is based on LLOC and in the special case of operation over a family of single bit registers a collection ... More
ClangJIT: Enhancing C++ with Just-in-Time CompilationApr 18 2019The C++ programming language is not only a keystone of the high-performance-computing ecosystem but has proven to be a successful base for portable parallel-programming frameworks. As is well known, C++ programmers use templates to specialize algorithms, ... More
Low-Latency Graph Streaming Using Compressed Purely-Functional TreesApr 17 2019Due to the dynamic nature of real-world graphs, there has been a growing interest in the graph-streaming setting where a continuous stream of graph updates is mixed with arbitrary graph queries. In principle, purely-functional trees are an ideal choice ... More
Relay: A High-Level IR for Deep LearningApr 17 2019Frameworks for writing, compiling, and optimizing deep learning (DL) models have recently enabled progress in areas like computer vision and natural language processing. Extending these frameworks to accommodate the rapidly diversifying landscape of DL ... More
On Resolving Non-determinism in ChoreographiesApr 17 2019Choreographies specify multiparty interactions via message passing. A \emph{realization} of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies ... More
Scalable Verification of Probabilistic NetworksApr 17 2019This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This ... More
A 2-Categorical Study of Graded and Indexed MonadsApr 17 2019In the study of computational effects, it is important to consider the notion of computational effects with parameters. The need of such a notion arises when, for example, statically estimating the range of effects caused by a program, or studying the ... More
Using Dynamic Analysis to Generate Disjunctive InvariantsApr 16 2019Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. ... More
The Geometry of Bayesian ProgrammingApr 16 2019We give a geometry of interaction model for a typed lambda-calculus endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The model is based ... More
Resource-Guided Program SynthesisApr 16 2019Apr 18 2019This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines ... More
Resource-Guided Program SynthesisApr 16 2019This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines ... More
swTVM: Exploring the Automated Compilation for Deep Learning on Sunway ArchitectureApr 16 2019Apr 18 2019The flourish of deep learning frameworks and hardware platforms has been demanding an efficient compiler that can shield the diversity in both software and hardware in order to provide application portability. Among the exiting deep learning compilers, ... More
swTVM: Exploring the Automated Compilation for Deep Learning on Sunway ArchitectureApr 16 2019The flourish of deep learning frameworks and hardware platforms has been demanding an efficient compiler that can shield the diversity in both software and hardware in order to provide application portability. Among the exiting deep learning compilers, ... More
A Path To DOT: Formalizing Fully-Path-Dependent TypesApr 15 2019The Dependent Object Types (DOT) calculus aims to formalize the Scala programming language with a focus on path-dependent types $-$ types such as $x.a_1\dots a_n.T$ that depend on the runtime value of a path $x.a_1\dots a_n$ to an object. Unfortunately, ... More
Specifying Concurrent Programs in Separation Logic: Morphisms and SimulationsApr 15 2019In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources - a form of state transition systems - to describe the state-based program invariants that must ... More
Taking Linear Logic ApartApr 15 2019Process calculi based on logic, such as $\pi$DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the $\pi$-calculus: ... More
On the Lambek Calculus with an Exchange ModalityApr 15 2019In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should view this logic ... More
From Linear Logic to Cyclic SharingApr 15 2019We present a translation from Multiplicative Exponential Linear Logic to a simply-typed lambda calculus with cyclic sharing. This translation is derived from a simple observation on the Int-construction on traced monoidal categories. It turns out that ... More
The Bang Calculus and the Two Girard's TranslationsApr 15 2019We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to ... More
From Theory to Systems: A Grounded Approach to Programming Language EducationApr 14 2019I present a new approach to teaching a graduate-level programming languages course focused on using systems programming ideas and languages like WebAssembly and Rust to motivate PL theory. Drawing on students' prior experience with low-level languages, ... More
Got: Git, but for ObjectsApr 13 2019We look at one important category of distributed applications characterized by the existence of multiple collaborating, and competing, components sharing mutable, long-lived, replicated objects. The problem addressed by our work is that of object state ... More
Flint for Safer Smart ContractsApr 13 2019The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the platform; however, they have been subject to numerous attacks due to the ... More
SyGuS-Comp 2018: Results and AnalysisApr 12 2019Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation $f$ that meets both a semantic constraint given by a logical formula $\phi$ in a background theory $\mathbb{T}$, and a syntactic constraint given by a grammar $G$, ... More
Verified Optimization in a Quantum Intermediate RepresentationApr 12 2019We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate ... More
Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and ApplicationsApr 12 2019This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and ... More
Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees - Extended VersionApr 11 2019Applications in many domains are based on a series of traversals of tree structures, and fusing these traversals together to reduce the total number of passes over the tree is a common, important optimization technique. In applications such as compilers ... More
Synthesizing Database Programs for Schema RefactoringApr 11 2019Many programs that interact with a database need to undergo schema refactoring several times during their life cycle. Since this process typically requires making significant changes to the program's implementation, schema refactoring is often non-trivial ... More
Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrencyApr 10 2019Crary and Sullivan's Relaxed Memory Calculus (RMC) proposed a new declarative approach for writing low-level shared memory concurrent programs in the presence of modern relaxed-memory multi-processor architectures and optimizing compilers. In RMC, the ... More
Tea: A High-level Language and Runtime System for Automating Statistical AnalysisApr 10 2019Though statistical analyses are centered on research questions and hypotheses, current statistical analysis tools are not. Users must first translate their hypotheses into specific statistical tests and then perform API calls with functions and parameters. ... More
A HoTT Quantum Equational Theory (Extended Version)Apr 08 2019This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum ... More
Verification Logics for Quantum ProgramsApr 08 2019We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare ... More
Mek: Mechanics Prototyping Tool for 2D Tile-Based Turn-Based Deterministic GamesApr 06 2019There are few digital tools to help designers create game mechanics. A general language to express game mechanics is necessary for rapid game design iteration. The first iteration of a mechanics-focused language, together with its interfacing tool, are ... More
Type-Level Computations for Ruby LibrariesApr 06 2019Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a ... More
On the Representation of Partially Specified Implementations and its Application to the Optimization of Linear Algebra Kernels on GPUApr 06 2019Traditional optimizing compilers rely on rewrite rules to iteratively apply program transformations. This iterative approach hides optimization opportunities behind intermediate transformation steps. For instance, vectorization can only be applied to ... More
Exploring and Benchmarking High Performance & Scientific Computing using R R HPC Packages and Lower level compiled languages A Comparative StudyApr 06 2019R is a robust open-source programming language mainly used for statistical computing . Many areas of statistical research are experiencing rapid growth in the size of data sets. Methodological advances drive increased use of simulations. A common approach ... More
A Literature Study of Embeddings on Source CodeApr 05 2019Natural language processing has improved tremendously after the success of word embedding techniques such as word2vec. Recently, the same idea has been applied on source code with encouraging results. In this survey, we aim to collect and discuss the ... More
An Evolutionary Framework for Automatic and Guided Discovery of AlgorithmsApr 05 2019This paper presents Automatic Algorithm Discoverer (AAD), an evolutionary framework for synthesizing programs of high complexity. To guide evolution, prior evolutionary algorithms have depended on fitness (objective) functions, which are challenging to ... More
Proving tree algorithms for succinct data structuresApr 04 2019Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different ... More
Symbolic Exact Inference for Discrete Probabilistic ProgramsApr 03 2019The computational burden of probabilistic inference remains a hurdle for applying probabilistic programming languages to practical problems of interest. In this work, we provide a semantic and algorithmic foundation for efficient exact inference on discrete-valued ... More
Symbolic Exact Inference for Discrete Probabilistic ProgramsApr 03 2019Apr 11 2019The computational burden of probabilistic inference remains a hurdle for applying probabilistic programming languages to practical problems of interest. In this work, we provide a semantic and algorithmic foundation for efficient exact inference on discrete-valued ... More
A Message-Passing Interpretation of Adjoint LogicApr 02 2019We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, ... More
Value-Dependent Session Design in a Dependently Typed LanguageApr 02 2019Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care ... More
Multiparty Session Type-safe Web Development with Static LinearityApr 02 2019Modern web applications can now offer desktop-like experiences from within the browser, thanks to technologies such as WebSockets, which enable low-latency duplex communication between the browser and the server. While these advances are great for the ... More
Concurrent Typestate-Oriented Programming in JavaApr 02 2019We describe a generative approach that enables concurrent typestate-oriented programming in Java and other mainstream languages. The approach allows programmers to implement objects exposing a state-sensitive interface using a high-level synchronization ... More
FreeST: Context-free Session Types in a Functional LanguageApr 02 2019FreeST is an experimental concurrent programming language. Based on a core linear functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types ... More
Service Equivalence via Multiparty Session Type IsomorphismsApr 02 2019This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Multiparty ... More
Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program VerificationApr 01 2019We present a new inductive proof rule for reasoning about lower bounds on weakest preexpectations, i.e., expected values of random variables after execution of a probabilistic loop. Our rule is simple in the sense that the semantics of the loop needs ... More
Modular Synthesis of Divide-and-Conquer Parallelism for Nested Loops (Extended Version)Apr 01 2019We propose a methodology for automatic generation of divide-and-conquer parallel implementations of sequential nested loops. We focus on a class of loops that traverse read-only multidimensional collections (lists or arrays) and compute a function over ... More
A benchmark for C program verificationApr 01 2019We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last ... More
A Provable Defense for Deep Residual NetworksMar 29 2019We present a training system, which can provably defend significantly larger neural networks than previously possible, including ResNet-34 and DenseNet-100. Our approach is based on differentiable abstract interpretation and introduces two novel concepts: ... More
Using Structured Input and Modularity for Improved LearningMar 29 2019We describe a method for utilizing the known structure of input data to make learning more efficient. Our work is in the domain of programming languages, and we use deep neural networks to do program analysis. Computer programs include a lot of structural ... More
Proving Differential Privacy with Shadow ExecutionMar 28 2019Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness -- generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those ... More
Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input GenerationMar 28 2019We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the ... More
Generalized Convolution and Efficient Language RecognitionMar 26 2019Convolution is a broadly useful operation with applications including signal processing, machine learning, probability, optics, polynomial multiplication, and efficient parsing. Usually, however, this operation is understood and implemented in more specialized ... More
Lost in translation: Exposing hidden compiler optimization opportunitiesMar 25 2019Mar 28 2019To increase productivity, today's compilers offer a two-fold abstraction: they hide hardware complexity from the software developer, and they support many architectures and programming languages. At the same time, due to fierce market competition, most ... More
The Random Conditional Distribution for Higher-Order Probabilistic InferenceMar 25 2019The need to condition distributional properties such as expectation, variance, and entropy arises in algorithmic fairness, model simplification, robustness and many other areas. At face value however, distributional properties are not random variables, ... More
On Evaluating the Renaissance Benchmarking Suite: Variety, Performance, and ComplexityMar 25 2019The recently proposed Renaissance suite is composed of modern, real-world, concurrent, and object-oriented workloads that exercise various concurrency primitives of the JVM. Renaissance was used to compare performance of two stateof-the-art, production-quality ... More
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation LogicMar 22 2019We introduce a new dynamic analysis technique to discover invariants in separation logic for heap-manipulating programs. First, we use a debugger to obtain rich program execution traces at locations of interest on sample inputs. These traces consist of ... More
Active-Code Replacement in the OODIDA Data Analytics PlatformMar 22 2019OODIDA (On-board/Off-board Distributed Data Analytics) is a platform for distributing and executing concurrent data analysis tasks. It targets a fleet of reference vehicles in the automotive industry and has a particular focus on rapid prototyping. Its ... More
Elaborating Inductive Datatypes and Course-of-Values Pattern Matching to CedilleMar 19 2019In CDLE, a pure Curry-style type theory, it is possible to generically derive induction for {\lambda}-encoded data whose types are least fixed points of functors. From this comes fruitful research into the design-space for datatype systems: \cite{FDJS18_CoV-Ind} ... More
No more, no less - A formal model for serverless computingMar 19 2019Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. ... More
Specification and Inference of Trace Refinement RelationsMar 18 2019Modern software is constantly changing. Researchers and practitioners are increasingly aware that verification tools can be impactful if they embrace change through analyses that are compositional and span program versions. Reasoning about similarities ... More
Compiler-assisted Adaptive Program Scheduling in big.LITTLE SystemsMar 17 2019Energy-aware architectures provide applications with a mix of low (LITTLE) and high (big) frequency cores. Choosing the best hardware configuration for a program running on such an architecture is difficult, because program parts benefit differently from ... More
Replication-Aware LinearizabilityMar 15 2019Geo-distributed systems often replicate data at multiple locations to achieve availability and performance despite network partitions. These systems must accept updates at any replica and propagate these updates asynchronously to every other replica. ... More
Get rid of inline assembly through trustable verification-oriented liftingMar 15 2019Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable ... More
Mutual CoinductionMar 14 2019Mar 21 2019In this paper we present mutual coinduction as a dual of mutual induction and also as a generalization of standard coinduction. In particular, we present a precise formal definition of mutual induction and mutual coinduction. In the process we present ... More
Mutual CoinductionMar 14 2019Mar 19 2019In this paper we present mutual coinduction as a dual of mutual induction and as a generalization of standard coinduction. In particular, we present a formal definition of mutual induction and mutual coinduction, and in the process we present, and prove, ... More
Mutual CoinductionMar 14 2019In this paper we present mutual coinduction as a dual of mutual induction and as a generalization of standard coinduction. In particular, we present a formal definition of mutual induction and mutual coinduction, and in the process we present, and prove, ... More
Mutual CoinductionMar 14 2019Apr 08 2019In this paper we present mutual coinduction as a dual of mutual induction and also as a generalization of standard coinduction. In particular, we present a precise formal definition of mutual induction and mutual coinduction. In the process we present ... More
Simply RaTT: A Fitch-style Modal Calculus for Reactive ProgrammingMar 14 2019Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all programs are causal, ... More
SymPas: Symbolic Program SlicingMar 13 2019Program slicing is a technique for simplifying programs by focusing on selected aspects of their behaviour. Current mainstream static slicing methods operate on the PDG (program dependence graph) or SDG (system dependence graph), but these friendly graph ... More
Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program VerificationMar 11 2019Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects ... More
Certifying Safety when Implementing ConsensusMar 08 2019Ensuring the correctness of distributed system implementations remains a challenging and largely unaddressed problem. In this paper we present a protocol that can be used to certify the safety of consensus implementations. Our proposed protocol is efficient ... More
Formal Constraint-based Compilation for Noisy Intermediate-Scale Quantum SystemsMar 08 2019Noisy, intermediate-scale quantum (NISQ) systems are expected to have a few hundred qubits, minimal or no error correction, limited connectivity and limits on the number of gates that can be performed within the short coherence window of the machine. ... More
Deductive Optimization of Relational Data StorageMar 08 2019Optimizing the physical data storage and retrieval of data are two key database management problems. In this paper, we propose a language that can express a wide range of physical database layouts, going well beyond the row- and column- based methods ... More
Only Connect, SecurelyMar 07 2019The lattice model proposed by Denning in her seminal work provided secure information flow analyses with an intuitive and uniform mathematical foundation. Different organisations, however, may employ quite different security lattices. In this paper, we ... More
LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable ModelsMar 06 2019We develop a new Low-level, First-order Probabilistic Programming Language (LF-PPL) suited for models containing a mix of continuous, discrete, and/or piecewise-continuous variables. The key success of this language and its compilation scheme is in its ... More
Lenses and LearnersMar 05 2019Lenses are a well-established structure for modelling bidirectional transformations, such as the interactions between a database and a view of it. Lenses may be symmetric or asymmetric, and may be composed, forming the morphisms of a monoidal category. ... More
Custom Code Generation for a Graph DSLMar 05 2019Graph algorithms are at the heart of several applications, and achieving high performance with them has become critical due to the tremendous growth of irregular data. However, irregular algorithms are quite challenging to parallelize automatically, due ... More
Dijkstra Monads for AllMar 04 2019This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational ... More
Oxide: The Essence of RustMar 03 2019Rust is a major advancement in industrial programming languages due in large part to its success in bridging the gap between low-level systems programming and high-level application programming. This success has ultimately empowered programmers to more ... More
Semantics of higher-order probabilistic programs with conditioningFeb 28 2019We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the ... More
Stateful Dataflow Multigraphs: A Data-Centric Model for High-Performance Parallel ProgramsFeb 27 2019With the ubiquity of accelerators, such as FPGAs and GPUs, the complexity of high-performance programming is increasing beyond the skill-set of the average scientist in domains outside of computer science. It is thus imperative to decouple programming ... More
TensorFlow Eager: A Multi-Stage, Python-Embedded DSL for Machine LearningFeb 27 2019TensorFlow Eager is a multi-stage, Python-embedded domain-specific language for hardware-accelerated machine learning, suitable for both interactive research and production. TensorFlow, which TensorFlow Eager extends, requires users to represent computations ... More
Sound Invariant Checking Using Type Modifiers and Object CapabilitiesFeb 26 2019In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees that class invariants hold for all objects involved in execution. Invariants ... More
Induction, Coinduction, and Fixed Points in PL Type TheoryFeb 26 2019Recently we presented a concise survey of the formulation of the induction and coinduction principles, and some concepts related to them, in programming languages type theory and four other mathematical disciplines. The presentation in type theory involved ... More
The $C_π$-calculus: a Model for Confidential Name PassingFeb 26 2019Feb 27 2019Sharing confidential information in distributed systems is a necessity in many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which dissemination of ... More
Iteratively Composing Statically Verified TraitsFeb 26 2019Metaprogramming is often used to programmatically generate faster specialised code when some parameters are known in advance. To use metaprogramming and SV together, we could generate code containing contracts, and such code could be checked after metaprogramming ... More
Reliable State Machines: A Framework for Programming Reliable Cloud ServicesFeb 25 2019Feb 27 2019Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. ... More
A Systematic Impact Study for Fuzzer-Found Compiler BugsFeb 25 2019Despite much recent interest in randomised testing (fuzzing) of compilers, the practical impact of fuzzer-found miscompilations on real-world applications has barely been assessed. We present the first quantitative study of the tangible impact of fuzzer-found ... More
A Systematic Impact Study for Fuzzer-Found Compiler BugsFeb 25 2019Apr 08 2019Despite much recent interest in compiler fuzzing, the practical impact of fuzzer-found miscompilations on real-world applications has barely been assessed. We present the first quantitative and qualitative study of the tangible impact of fuzzer-found ... More
Neural Reverse Engineering of Stripped BinariesFeb 25 2019We address the problem of predicting procedure names in stripped executables which contain no debug information. Predicting procedure names can dramatically ease the task of reverse engineering, saving precious time and human effort. We present a novel ... More
Mitigating Power Side Channels during CompilationFeb 25 2019The code generation modules inside modern compilers such as GCC and LLVM, which use a limited number of CPU registers to store a large number of program variables, may introduce side-channel leaks even in software equipped with state-of-the-art countermeasures. ... More
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart ContractsFeb 23 2019Mar 09 2019This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services at the source code level of smart contracts, and a Coq proof assistant ... More
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart ContractsFeb 23 2019This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services at the source code level of smart contracts, and a Coq proof assistant ... More
Optimizing Space of Parallel ProcessesFeb 22 2019This paper is a contribution to exploring and analyzing space-improvements in concurrent programming languages, in particular in the functional process-calculus CHF. Space-improvements are defined as a generalization of the corresponding notion in deterministic ... More
Automating the Diagram Method to Prove Correctness of Program TransformationsFeb 22 2019We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct ... More
Reducing Total Correctness to Partial Correctness by a Transformation of the Language SemanticsFeb 22 2019We give a language-parametric solution to the problem of total correctness, by automatically reducing it to the problem of partial correctness, under the assumption that an expression whose value decreases with each program step in a well-founded order ... More