ConCREST

ConCREST is a concolic testing tool for multi-threaded C programs. It is an extension of the concolic testing tool CREST. A concolic testing tool usually consists of a concolic execution engine, a path exploration strategy, and a realizability checker:

Given an input vector, the concolic execution engine performs a concrete and symbolic execution of the program and thereby obtains an execution trace that contains a sequence of constraints on symbolic inputs (i.e. branch conditions encountered during execution). The path exploration strategy selects one of these branch conditions and negates it in order to guide the execution along a different path. Then, the realizability checker uses an SMT solver to try to generate a new input vector that would satisfy the new path constraint.

While for a deterministic sequential program each input vector specifies a single path in the program, the behaviour of a concurrent program, however, is not only influenced by the input vector, but also by the interleaving of execution of threads. Each interleaving determines a pattern of interferences among the threads. An interference happens when a thread reads a value that is generated by another thread. An interference could substantially change the course of the local computation of a thread, because the value generated by another thread may not be producible locally. Therefore, the local behaviour (e.g. an assertion violation) followed by this interference may never surface by pure sequential testing.

ConCREST uses the concept of interference scenario to represent a set of interferences among threads. Conceptually, interference scenarios are the essential information that define the important scheduling constraints for a concurrent program run; in other words, all runs with the same interference scenario are behaviourally equivalent under the same input values. The constraint system for sequential concolic execution is also modified to model interferences as well. ConCREST is then able to produce schedules, in addition to input vectors, for concurrent programs. ConCREST has an interference exploration strategy that systematically navigates the space of all interference scenarios. Find more details in “Con2colic Testing”.

People

Azadeh Farzan
University of Toronto

Andreas Holzer
TU Wien

Niloofar Razavi
University of Toronto

Helmut Veith
TU Wien

Downloads

FSE’13 Presentation

(21. August 2013)

Publications

Partners

Contact

Address:
Andreas Holzer
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria