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 Informationssysteme 184/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

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

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