Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

21

TAP
2009
Springer

favoriteEmaildiscussreport

127views Hardware» more TAP 2009»

Could We Have Chosen a Better Loop Invariant or Method Contract?

14 years 5 months ago

Could We Have Chosen a Better Loop Invariant or Method Contract?

Download www.uni-koblenz.de

The method contract and loop invariant rules (contract rules) are an important software veriﬁcation technique for handling method invocations and loops. However, if a veriﬁcation condition resulting from using a contract rule turns out to be falsiﬁable, then the user does not know if she could have chosen a stronger contract to verify the program or if the program is not veriﬁable due to a software bug. We approach this problem and present a novel technique that uniﬁes veriﬁcation and software bug detection.

Christoph Gladisch

Real-time Traffic

Contract Rule | Hardware | Method Contract | Software Veriﬁcation Technique | TAP 2009 |

claim paper

Related Content

» ContractBased Data Structure Repair Using Alloy

» On integration of eventbased estimation and robust MPC in a feedback loop

» Closing the loop in webpage understanding

» Intramodule Inference

» Experiments with Clustering as a Software Remodularization Method

» Differential static analysis opportunities applications and challenges

» Using persistent homology to recover spatial information from encounter traces

Post Info
More Details (n/a)

Added	27 May 2010
Updated	27 May 2010
Type	Conference
Year	2009
Where	TAP
Authors	Christoph Gladisch

Comments (0)