Abstract | ||
---|---|---|
We apply linear relation analysis [CH78, HPR97] to the verification of declarative synchronous programs [Hal98]. In this approach, state partitioning plays an important role: on one hand the precision of the results highly depends on the fineness of the partitioning; on the other hand, a too much detailed partitioning may result in an exponential explosion of the analysis. In this paper, we propose to dynamically select a suitable partitioning according to the property to be proved. |
Year | DOI | Venue |
---|---|---|
1999 | 10.1007/3-540-48294-6_3 | SAS |
Keywords | Field | DocType |
dynamic partitioning,important role,linear relation analysis,state partitioning,numerical properties,suitable partitioning,exponential explosion,declarative synchronous program,detailed partitioning | Dynamic programming,Exponential function,Partial evaluation,Computer science,Abstract interpretation,Algorithm,Real-time computing,Linear programming,Program analysis,Boolean data type,Formal verification | Conference |
Volume | ISSN | ISBN |
1694 | 0302-9743 | 3-540-66459-9 |
Citations | PageRank | References |
39 | 2.17 | 10 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Bertrand Jeannet | 1 | 641 | 29.06 |
Nicolas Halbwachs | 2 | 3957 | 426.43 |
Pascal Raymond | 3 | 567 | 53.53 |