Name
Abstract | ||
|---|---|---|
Recently, software verification is being used to prove the presence of contradictions in source code, and thus detect potential weaknesses in the code or provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source code to logic can be very simple and thus easy to solve by automated theorem provers. In this paper, we present a translation of Java into logic that is suitable for proving the presence of contradictions in code. We show that the translation, which is based on the Jimple language, can be used to analyze real-world programs, and discuss some issues that arise from differences between Java code and its bytecode. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2487568.2487570 | SOAP@PLDI |
Keywords | Field | DocType |
compiler optimization,real-world program,potential weakness,jimple language,automated theorem provers,java code,correctness property,source code,software verification,theorem prover | Unreachable code,Dead code elimination,Object code,Threaded code,Programming language,Computer science,Source code,Code generation,Bytecode,Dead code | Conference |
Citations | PageRank | References |
5 | 0.47 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stephan Arlt | 1 | 69 | 7.01 |
| Philipp Rümmer | 2 | 655 | 43.87 |
| Martin Schäf | 3 | 135 | 14.71 |