Sciweavers

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

12

ESOP
2007
Springer

favoriteEmaildiscussreport

85views Programming Languages» more ESOP 2007»

Using History Invariants to Verify Observers

13 years 10 months ago

Using History Invariants to Verify Observers

Download research.microsoft.com

Abstract. This paper contributes a technique that expands the set of object invariants that one can reason about in modular veriﬁcation. The technique uses history invariants, two-state invariants that describe the evolution of data values. The technique enables a ﬂexible new way to specify and verify variations of the observer pattern, including iterators. The paper details history invariants and the new kind of object invariants, and proves a soundness theorem.

K. Rustan M. Leino, Wolfram Schulte

Real-time Traffic

ESOP 2007 | History Invariants | Object Invariants | Programming Languages | Two-state Invariants |

claim paper

Related Content

» Reasoning about Optimistic Concurrency Using a Program Logic for History

» Does the Past Say It All Using History to Predict Change Sets in a CMDB

» Efficient incremental algorithms for dynamic detection of likely invariants

» Verifying linearizability with hindsight

» Verifying Design with Proof Scores

» A FirstOrder Policy Language for HistoryBased Transaction Monitoring

» Verifying properties of wellfounded linked lists

» Observations on the Decidability of Transitions

» On Some Transformation Invariants Under Retiming and Resynthesis

Post Info
More Details (n/a)

Added	07 Jun 2010
Updated	07 Jun 2010
Type	Conference
Year	2007
Where	ESOP
Authors	K. Rustan M. Leino, Wolfram Schulte

Comments (0)