1,205 papers · page 11 of 61
Gregor Wagner, Per Larsen, Stefan Brunthaler, Michael Franz
The web browser is the “new desktop.” Not only do many users spend most of their time using the browser, the browser has also become host to rich and dynamic applications that were previously tailored to each individual operating system. The lingua franca of web scripting, JavaSc…
Paraskevas Yiapanis, Gavin Brown, Mikel Luján
Current parallelizing compilers can tackle applications exercising regular access patterns on arrays or affine indices, where data dependencies can be expressed in a linear form. Unfortunately, there are cases that independence between statements of code cannot be guaranteed and …
Andrew W. Appel
This article presents a full formal machine-checked verification of a C program: the OpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C is a separation logic for …
Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, John Wickerson
We present a technique for the formal verification of GPU kernels, addressing two classes of correctness properties: data races and barrier divergence. Our approach is founded on a novel formal operational semantics for GPU kernels termed synchronous, delayed visibility (SDV) sem…
Dariusz Biernacki, Olivier Danvy, Kevin Millikin
We put a preexisting definitional abstract machine for dynamic delimited continuations in defunctionalized form, and we present the consequences of this adjustment. We first prove the correctness of the adjusted abstract machine. Because it is in defunctionalized form, we can ref…
Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, Matteo Maffei
Recent research has shown that it is possible to leverage general-purpose theorem-proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many respects, these type systems fall sho…
Loris D'Antoni, Margus Veanes, Benjamin Livshits, David Molnar
Tree automata and transducers are used in a wide range of applications in software engineering. While these formalisms are of immense practical use, they can only model finite alphabets. To overcome this problem we augment tree automata and transducers with symbolic alphabets rep…
Michael Frechtling, Philip Heng Wai Leong
Runtime analysis provides an effective method for measuring the sensitivity of programs to rounding errors. To date, implementations have required significant changes to source code, detracting from their widespread application. In this work, we present an open source system that…
Nils Gesbert, Pierre Genevès, Nabil Layaïda
We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types, together with type variables. We consider the subtyping relation defined by Castagna and Xu [2011] over such type expressions and show how this relation can be decide…
Tobias Grosser, Sven Verdoolaege, Albert Cohen
Abstract mathematical representations such as integer polyhedra have been shown to be useful to precisely analyze computational kernels and to express complex loop transformations. Such transformations rely on abstract syntax tree (AST) generators to convert the mathematical repr…
Baris Kasikci, Cristian Zamfir, George Candea
Data races are one of the main causes of concurrency problems in multithreaded programs. Whether all data races are bad, or some are harmful and others are harmless, is still the subject of vigorous scientific debate [Narayanasamy et al. 2007; Boehm 2012]. What is clear, however,…
Gary T. Leavens, David A. Naumann
Verification of a dynamically dispatched method call, E . m (), seems to depend on E ’s dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction. In other words, one reasons about E . m () using m ’s s…
Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, Frank Piessens
A fully abstract compiler prevents security features of the source language from being bypassed by an attacker operating at the target language level. Unfortunately, developing fully abstract compilers is very complex, and it is even more so when the target language is an untyped…
Farn Wang, Sven Schewe, Chung-Hao Huang
We propose an extension to ATL ( alternating-time temporal logic ), called BSIL ( basic strategy-interaction logic ), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL + but incomparable with ATL * , GL ( game…
Alexander Kaiser, Daniel Kroening, Thomas Wahl
Pthread-style multithreaded programs feature rich thread communication mechanisms, such as shared variables, signals, and broadcasts. In this article, we consider the automated verification of such programs where an unknown number of threads execute a given finite-data procedure …
Sheng Chen, Martin Erwig, Eric Walkingshaw
Through the use of conditional compilation and related tools, many software projects can be used to generate a huge number of related programs. The problem of typing such variational software is difficult. The brute-force strategy of generating all variants and typing each one in…
Jade Alglave, Luc Maranget, Michael Tautschnig
We propose an axiomatic generic framework for modelling weak memory. We show how to instantiate this framework for Sequential Consistency (SC), Total Store Order (TSO), C++ restricted to release-acquire atomics, and Power. For Power, we compare our model to a preceding operationa…
Min Aung, Susan Horwitz, Richard Joiner, Thomas W. Reps
This paper defines a new variant of program slicing, called specialization slicing , and presents an algorithm for the specialization-slicing problem that creates an optimal output slice. An algorithm for specialization slicing is polyvariant : for a given procedure р, the algori…
Gilles Barthe, Delphine Demange, David Pichardie
CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it ha…
Camil Demetrescu, Irene Finocchi, Andrea Ribichini
Dataflow languages provide natural support for specifying constraints between objects in dynamic applications, where programs need to react efficiently to changes in their environment. In this article, we show that one-way dataflow constraints, largely explored in the context of …