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
2014 | |
[3] | Concolic Testing of Concurrent Programs 2014, Unpublished contribution to: CAV Workshop (EC)^2. |
2013 | |
[2] | Solving Constraints for Generational Search Tests and Proofs - 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, 2013. Proceedings (Margus Veanes, Luca Viganò, eds.), volume 7942 of Lecture Notes in Computer Science, pages 197–213, 2013, Springer. |
[1] | Con2colic testing Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013 (Bertrand Meyer, Luciano Baresi, Mira Mezini, eds.), pages 37-47, 2013, ACM. |
Partners
Contact
Address:
Andreas Holzer
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria
Room: | HD 03 13 (how to get there) |
Phone: | +43 (1) 58801 – 184 67 |
Email: | holzer@forsyte.at |
Web: | http://forsyte.at/~holzer/ |