Publications

 Graphical user interfaces (GUIs) are a common way to interact with software. To ensure the quality of such software it is important to test the possible interactions with its user interface. GUI testing is a challenging task as they can allow, in general, infinitely many different sequences of interactions with the software. As it is only possible to test a limited amount of possible user interactions, it is crucial for the quality of GUI testing to identify relevant sequences and avoid improper ones. In this paper we propose a model for better GUI testing. Our model is created based on two observations. It is a common case that different user interactions result in the execution of the same code fragments. That is, it is sufficient to test only interactions that execute different code fragments. Our second observation is that user interactions are context-sensitive. That is, the control flow that is taken in a program fragment handling a user interaction depends on the order of some preceding user interactions. We show that these observations are relevant in practice. We present a preliminary implementation that utilizes these observations for test case generation.

We present a new interpolation based abstraction refinement algorithm for software model-checking. The refinement step uses interpolants computed from an error path to split the abstract states on this path. It incorporates the ideas of slicing abstraction and large block encoding. We run our model-checker on several benchmarks and show empirically that the presented algorithm terminates more often with a result than existing model checking techniques.

Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Integration aims at supporting collaborative healthcare workflows (CHWF) for improvement in sharing healthcare information and resources, efficiency of services and patients safety. CHWF are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modelling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We also follow the idea of UML of some visualized models, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work.

Graphical user interfaces (GUIs) are a common way to interact with software. To ensure the quality of such software it is important to test the possible interactions with its user interface. GUI testing is a challenging task as they can allow, in general, infinitely many different sequences of interactions with the software. As it is only possible to test a limited amount of possible user interactions, it is crucial for the quality of GUI testing to identify relevant sequences and avoid improper ones. In this paper we propose a model for better GUI testing. Our model is created based on two observations. It is a common case that different user interactions result in the execution of the same code fragments. That is, it is sufficient to test only interactions that execute different code fragments. Our second observation is that user interactions are contextsensitive. That is, the control flow that is taken in a program fragment handling a user interaction depends on the order of some preceding user interactions. We show that these observations are relevant in practice. We present a preliminary implementation that utilizes these observations for test case generation.

 Localizing the cause of an error in an error trace is one of the most time-consuming aspects of debugging. We develop a novel technique to automate this task. For this purpose, we introduce the concept of "error invariants". An error invariant for a position in an error trace is a formula over program variables that over-approximates the reachable states at the given position while only capturing states that will still produce the error, if execution of the trace is continued from that position. Error invariants can be used for slicing error traces and for obtaining concise error explanations. We present an algorithm that computes error invariants from Craig interpolants, which we construct from proofs of unsatisfiability of formulas that explain why an error trace violates a particular correctness assertion. We demonstrate the effectiveness of our algorithm by using it to localize faults in real-world programs.

 A piece of code in a computer program is infeasible if it cannot be part of any normally-terminating execution of the program. We develop an algorithm for the automatic detection of all infeasible code in a program. We first translate the task of determining all infeasible code into the problem of finding all statements that can be covered by a feasible path. We prove that in order to identify all coverable statements, it is sufficient to find all coverable statements within a certain minimal subset. For this, our algorithm repeatedly queries an oracle, asking for the infeasibility of specific sets of control-flow paths. 

 We present Joogie, a tool that detects infeasible code in Java programs. Infeasible code is code that does not occur on feasible control-flow paths and thus has no feasible execution. Infeasible code comprises many errors detected by static analysis in modern IDEs such as guaranteed null-pointer dereference or unreachable code. Unlike existing techniques, Joogie identifies infeasible code by proving that a particular statement cannot occur on a terminating execution using techniques from static verification. Thus, Joogie is able to detect infeasible code which is overlooked by existing tools. Joogie works fully automatic, it does not require user- provided specifications and (almost) never produces false warnings.

 This chapter gives an overview of the recent advances in GUItesting.Considering the increasing popularity and fast software development cycles (e.g.,desktop and mobile applications), GUI testing gains more importance as it allows us to verify the behavior of a system from the user’s perspective.Thus, it can quickly uncover relevant bugs, which a user could face. Traditional capture-replay GUI testing approaches do not meet the demands of developers anymore. Therefore, there is an increasing research activity in model-based GUI testing, where the user interaction behavior is simulated using a graph-based model.In the following, we outline different graphical notations to describe feasible user interactions, and methods to generate and execute test cases from these models. We discuss the benefits and limitations of the state-of-the-art in GUI testing research and give a brief outlook about new trends and possibilities to improve the GUI testing automation.

consuming part in program debugging. Fault localization techniques can help to automate this task. Particularly promising are static proof-based techniques that rely on an encoding of error traces into trace formulas. By identifying irrelevant portions of the trace formula, the possible causes of the error can be isolated. One limitation of these approaches is that they do not take into account the control flow of the program and therefore miss common causes of errors, such as faulty branching conditions. This limitation is inherent to the way the error traces are encoded. In this paper, we present a new flow-sensitive encoding of error traces into trace formulas. The new encoding enables proof-based techniques to identify irrelevant conditional choices in an error trace and to include a justification for the truth value of branching conditions that are relevant for the localized cause of an error. We apply our new encoding to the fault localization technique based on error invariants and show that it produces more meaningful error explanations than previous approaches.

Recently, software verification is being used to prove the presence of contradictions in source code and thus reveal potential weaknesses in the code or provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source code to logic can be very simple and thus easy to solve by automated theorem provers. In this paper, we present a translation of Java into logic that is suitable for proving the presence of contradictions in code. We show that the translation, which is based on the Jimple language, can be used to analyze real-world programs, and discuss some issues that arise from differences between Java code and its bytecode