September 2006 - tr-announce - lists.rwth-aachen.de

2006-05: Adjoint Code by Source Transformation with OpenAD/F
by Peter Schneider-Kamp 26 Sep '06

26 Sep '06

The following technical report is available from http://aib.informatik.rwth-aachen.de: Adjoint Code by Source Transformation with OpenAD/F Uwe Naumann, Jean Utke, Patrick Heimbach, Chris Hill, Derya Ozyurt, Carl Wunsch, Mike Fagan, Nathan Tallent, Michelle Strout AIB 2006-05 This document reports on recent advances in the development of the adjoint code generator OpenAD/F. We give an overview of the software design, and we discuss case studies that illustrate the feasibility of adjoint code generation. Our main target application is the MIT General Circulation Model --- a numerical model designed for study of the atmosphere, ocean, and climate.

1 0

2006-09: Counterexamples in Probabilistic Model Checking
by Peter Schneider-Kamp 11 Sep '06

11 Sep '06

The following technical report is available from http://aib.informatik.rwth-aachen.de: Counterexamples in Probabilistic Model Checking Tingting Han, Joost-Pieter Katoen AIB 2006-09 This paper considers algorithms and complexity results for the generation of counterexamples in model checking of probabilistic until-formulae in discrete-time Markov chains (DTMCs). It is shown that finding the strongest evidence (i.e, the most probable path) that violates a (bounded) until-formula can be found in polynomial time using single-source (hop-constrained) shortest path algorithms. We also show that computing the smallest counterexample that is mostly deviating from the required probability bound can be found in a pseudo-polynomial time complexity by adopting a certain class of algorithms for the (hop-constrained) $k$ shortest paths problem.

1 0

2006-11: Model Checking Software for Microcontrollers
by Peter Schneider-Kamp 07 Sep '06

07 Sep '06

The following technical report is available from http://aib.informatik.rwth-aachen.de: Model Checking Software for Microcontrollers Bastian Schlich, Michael Rohrbach, Michael Weber, Stefan Kowalewski AIB 2006-11 A method for model checking of microcontroller code is presented. The main objective is to check embedded C code including typical hardware specific ingredients like embedded assembly statements, direct memory accesses, direct register accesses, interrupts, and timers, without any further manual preprocessing. For this purpose, the state space is generated directly from the assembly code that is generated from C code for the specific microcontroller, in our case the ATMEL ATmega family. The properties to be checked can refer to the global C variables as well as to the microcontroller registers and the SRAM. By this approach we are able to find bugs which cannot be found if one looks at the C code or the assembly code alone. The paper explains the basic functionality of our tools using two illustrative examples.

1 0