Name
Abstract | ||
|---|---|---|
We define a method to statically bound the size of values computed during the execution of a program as a function of the size of its parameters. More precisely, we consider bytecode programs that should be executed on a simple stack machine with support for algebraic data types, pattern-matching and tail-recursion. Our size verification method is expressed as a static analysis, performed at the level of the bytecode, that relies on machine-checkable certificates. We follow here the usual assumption that code and certificates may be forged and should be checked before execution. Our approach extends a system of static analyses based on the notion of quasi-interpretations that has already been used to enforce resource bounds on first-order functional programs. This paper makes two additional contributions. First, we are able to check optimized programs, containing instructions for unconditional jumps and tail-recursive calls, and remove restrictions on the structure of the bytecode that was imposed in previous works. Second, we propose a direct algorithm that depends only on solving a set of arithmetical constraints. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11575467_17 | APLAS |
Keywords | Field | DocType |
algebraic data type,bytecode program,optimized program,tail-recursive virtual machine,machine-checkable certificate,direct algorithm,additional contribution,arithmetical constraint,size verification method,first-order functional program,static analysis,functional programming,virtual machine,program analysis,data type,first order,pattern matching | Programming language,Functional programming,Computer science,Static analysis,Theoretical computer science,Data type,Stack machine,Recursion,Distributed computing,Program optimization,Algorithm,Algebraic data type,Bytecode | Conference |
Volume | ISSN | ISBN |
3780 | 0302-9743 | 3-540-29735-9 |
Citations | PageRank | References |
4 | 0.43 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Silvano Dal Zilio | 1 | 157 | 9.91 |
| Régis Gascon | 2 | 76 | 5.23 |