Changeset 3459

Timestamp:

Feb 21, 2014, 10:35:10 AM (6 years ago)

Author:

mulligan

Message:

small changes to abstract again

File:

• Papers/fopara2013/fopara13.tex (modified) (1 diff)

Papers/fopara2013/fopara13.tex

@@ -97 +97 @@
 (`Certified Complexity'). Our main achievement is
 the development of a technique for analysing non-functional
-properties of programs (time, space) at the source level, with little or no loss of accuracy,
-and with a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose at
-the source level---and track precisely---the actual (non-asymptotic)
-computational cost of the input program. Untrusted invariant generators and trusted theorem provers
+properties of programs (time, space) at the source level with little or no loss of accuracy
+and a small trusted code base. We developed a certified compiler that translates C source code to object code, producing a copy of the source code embellished with cost annotations as an additional side-effect. These annotations expose and track precisely the actual (non-asymptotic)
+computational cost of the input program at
+the source level. Untrusted invariant generators and trusted theorem provers
 may then be used to compute and certify the parametric execution time of the
 code.