Sciweavers

SAS
2009
Springer
149views Formal Methods» more  SAS 2009»
14 years 6 months ago
Creating Transformations for Matrix Obfuscation
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...
Stephen Drape, Irina Voiculescu
SAS
2009
Springer
147views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Polymorphic Fractional Capabilities
Abstract. The capability calculus is a framework for statically reasoning about program resources such as deallocatable memory regions. Fractional capabilities, originally proposed...
Hirotoshi Yasuoka, Tachio Terauchi
SAS
2009
Springer
281views Formal Methods» more  SAS 2009»
15 years 3 hour ago
A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination
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...
SAS
2009
Springer
175views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Automatic Parallelization and Optimization of Programs by Proof Rewriting
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...
Clément Hurlin
SAS
2009
Springer
214views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Abstract Interpretation of FIFO Replacement
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...
Daniel Grund, Jan Reineke
SAS
2009
Springer
147views Formal Methods» more  SAS 2009»
15 years 3 hour ago
The Complexity of Andersen's Analysis in Practice
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...
Manu Sridharan, Stephen J. Fink
SAS
2009
Springer
119views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Abstraction Refinement for Quantified Array Assertions
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...
SAS
2009
Springer
171views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Bottom-Up Shape Analysis
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...
SAS
2009
Springer
148views Formal Methods» more  SAS 2009»
15 years 3 hour ago
Abstract Interpretation from a Topological Perspective
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...
David A. Schmidt