Changeset 3612


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

more work on conclusions prior to meeting student

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.tex

    r3611 r3612  
    651651%   Future work
    652652
    653 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.
    654 `Soft real time' applications, and cryptography libraries, are two important classes of programs fitting this pattern.
    655 
    656 Worst Case Execution Time (WCET) tools currently represent the state of the art in determining accurate concrete resource bounds for programs.
     653In 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.
     654Here, `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.
     655`Soft real time' applications and cryptography libraries are two important classes of programs fitting this pattern.
     656
     657Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs.
     658These 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.
    657659
    658660The 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.
Note: See TracChangeset for help on using the changeset viewer.