Changeset 3459 for Papers/fopara2013


Ignore:
Timestamp:
Feb 21, 2014, 10:35:10 AM (6 years ago)
Author:
mulligan
Message:

small changes to abstract again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3455 r3459  
    9797(`Certified Complexity'). Our main achievement is
    9898the development of a technique for analysing non-functional
    99 properties of programs (time, space) at the source level, with little or no loss of accuracy,
    100 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
    101 the source level---and track precisely---the actual (non-asymptotic)
    102 computational cost of the input program. Untrusted invariant generators and trusted theorem provers
     99properties of programs (time, space) at the source level with little or no loss of accuracy
     100and 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)
     101computational cost of the input program at
     102the source level. Untrusted invariant generators and trusted theorem provers
    103103may then be used to compute and certify the parametric execution time of the
    104104code.
Note: See TracChangeset for help on using the changeset viewer.