[All BiBTeX entries for this year]

E.D. Schabell, and S.J.B.A. (Stijn) Hoppenbrouwers. * Empowering Full Scale Straight Through Processing with BPM. *Technical report: ICIS-R08004, February, SNS Bank, 2009.

The SNS Bank (the Netherlands) has made a strategic decision to empower her customers on-line by fully automating her business processes. The ability to automate these service channels is achieved by applying Business Process Management (BPM) techniques to existing selling channels. Both the publicly available and internal processes are being revamped into full scale Straight Through Processing (STP) services. This extreme use of on-line STP is the trigger in a shift that is of crucial importance to cost effective banking in an ever turbulent and changing financial world. The key elements used in implementing these goals continue to be (Free) Open Source Software (FOSS), Service oriented architecture (SOA), and BPM. In this paper we present an industrial application describing the efforts of SNS Bank to make the change from traditional banking services to a full scale STP and BPM driven bank.

[ PDF ] [ Bibtex ] [ External URL ]

Christian Haack, and Erik Poll. * Type-based Object Immutability with Flexible Initialization. *Technical report: ICIS-R09001, January, Radboud University Nijmegen, 2009.

We present a type system for checking object immutability, reference immutability, and class immutability in an open or closed world. In order to separate object initialization from object constructors (which is often needed in practice), immutable objects are initialized in lexically scoped regions. The system is simple and direct; its only type qualifiers specify immutability properties. No auxiliary annotations, e.g., ownership types, are needed, yet good support for deep immutability is provided. To express object confinement, as required for class immutability in an open world, we make use of qualifier polymorphism. The system has two versions: one version with explicit specification commands that delimit the object initialization phase, and one version where such commands are implicit and inferred. In the latter version, all annotations are compatible with Java`s extended annotation syntax, as proposed in JSR 308.

Lionel Elie Mamane, Herman Geuvers, and James McKinna. * A Saturated Extension of Lambda-Bar-Mu-Mu-Tilde. *Technical report: ICIS-R09002, July, Radboud University Nijmegen, 2009.

This report presents a proof language based on the work of Sacerdoti Coen, Kirchner and Autexier on lambda-bar-mu-mu-tilde,a calculus introduced by Curien and Herbelin. Just as lambda-bar-mu-mu-tilde preserves several proof structures that are identified by the lambda-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being /logically saturated/. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses. We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar. lambda-bar-mu-mu-tilde is a proof term language for sequent calculus proofs; the pseudo-natural language rendering thus contributes a way to talk about these proofs in natural language.

[ PDF ] [ Bibtex ] [ External URL ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. * Collected Size Semantics for Functional Programs over Polymorphic Nested Lists. *Technical report: ICIS-R09003, July, Radboud University Nijmegen, 2009.

Size analysis is an important prerequisite for heap consumption analysis. This paper is part of ongoing work about typing support for checking output-on-input size dependencies for function definitions in a strict functional language. A significant restriction for our earlier results is that emph{inner} data structures (e.g. in a list of lists) all must have the same size. Here, we make a big step forwards by overcoming this limitation via the introduction of higher-order size annotations such that variate sizes of inner data structures can be expressed.

Wojciech Mostowski, and Erik Poll. * Midlet Navigation Graphs in JML. *Technical report: ICIS-R09004, August, Radboud University Nijmegen, 2009.

In the context of the Mobius project on Proof Carrying Code for mobile device Java applications (so called midlets), we present a way to formalise midlet navigation graphs in Java Modelling Language. Navigation graphs are used to express certain security policies of a midlet. Our resulting JML specifications are automatically verifiable with the static Java checker ESC/Java2. In the paper we relate to the earlier work on midlet navigation graphs generation from Java bytecode. Our work complements this earlier work by providing a mechanisms for establishing midlet navigation graph properties. In the paper we also discuss in detail practical difficulties with creating efficient and meaningful JML specifications for automatic verification with a lightweight verification tool. Our work was guided by one of the Mobius project realistically sized case studies developed by our industrial partners.

Jozef Hooman, and Marcel Verhoef. * Formal Semantics of a VDM Extension for Distributed Embedded Systems. *Technical report: ICIS-R09005, December, Radboud University Nijmegen, 2009.

To support model-based development and analysis of embedded systems, the specification language VDM++ has been extended with asynchronous communication and improved timing primitives. In addition, we have defined an interface for the co-simulation of a VDM++ model with a continuous-time model of its environment. This enables multi-disciplinary design space exploration and continuous validation of design decisions throughout the development process. We present an operational semantics which formalizes the precise meaning of the VDM extensions and the co-simulation concept.

Sander D. Vermolen, Jozef Hooman, and Peter Gorm Larsen. * Proving Consistency of VDM models using HOL. *Technical report: ICIS-R09006, December, Radboud University Nijmegen, 2009.

Although consistency of formal models is crucial, consistency proofs should not be a large burden to the user. Hence, it is important to have access to efficient proof support which is able to automate a large part of the consistency proofs. We have developed a tool that automatically translates a large subset of VDM and its associated proof obligations, which ensure model consistency, to the theorem prover HOL. In addition, powerful tactics have been constructed to discard most of the proof obligations automatically. The application of our approach to four case studies shows that a high degree of automation can be achieved.

Milad Niqui, and Freek Wiedijk. * `Many Digits` Friendly Competition. *Technical report: ICIS-R09007, December, Radboud University Nijmegen, 2009.

In this article we give an account of the ``Many Digits`` friendly competition, a competition between arbitrary precision arithmetic packages that was organised following the competition described in J. Blanck, ``Exact Real Arithmetic Systems: Results of Competition``, and was held on October 3-4, 2005 in order to investigate the state of the art in the field of exact and arbitrary precision arithmetic. The competition consisted of two types of problems, a basic and an intermediate set. The basic problems consisted of simple expressions involving elementary functions. The intermediate problems involved more mathematical construct or slightly more programming. A solution consisted of a sequence of decimal digits, for most problems 10000 digits. The systems were required to calculate the solution within two minutes and depending on their success retry the problem with a higher/lower number of digits. The competition had nine participants, some of them competing remotely.

Marko van Eekelen (editor), and Olha Shkaravska (editor). * International Workshop on Foundational and Practical Aspects of Resource Analysis FOPARA . *Technical report: ICIS-R09008, December, Radboud University Nijmegen, 2009.

The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (time, space) consumption by computer programs. FOPARA aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions have been encouraged. The contributions cover the following topics: resource analysis for embedded systems, logical and machine-independent characterisations of complexity classes, logics closely related to complexity classes, type systems for controlling complexity, semantic methods to analyse resources, incl. quasi- and sup-interpretations, practical applications of resource analysis, etc. After the workshop the program committee will select papers for nal proceedings. These nal proceedings will be published by Springer in a volume of the Lecture Notes in Computer Science series.