There are many programming situations where it would be convenient to conceal the meaning of code, or the meaning of certain variables. This can be achieved through program transfo...
Abstract. The capability calculus is a framework for statically reasoning about program resources such as deallocatable memory regions. Fractional capabilities, originally proposed...
The Java programming language requires that out-of-bounds array accesses produce runtime exceptions. In general, this requires a dynamic bounds check each time an array element is...
David Niedzielski, Jeffery von Ronne, Andreas Gamp...
We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized an...
Interpretation of FIFO Replacement Daniel Grund and Jan Reineke Saarland University, Saarbr?ucken, Germany In hard real-time systems, the execution time of programs must be bounded...
Abstract. While the tightest proven worst-case complexity for Andersen's points-to analysis is nearly cubic, the analysis seems to scale better on real-world codes. We examine...
ion Refinement for Quantified Array Assertions Mohamed Nassim Seghir1, , Andreas Podelski1 , and Thomas Wies1,2 1 University of Freiburg, Germany 2 EPFL, Switzerland Abstract. We p...
Mohamed Nassim Seghir, Andreas Podelski, Thomas Wi...
In this paper we present a new shape analysis algorithm. The key distinguishing aspect of our algorithm is that it is completely compositional, bottom-up and non-iterative. We pres...
Bhargav S. Gulavani, Supratik Chakraborty, Ganesan...
Interpretation from a Topological Perspective David A. Schmidt Kansas State University, Manhattan, Kansas, USA Abstract. Topology is the study of property sets (open sets) and cont...