Communications of the ACM
New Mathematical Framework Formalizes Oddball Programming Techniques
Credit: Veer | PixelEmbargo
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. 
, Bethesda, Maryland, USA
No entries found