Name
Abstract | ||
|---|---|---|
Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1016/j.jsc.2010.06.004 | J. Symb. Comput. |
Keywords | DocType | Volume |
safety checking,Contracts,abstract interpretation,linear equality,Quantifier elimination,logic formula,Specification languages,modular inference,practical applicability,Functional behavior,Inference,subprogram contract,boolean combination,Weakest precondition,different kind,large size,Abstract interpretation,C code,quantifier elimination,important originality | Journal | 45 |
Issue | ISSN | Citations |
11 | Journal of Symbolic Computation | 10 |
PageRank | References | Authors |
0.53 | 27 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yannick Moy | 1 | 69 | 9.25 |
| Claude Marché | 2 | 814 | 47.43 |