SOS Research Publications


2007

Reports

Olha Shkaravska, and M.C.J.D. van Eekelen. Static inference of polynomial size-aware types. Technical report: ICIS-R07028, November, Radboud University Nijmegen, 2007.

We propose a static size analysis procedure that combines term-rewriting and type checking to automatically obtain output-on-input size dependencies for first-order functions. Attention is restricted to functions for which the size of the result is strictly polynomial, not necessarily monotonous, in the sizes of the arguments. To infer a size dependency, the procedure generates hypotheses for increasing degrees of polynomials. For each degree, to define a hypothetical polynomial one needs to know its values on a finite collection of points (subject to some geometrical condition). To compute the value of a size polynomial in a certain point we use a term-rewriting system generated by a standard size-annotations inference procedure. We have proven that if a function with a given input terminates at run-time on a meaningful stack and heap then the static (`compile-time`) term rewriting system of the size inference also terminates, on the integers representing the sizes of the corresponding inputs. The term rewriting system may terminate at compile-time when the underlying function definition does not at run-time. This makes the theoretical applicability of the proposed approach larger than the previous state-of-the-art, where run-time testing was used to generate hypothetical polynomials. Also, the practical applicability is improved due to increased efficiency since the term rewriting system at compile time abstracts from many computations that are done at run-time. We give the proof that if a function body terminates on a meaningful stack and heap then term-rewriting terminates on the integers representing the sizes of inputs. Term-rewriting may terminates when the underlying function definition does not. This makes the applicability of the proposed approach larger then its previous version, where we use run-time testing to generate hypothetical polynomials.

[ PDF ] [ Bibtex ]

C. Haack, E. Poll, J. Schafer, and A. Schubert. Immutable Objects for a Java-like Language. Technical report: ICIS-R07009, April, Radboud University Nijmegen, 2007.

We extend a Java-like language with immutability specifications and a static type system for verifying immutability. A class modifier immutable specifies that all class instances are immutable objects. Ownership types specify the depth of object states and enforce encapsulation of representation objects. The type system guarantees that the state of immutable objects does not visibly mutate during a program run. Provided immutability-annotated classes and methods are final, this is true even if immutable classes are composed with untrusted classes that follow Java

[ PDF ] [ Bibtex ]

Christian Haack, Marieke Huisman, Joe Kiniry, and Erik Poll. Proceedings of the Workshop on Verification and Analysis of Multi-threaded Java-like Programs. Technical report: ICIS-R07021, August, Radboud University Nijmegen, 2007.

This report contains the proceedings of the first Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP), held on September 3, 2007, as a satellite event to CONCUR in Lisbon, Portugal.

[ PDF ] [ Bibtex ]

Wojciech Mostowski, and Erik Poll. Testing the Java Card Applet Firewall. Technical report: ICIS-R07029, December, Radboud University Nijmegen, 2007.

In this paper we discuss the methodology and results of testing the Java Card applet firewall mechanism. The main motivation for this work is the complexity of the firewall. Given the complexity, non-compliance of the cards with respect to the official specification is not unlikely. Firewall implementation faults may lead to serious security issues. Although we did not discover any serious problems on our test cards, a few minor specification violations are reported. We only found one specification violation on one card that could be considered unsafe, in that it might introduce a security risk for specific applications.

[ PDF ] [ Bibtex ]

Wolter Pieters, and Robert van Haren. E-voting discourses in the UK and the Netherlands. Technical report: ICIS-R07020, August, Radboud University Nijmegen, 2007.

A qualitative case study of the e-voting discourses in the UK and the Netherlands was performed based on the theory of strategic niche management. In both countries, eight e-voting experts were interviewed on their expectations, risk estimations, cooperation and learning experiences. The results show that differences in these variables can partly explain the variations in the embedding of e-voting in the two countries, from a qualitative point of view.

[ PDF ] [ Bibtex ]

O. Shkaravska, R. van Kesteren, and M.C.J.D. van Eekelen. Type Checking and Weak Type Inference for Polynomial Size Analysis of First-Order Functions. Technical report: ICIS-R07004, January, Radboud University Nijmegen, 2007.

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 the arguments. Examples of shapely functions are matrix multiplication and the Cartesian product of two lists. The type checking problem for the type system is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear. Furthermore, an algorithm for weak type inference for this system is given.

[ PDF ] [ Bibtex ]

M.C.J.D. van Eekelen, Stefan ten Hoedt, Rene Schreurs, and Yaroslav Usenko. Modeling and verifying a Real-Life Industrial Session-Layer Protocol in mCRL2. Technical report: ICIS-R07014, June, Radboud University Nijmegen, 2007.

This report describes the analysis of an industrial implementation of the session-layer of a load-balancing software system. This software comprises 7.5 thousand lines of C code. It is used for distribution of the print jobs among several document processors (workers). A large part of this commercially used software system has been modeled closely and analyzed using process-algebraic techniques. Several critical issues were discovered. Since the model was close to the code, all problems that were found in the model, could be traced back to the actual code resulting in concrete suggestions for improvement of the code. All in all, the analysis significantly improved the quality of this real-life system.

[ PDF ] [ Bibtex ]

Hendrik Tews. Proceedings of the C/C++ Verification workshop. Technical report: ICIS-R07015, June, Radboud University Nijmegen, 2007.

This report contains the proceedings of the first C/C++ Verification Workshop held in Oxford on July 2nd, 2007 as a side event of IFM 2007.

[ PDF ] [ Bibtex ]