Paper Info

• Paper Name
• Author
• Conference or Journal, Year

Problem

Here, you want to use an example to describe the problem the paper attempts to solve. Also use the example (if possible) to show why the problem is interesting and why it is difficult for existing works. For example,

The paper attempts to find inputs reaching difficult program locations. Consider the following code snippet:

int foo(x, y){
  if (2**x == 64 && y+3 == 123){
     //L
     assert(0);
  } 
}

In the above code, the goal is to find whether we can violate the assertion, i.e., we can reach line L. If we can, then that means the program has a bug because it violates an assertion.

Existing works such as fuzzing are not adequate because it is difficult to fuzz the exact values of x and y that allows the program to go to L.

The approach

Here you want to talk about the proposed approach using examples. Try to reuse examples you have in the Problem section above if possible. First, give a high-level description of the approach. Then use the example to illustrate. For example,

The paper describes a technique called symbolic execution to find inputs reaching difficult locations, e.g., those representing assertion violations. The technique assigns symbolic values to program inputs and "execute" the program using these symbolic inputs. By using symbolic values, the program execution path is represented by logical constraints over symbolic values. That is, every path leading to some program location is captured by a path condition. Using a constraint solver such as SAT/SMT solver allows us to compute concrete input values allowing the program to reach the desired program location.

Using the above example, we assign the symbolic values A and B for the inputs x,y, respective. Then we execute the program using these values and obtain the path condition 2**A == 64 and B+3 == 123, which can then be solved by an SMT solver to obtain A==8 and B==120, which say that the program will reach location L on input x==8 and y==120.

The Algorithm

Here, give the detailed algorithm of the approached

Limitations

Here, describe the main limitations of the approach. Give examples whenever possible. For example

The three main limitations of symbolic executions are

• Space Explosion: symbolic execution can produce an exponentially large number of paths, e.g., when the program has loops or lots of (sequential) conditional statements.
• Third-party Library or Unknown code: we cannot generate a path condition representing the semantics of 3rd-parth library or unknown code.
• Limitations of Constraint Solving: current constraint solver might not be able to solve path conditions extracted from difficult or complex code (e.g., dealing with nonlinear arithmetics).