1,205 papers · page 4 of 61
Tobias Runge, Marco Servetto, Alex Potanin, Ina Schaefer
Security-critical software applications contain confidential information which has to be protected from leaking to unauthorized systems. With language-based techniques, the confidentiality of applications can be enforced. Such techniques are for example type systems that enforce …
Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, Talia Ringer
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpora to synthesize proofs have ju…
Elizabeth Scott, Adrian Johnstone, Robert Walsh
This article introduces two new approaches in the areas of lexical analysis and context-free parsing. We present an extension, MGLL, of generalised parsing which allows multiple input strings to be parsed together efficiently, and we present an enhanced approach to lexical analys…
Luigi D. C. Soares, Michael Canesche, Fernando Magno Quintão Pereira
Partial control-flow linearization is a code transformation conceived to maximize work performed in vectorized programs. In this article, we find a new service for it. We show that partial control-flow linearization protects programs against timing attacks. This transformation is…
Matías Toro, David Darais, Chike Abuah, Joseph P. Near, Damián Árquez, Federico Olmedo, Éric Tanter
Language support for differentially private programming is both crucial and delicate. While elaborate program logics can be very expressive, type-system-based approaches using linear types tend to be more lightweight and amenable to automatic checking and inference, and in partic…
Maja Vukasovic, Aleksandar Prokopec
Availability of profiling information is a major advantage of just-in-time (JIT) compilation. Profiles guide the compilation order and optimizations, thus substantially improving program performance. Ahead-of-time (AOT) compilation can also utilize profiles, obtained during separ…
Eugene Yip, Alain Girault, Partha S. Roop, Morteza Biglari-Abhari
Embedded real-time systems are tightly integrated with their physical environment. Their correctness depends both on the outputs and timeliness of their computations. The increasing use of multi-core processors in such systems is pushing embedded programmers to be parallel progra…
Patrick Baillot, Alexis Ghyselen
Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular, some systems allow one to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to par…
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei
Dedicated to Tony Hoare. In a paper published in 1972, Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: co…
Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this article, we present the metatheory of…
Chaoqiang Deng, Patrick Cousot
Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is pr…
Dominique Devriese, Marco Patrignani, Frank Piessens
The formal calculus System F models the essence of polymorphism and abstract data types, features that exist in many programming languages. The calculus’ core property is parametricity: a theorem expressing the language’s abstractions and validating important principles like info…
Maria I. Gorinova, Andrew D. Gordon, Charles Sutton, Matthijs Vákár
A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to re-write their models to improve efficiency of inference or meet restrictions imposed by the PPL. Con…
Maximilian P. L. Haslbeck, Peter Lammich
We present a framework to verify both, functional correctness and (amortized) worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structure the resource analysis alon…
Martin Hecker, Simon Bischof, Gregor Snelting
We present efficient algorithms for time-sensitive control dependencies (CDs). If statement y is time-sensitively control dependent on statement x , then x decides not only whether y is executed but also how many timesteps after x . If y is not standard control dependent on x , b…
Qinheping Hu, Rishabh Singh, Loris D'Antoni
Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popul…
Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use …
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Determining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource compl…
Alex C. Keizer, Henning Basold, Jorge A. Pérez
Compositional methods are central to the verification of software systems. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can st…
Ori Lahav, Udi Boker
While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still unclear. In this article, we es…