Roland Kindermann

Dipl.-Inform., Researcher

Office:

Room T-B349, Computer Science Building,
Konemiehentie 2, Otaniemi campus area, Espoo

Postal Address:

Aalto University, School of Science and Technology,
Department of Information and Computer Science,
P.O. Box 15400, FI-00076 Aalto, Finland

Telephone:

+358 9 470 22895

Email:

roland(dot)kindermann(at)aalto(dot)fi

About me

Since 2009, I have been a doctoral student and researcher under the supervision of Prof. Dr. Ilkka Niemelä at Aalto University (Helsinki University of Technology before Aalto University existed), currently instructed by Dr. Tommi Junttila.

I am interested in symbolic verification methods with a focus on sybmolic methods for timed systems.

Publications

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä. Bounded Model Checking of an MITL Fragment for Timed Automata. ACSD 2013, IEEE 2013, to appear.

Roland Kindermann, Tommi Junttila and Ilkka Niemelä. SMT-based Induction Methods for Timed Systems. FORMATS 2012, Springer 2012.

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. FMOODS/FORTE 2012, pages 84-100, Springer 2012.

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä. Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks. ACSD 2011, pages 185-194, IEEE 2011.

Kari Kähkönen, Roland Kindermann, Keijo Heljanko, Ilkka Niemelä. Experimental Comparison of Concolic and Random Testing for Java Card Applets. SPIN 2010, pages 22-39, Springer 2010.

Roland Kindermann. Testing a Java Card applet using the LIME Interface Test Bench: A case study. Technical Report TKK-ICS-R18, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, September 2009.

Roland Kindermann. Static Detection of Buffer Overflows in Executables. Diploma thesis ("Diplomarbeit"), 2008.

Software

Aalto Timed Model Checker (ATMOC) Version 1.0 -- Implementation of k-Induction and a timed variant of the IC3 algorithm. For details refer to the FORMATS 2012 paper. Published under GPL license.

Diesel generator models, used in the ACSD 2011, the FMOODS/FORTE 2012 and the FORMATS 2012 paper. Note that these models are not published under the GPL license.

MITL_0,∞ BMC tool, implementation fo the ACSD 2013 paper. Published under GPL license.