Changeset 3441 for Papers


Ignore:
Timestamp:
Feb 17, 2014, 11:17:28 AM (5 years ago)
Author:
mulligan
Message:

Some language/spelling changes in fopara2013.tex up to Section 2. Continuing...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3438 r3441  
    155155reduce non-functional verification to the functional case and exploit the state
    156156of the art in automated high-level verification~\cite{survey}. The techniques
    157 currently used by the Worst Case Execution Time (WCET) community, which perform the analysis on object code,
     157currently used by the Worst Case Execution Time (WCET) community, who perform analyses on object code,
    158158are still available but can now be coupled with an additional source-level
    159159analysis. Where the approach produces precise cost models too complex to reason
     
    169169very lightweight tracking of code changes through compilation. We have studied
    170170how to formally prove the correctness of compilers implementing this technique.
    171 We have implemented such a compiler from C to object binaries for the 8051
     171We have implemented such a compiler from C to object binaries for the MCS-51
    172172micro-controller for predicting execution time and stack space usage,
    173173and verified it in an interactive theorem prover.  As we are targeting
     
    180180program respects these costs by calling automated theorem provers, a
    181181new and innovative technique in the field of cost analysis. Finally,
    182 we have conduct several case studies, including showing that the
     182we have conducted several case studies, including showing that the
    183183plugin can automatically compute and certify the exact reaction time
    184184of Lustre~\cite{lustre} data flow programs compiled into C.
Note: See TracChangeset for help on using the changeset viewer.