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

Azadeh Farzan
University of Toronto

Niloofar Razavi

Niloofar Razavi
University of Toronto

Downloads

FSE’13 Presentation (21. August 2013)

Publications

2014
[3]Concolic Testing of Concurrent Programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
2014, Unpublished contribution to: CAV Workshop (EC)^2.
[bibtex]
2013
[2] Solving Constraints for Generational Search
Daniel Pötzl, Andreas Holzer
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.
[bibtex] [pdf] [doi]
[1] Con2colic testing
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
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.
[bibtex] [pdf] [doi]

Partners

Logo ARiSE University of Toronto Logo TU Wien

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: ta.etysrofnull@rezloh
Web: http://forsyte.at/~holzer/

Latest News

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Full news archive