26,098 papers · page 154 of 1,305
C++ is crucial in software development, providing low-level memory control for performance and supporting object-oriented programming to construct modular, reusable code structures. Consequently, tackling pointer analysis for C++ becomes challenging, given the need to address the…
The main goal of most static analyses is to prove the absence of bugs : if the analysis reports no alarms, then the program will not exhibit any unwanted behaviours. For this reason, they are designed to over-approximate program behaviours and, consequently, they can report some …
This article addresses the long-standing problem of program correctness for programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level models expressed as transition systems. The implem…
Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, wh…
Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used i…
Robustness is a key and desirable property of any classifying system, in particular, to avoid the ever-rising threat of adversarial attacks. Informally, a classification system is robust when the result is not affected by the perturbation of the input. This notion has been extens…
Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into execut…
Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The…
We introduce layering to modal type theory to support meta-programming and intensional analysis coherently. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed λ -calculus with no modalit…
Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide developers in designing efficient algorithms, but it can still be difficult to apply algorithmic paradigms to practical tasks. To ease the usage of paradigms, many research efforts have been devoted to t…
Big data analytics frameworks, such as Spark and Giraph, need to process and cache massive datasets that do not always fit on the managed heap. Therefore, frameworks temporarily move long-lived objects outside the heap (off-heap) on a fast storage device. However, this practice r…
Mainstream compilers perform a multitude of analyses and optimizations on the given input program. Each analysis (such as points-to analysis) may generate a program-abstraction (such as points-to graph). Each optimization is typically composed of multiple alternating phases of in…
This article discusses the relationship between two frameworks: universal composability ( \(\mathsf{UC}\) ) and robust compilation ( RC ). In cryptography, \(\mathsf{UC}\) is a framework for the specification and analysis of cryptographic protocols with a strong compositionality …
Data-parallel computations, such as linear algebra routines and stencil computations, constitute one of the most relevant classes in parallel computing, e.g., due to their importance for deep learning. Efficiently de-composing such computations for the memory and core hierarchies…
This article presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence are useful for representing c…
We consider the problem of making expressive, interactive static analyzers compositional . Such a technique could help bring the power of server-based static analyses to integrated development environments (IDEs), updating their results live as the code is modified. Compositional…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.