The integer relations computed using the code, the points-to information and contract: A report on the error in line [5] of main; the inequalities before execution of line [5] and a counter example: Results are the results of running CSSV on extreme string manipulation procedures. As can be seen the outcome is very good, detects errors with low false alarm rate. But the consumed time and space resources are very high, increasing with procedure size. Time can be reduced by simplifying the constrains, as in Microsoft SAL which uses only {0,1} coefficients in the conditions. In common cases where less complicated string manipulation is performed, the results are even better. Also one should have in mind that due to the fact that each procedure is analyzed alone, the memory consumption of the whole analysis is mostly influenced by the largest procedure. Compile-Time Verification of Properties of Heap Intensive Programs by Mooly Sagiv, Thomas Reps, Reinhard Wilhem. For more information you can look at: Introduction to Shape Analysis The intention of this collaborative work is to verify through static analysis a code that makes intensive use of the heap. The TVLA system was developed at Tel Aviv University. It produces static analysis of the code using set of rules given by the programmer. It handles specially issues and deals with dynamic allocations and pointers. In fact, TVLA does Shape Analysis of the code.
The integer relations computed using the code, the points-to information and contract: A report on the error in line [5] of main; the inequalities before execution of line [5] and a counter example: Results are the results of running CSSV on extreme string manipulation procedures. As can be seen the outcome is very good, detects errors with low false alarm rate. But the consumed time and space resources are very high, increasing with procedure size. Time can be reduced by simplifying the constrains, as in Microsoft SAL which uses only {0,1} coefficients in the conditions. In common cases where less complicated string manipulation is performed, the results are even better. Also one should have in mind that due to the fact that each procedure is analyzed alone, the memory consumption of the whole analysis is mostly influenced by the largest procedure. Compile-Time Verification of Properties of Heap Intensive Programs by Mooly Sagiv, Thomas Reps, Reinhard Wilhem. For more information you can look at: Introduction to Shape Analysis The intention of this collaborative work is to verify through static analysis a code that makes intensive use of the heap. The TVLA system was developed at Tel Aviv University. It produces static analysis of the code using set of rules given by the programmer. It handles specially issues and deals with dynamic allocations and pointers. In fact, TVLA does Shape Analysis of the code.
cssv_scribe.docx