tr-announce September 2006

tr-announce@lists.rwth-aachen.de

1 participants
3 discussions

2006-05: Adjoint Code by Source Transformation with OpenAD/F

by Peter Schneider-Kamp

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.

17 years, 11 months

2006-09: Counterexamples in Probabilistic Model Checking

by Peter Schneider-Kamp

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.

18 years

2006-11: Model Checking Software for Microcontrollers

by Peter Schneider-Kamp

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.

18 years

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce September 2006