Changeset 3620


Ignore:
Timestamp:
Mar 6, 2017, 4:06:33 PM (8 months ago)
Author:
boender
Message:

Rewrote introduction to sound less futuristic/defensive

File:
1 edited

Legend:

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

    r3619 r3620  
    4444\end{itemize*}
    4545
    46 \paragraph{Vision and approach.}
     46\paragraph{Vision.}
    4747We want to reconcile functional and non-functional analysis: to share
    4848information between them and perform both at the same time on high-level source
     
    7878lightweight tracking of code changes through the compilation pipeline.
    7979
    80 We have studied how to formally prove the correctness of compilers implementing
    81 this technique, and have implemented such a compiler from C to object binaries
    82 for the 8051 microcontroller that predicts execution time and stack space
    83 usage, verifying it in an interactive theorem prover. As we are targeting an
    84 embedded microcontroller we do not consider dynamic memory allocation.
     80We have implemented a compiler from C to object binaries for the 8051
     81microcontroller which uses this technique. The compiler predicts
     82execution time and stack space usage. We have also verified the compile using
     83an interactive theorem prover. As we are targeting an embedded microcontroller
     84we have not considered dynamic memory allocation.
    8585
    8686To demonstrate source-level verification of costs we have implemented a Frama-C
Note: See TracChangeset for help on using the changeset viewer.