Invited Speaker

Doron A. Peled

Professor
University of Texas at Austin, USA

Web page,


Tracing the executions of concurrent programs

Abstract
Concurrent programs are highly prone to errors, while analyzing and debugging them is known to be a very difficult task. Applying automatic and manual verification and validation techniques to such programs is a nontrivial challenge. We describe here two techniques, which help the user to interactively analyze and debug concurrent programs.

The first method is the symbolic execution of traces of the program. We compile a visual representation, in the form of a flow graph of the concurrent processes, with one window for each concurrent process. The user is allowed to select an interleaved execution path. The system automatically calculates the weakest condition for executing the path, and tries to simplify it as much as possible. Such a path is not limited to start from the beginning of the program, nor do the variables need to be fully initialized. By selecting such paths, obtaining the conditions to execute them, and interactively changing them (e.g., by changing the order of interleaving concurrent actions, or providing a different suffix), we can obtain a better understanding of the program, and perform some simple verification tasks. This technique is implemented by the PET tool.

Another method employed by this tool is based on the application of temporal logic, as a way of assisting the debugging of a concurrent or a sequential program. Temporal logic over finite sequences is used here as a constraint formalism that is used to control the way we step through the states of the debugged system. Using such temporal specification and various search strategies, we are able to traverse the executions of the system and obtain important intuitive information about its behaviors.

In this talk the tool and techniques will be described and demonstrated.


Bio
Doron has all his degrees from the Technion, Israel Institute of Technology. Graduating his DSc in 1991, he has spent a postdoc year at the University of Warwick, UK. Doron is working in the area of formal methods, and is interested in deductive verification, model checking and testing, as well as combining these methods, and developing methodologies to improve the reliability of software. He is a coauthor of the book "model checking" and the author of the recent book "software reliability methods". Doron has worked in Bell Laboratories from 1992 to 2001 as a member of technical staff, and then moved to the University of Texas at Austin. Starting September 2002, Doron is joining again the University of Warwick as a professor of software engineering in the department of Computer Science.