Changeset 3441

Timestamp:

Feb 17, 2014, 11:17:28 AM (7 years ago)

Author:

mulligan

Message:

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

File:

• Papers/fopara2013/fopara13.tex (modified) (3 diffs)

Papers/fopara2013/fopara13.tex

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