Sign In

Communications of the ACM

ACM TechNews

New Mathematical Framework Formalizes Oddball Programming Techniques


Antivirus era

Massachusetts Institute of Technology (MIT) researchers have developed a mathematical framework that enables developers to reason rigorously about sloppy computation, providing mathematical guarantees that if a program behaves as intended, so will a fast-but-inaccurate modification of it.

MIT's Michael Carbin describes the framework as a type of formal verification, and says the performance gains promised by techniques such as loop perforation will give programmers confidence to try formal verification techniques.

"We're identifying all these opportunities where programmers can get much bigger benefits than they could before if they're willing to do a little verification," Carbin says.

The framework forces programmers to specify "acceptability properties" for each procedure in a program and by reference to the normal execution of the program. The framework also enables developers who have already verified their programs to reuse a lot of their previous reasoning. Carbin says the researchers are now working on a system that enables programmers to simply state acceptability properties.

From MIT News 
View Full Article

Abstracts Copyright © 2012 Information Inc. External Link, Bethesda, Maryland, USA


 

No entries found