Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Felix Pauck, M.Sc.

Address: Felix Pauck
Paderborn University
Faculty of Electrical Engineering, Computer Science and Mathematics
Warburger Str. 100
D-33098 Paderborn, Germany
Office: O4.128
Phone: +49 (0) 5251-60-1765
Fax:  +49 (0) 5251-60-3993 
Email: fpauck(at)
Secretary: Elisabeth Schlatt
Phone: +49 (0) 5251-60-3764
Email: schlatt(at)
Office: O4.125


SS 2019 PG: BANANA Organization
WS 2018/19 Modellierung Organization, Tutorial
SS 2018 Proseminar: Android App Analyse Organization
WS 2017/18 Software Analysis (in English) Tutorial, Laboratory


Open list in Research Information System


Do Android taint analysis tools keep their promises?

F. Pauck, E. Bodden, H. Wehrheim, in: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018, ACM Press, 2018


Validity of Software Verification Results on Approximate Hardware

T. Isenberg, M. Jakobs, F. Pauck, H. Wehrheim, IEEE Embedded Systems Letters (2018), pp. 22-25

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out “approximately correct” calculations. This provides a major challenge for software quality assurance: programs successfully verified to be correct might be erroneous on approximate hardware. In this letter, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which—when met by the AC hardware—guarantees the verification result to carry over to AC. On the practical side, we furthermore: 1) show how to extract tolerances from verification runs employing predicate abstraction as verification technology and 2) show how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.

Do Android Taint Analysis Tools Keep their Promises?

F. Pauck, E. Bodden, H. Wehrheim, in: arXiv:1804.02903, 2018



PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)

M. Jakobs, M. Töws, F. Pauck, in: Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems, 2016

We present PAndA2, an extendable, static analysis tool for Android apps which examines permission related security threats like overprivilege, existence of permission redelegation and permission flows. PAndA2 comes along with a textual and graphical visualization of the analysis result and even supports the comparison of analysis results for different android app versions.


Open list in Research Information System

Research Interest

Cooperative Android App Analysis

The University for the Information Society