Changeset 3459
- Timestamp:
- Feb 21, 2014, 10:35:10 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3455 r3459 97 97 (`Certified Complexity'). Our main achievement is 98 98 the 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 at101 the source level---and track precisely---the actual (non-asymptotic) 102 computational cost of the input program. Untrusted invariant generators and trusted theorem provers99 properties of programs (time, space) at the source level with little or no loss of accuracy 100 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) 101 computational cost of the input program at 102 the source level. Untrusted invariant generators and trusted theorem provers 103 103 may then be used to compute and certify the parametric execution time of the 104 104 code.
Note: See TracChangeset
for help on using the changeset viewer.