In concolic testing, what does "concrete execution" mean?

Question

I came across the terms "concrete & symbolic execution" when I was going through the concept of concolic testing. (The article mentioned there, "CUTE: A concolic unit testing engine for C", uses that term in its abstract section.)

"The approach used builds on previous work combining symbolic and concrete execution, and more specifically, using such a combination to generate test inputs to explore all feasible execution paths."

Can anyone please confirm what "concrete execution" means? In spite of my search, I could not find any direct citations / explicit statements.

From what I have understood, "concrete execution" means "the execution of a program with actual input values unlike symbolic execution, which assumes symbolic values to variables, inputs etc.". If I am wrong, please correct me (if possible with a small example).

Epiphenomenalism

Answer 1

Concolic execution is a mix between CONCrete execution and symbOLIC execution, with the purpose of feasibility.

Symbolic execution allows us to execute a program through all possible execution paths, thus achieving all possible path conditions (path condition = the set of logical constraints that takes us to a specific point in the execution). The problem is that, except for micro benchmarks, the cost of executing a program through all possible execution paths is exponentially large, thus prohibitive.

On the other hand, if we provide the symbolic execution with concrete values, you can guide it through a specific execution path (without traversing all of them) and achieve the respective path condition. This is feasible.

I hope this answers your question

Analytic

Answer 2

In the context you've mentioned, I'm pretty sure that "concrete execution" refers to actually running the program on specific inputs and seeing what happens. The "concolic testing" article you've linked to suggests a hybrid approach between testing on specific inputs (concrete execution, which is complete but unsound) and symbolic testing (symbolic execution, which sound but incomplete).

Hope this helps!

Impenitent

Hi, I was exactly looking for this answer and I infer the same from that article. Thanks for confirming. Also could I know if this term is standardized or does it vary in every different context or is that this term is just used by the author in the article as a part of english language. (as mentioned by other commentators on this post ) ? I feel this term has standard meaning by the way it is used but again no confirmation/not sure about this. – Epiphenomenalism

@SuhasChikkanna I'm not sure. I've never seen it before, but I also don't do a lot of work on program verification. – Impenitent

Nevertheless, I shall continue to search for the answer and will follow up this post for sometime. It is a very kind answer from you, which I feel is genuinely right. Please give me sometime before I confirm it, Thanks so much once again!!. – Epiphenomenalism

Could you explain why you said concrete execution is unsound? I don't quite understand. What purpose did you mean it is unsound for? – Freeloader

@Mehrdad I was using the term in the context of formal logic. Soundness means that if the tests report that the program is correct, then the program actually is correct, and completeness means that if the program is correct, the tests will report that it's correct. Concrete execution is complete (if the program is valid, it will pass the test) but unsound (a wrong program may still pass all the tests in a test suite). – Impenitent

@templatetypedef: ohh, yeah I know what soundness means in formal logic but I wasn't thinking about it the right way. Okay thanks! – Freeloader