Changeset 3612

Ignore:
Timestamp:
Mar 6, 2017, 2:26:45 PM (3 years ago)
Message:

more work on conclusions prior to meeting student

File:
1 edited

Legend:

Unmodified
 r3611 %   Future work In many application domains the intensional properties of programs---asymptotic or concrete time and space usage, for example---are an important factor in overall correctness. Soft real time' applications, and cryptography libraries, are two important classes of programs fitting this pattern. Worst Case Execution Time (WCET) tools currently represent the state of the art in determining accurate concrete resource bounds for programs. In many application domains the intensional properties of programs---time and space usage, for example---are an important factor in the specification of a program, and therefore overall program correctness. Here, intensional' properties can be analysed \emph{asymptotically}, or \emph{concretely}, with the latter computing resource bounds in terms of clock cycles, seconds, bits transmitted, or other concrete resource measures, for a program execution. Soft real time' applications and cryptography libraries are two important classes of programs fitting this pattern. Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs. These tools however possess a number of disadvantages: for instance, they require that the analysis be performed on machine code produced by a compiler, where all high-level program structure has been compiled away', rather than permitting an analysis at the source-code level. The CerCo verified compiler and associated toolchain has demonstrated that it is possible to perform static time and space analysis at the source level without losing accuracy, reducing the trusted code base and reconciling the study of functional and non-functional properties of programs.