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).
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