Digital Security (DiS) Research Publications


2015 2013 2012 2011 2010 2009 2008

Reports

Arjan Lamers, and Marko van Eekelen. Analyzing Isoefficiency of Partition Local Algorithms. Technical report: ICIS-R12003, February, Radboud University Nijmegen, 2012.

For network applications scalable performance is paramount. NoSQL database systems provide us with a tool to achieve scalable systems. In practice, scalability of performance can depend heavily upon the way of partitioning of the data models. To help making these engineering considerations we develop a first step towards a performance model that will incorporate the effects of partitioning. With this basic model we study the scalability properties of algorithms on sets of processors, each with its own statically assigned local part of a given data set. Within this model we calculate the isoefficiency of a special class of algorithms, partition local algorithms (that can run fully within a single partition). We study different algorithm complexity classes and show the validity of our results using a simulator.

[ PDF ] [ Bibtex ]

Attila Gobi, Olha Shkaravska, and Marko van Eekelen. A higher-order size system for a higher-order functional language. Technical report: ICIS-R12005, July, Radboud University Nijmegen, 2012.

The authors present a higher-order size type system for a higher-order functional language. A condition for decidability of type checking is given.

[ PDF ] [ Bibtex ]

Leonard Lensink, Sjaak Smetsers, and Marko van Eekelen. A Proof Framework for Concurrent Programs. Technical report: ICIS-R12001, January, Radboud University Nijmegen, 2012.

This paper presents a proof framework for verifying concurrent programs that communicate using global variables. The approach is geared towards verification of models that have an unbounded state size and are as close to the original code as possible. The bakery algorithm is used as a demonstration of the framework basics, while the (full) framework with thread synchronization was used to verify and correct the reentrant readers writers algorithm as used in the Qt library.

[ PDF ] [ Bibtex ]