AHA: Amortized Heap Space Usage Analysis – Project Paper – (2009)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
Abstract: This paper introduces AHA, an NWO-funded2 344K Euro project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
Polynomial Size Analysis of First-Order Shapely Functions (2009)
Shkaravska, Olha, Van Eekelen, Marko, Van Kesteren, Ron
We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a polynomial in...
Chapter 14 Project Evaluation Paper: Mobile Resource Guarantees (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resource bounds of mobile code. Key components of this infrastructure are a...
Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Lennart Beringer, Hans-wolfgang Loidl, ...
This paper summarises the main outcomes of the Mobile Resource Guarantees (MRG) project, a three year project funded by the EC under the FET proactive initiative on Global Computing, and discusses...
Type Checking and Weak Type Inference for Polynomial Size Analysis of First-Order Functions (2008)
Olha Shkaravska, Ron Van Kesteren, Marko Van Eekelen
Abstract. We present a size-aware type system for first-order shapely functions. Here, a function is called shapely when the size of the result is determined exactly by a polynomial in the sizes of...
A finite array � A, sel, upd � with values from the set V and locations in the set L is the set A equipped with sel: A × L → V and upd: A × L × V → A operations subject to the equations of...
Chapter 1 Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for resources to be applied to mobile code. Key components of this infrastructure are a...
AHA: Amortized Heap Space Usage Analysis – Project Paper – (2008)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
This paper introduces AHA, an NWO-funded 1 344K Euro research project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
Chapter 1 Mobile Resource Guarantees Evaluation Paper (2008)
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, ...
Abstract: This paper summarises the main outcomes of the Mobile Resource Guarantees (MRG) project, which focused on a proof-carrying-code (PCC) infrastructure for resources to be applied to mobile...
Eekelen. Polynomial size analysis of first-order functions (2007)
Olha Shkaravska, Ron Van Kesteren, Marko Van Eekelen
Abstract. We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a...
Stochastic simulation methods applied to a secure electronic voting model, (2005)
Nigel Thomas, Jeremy Bradley, Coffee Break, Charles Kubicek, Avelino F. Zorzo, ...
Estimating the cost of native method calls for resource-bounded functional programming languages,
Automatic Certification of Heap Consumption (2005)
Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
Abstract. We present a program logic for verifying the heap consumption of low-level programs. The proof rules employ a uniform assertion format and have been derived from a general purpose program...
Towards certificate generation for linear heap consumption (2004)
Lennart Beringer, Martin Hofmann, Alberto Momigliano, Olha Shkaravska
representation of the Java virtual machine language. The logic is defined by an expansion into the more general level, without recourse to the base logic. Format and interpretation of assertions...