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

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

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

Full news archive