26,098 papers · page 459 of 1,305
We describe a formal verification framework and tool implementation, based upon cyclic proofs, for certifying the safe termination of imperative pointer programs with recursive procedures. Our assertions are symbolic heaps in separation logic with user defined inductive predicate…
Karp-Miller tree construction on Petri nets is a classical well-known algorithm to construct the minimal coverability set via forward analysis. It enables us to construct decision procedures for several problems such as coverability and (place) boundedness. This paper formalizes …
Modern object-oriented programming languages greatly alleviate the memory management for programmers. Despite the efficiency of garbage collection and Just-In-Time program analyzes, memory still remains prone to be wasted.
JavaScript code running in the Node.js runtime is a major platform for developers building cloud, mobile, or IoT applications. A fundamental concept in Node.js programming is the use of asynchronous callbacks and event loops to provide highly responsive applications. While concep…
Today's complex software systems combine high-level concurrency models. Each model is used to solve a specific set of problems. Unfortunately, debuggers support only the low-level notions of threads and shared memory, forcing developers to reason about these notions instead of th…
In dynamic object-oriented languages, low-level mechanisms such as just-in-time compilation, object allocation, garbage collection (GC) and method dispatch are often handled by virtual machines (VMs). VMs are typically implemented using static languages, allowing only few changes…
JavaScriptCore (JSC) is an open-source high-performance implementation of JavaScript. JSC is used in the WebKit open source browser engine as well as a system framework on macOS and iOS. This talk will give a broad high-level overview of JSC’s performance-oriented architecture, i…
Mixing static and dynamic type checking in the same language is catching on, with the TypeScript and Flow variants of JavaScript, the MyPy and Reticulated variants of Python, the Strongtalk and Gradualtalk variants of Smalltalk, as well as Typed Racket, Typed Clojure, and Perl 6.…
We provide formal semantics for a large subset of the Lua programming language, in its version 5.2. We validate our model by mechanizing it and testing it against the test suite of the reference interpreter of Lua, obtaining evidence that our model accurately represents the langu…
Swift is a modern multi-paradigm programming language with an extensive developer community and open source ecosystem. Swift 3's memory management strategy is based on Automatic Reference Counting (ARC) augmented with unsafe APIs for manually-managed memory. We have seen ARC cons…
Grace is a dynamic object oriented programming language designed to aid programming education. We present a formal model of and give an operational semantics for its object model and name resolution algorithm. Our main contributions are a systematic model of Grace’s name resoluti…
In a precise data race detector, a race is detected only if the execution exhibits a real race. In such tools, every memory access from each thread is typically checked by a happens-before algorithm. What’s the optimal runtime performance of such tools? In this paper, we identify…
Computational scientists often prototype software using productivity languages that offer high-level programming abstractions. When higher performance is needed, they are obliged to rewrite their code in a lower-level efficiency language. Different solutions have been proposed to…
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Te…
The power of languages is rooted in composition. An infinite number of sentences can be composed from a finite set of generative rules. The more uniformly the rules apply, the more valid compositions there are. Hence simpler rules give rise to richer discourse - a case of ‘less i…
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement prot…
Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theo…
Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in tim…
In recent years, multiple vulnerabilities exploiting the serialisation APIs of various programming languages, including Java, have been discovered. These vulnerabilities can be used to devise in- jection attacks, exploiting the presence of dynamic programming language features li…
The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checki…