Allowing state changes in specifications

Mike Barnett, David A. Naumann, Wolfram Schulte, Qi Sun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

We provide a static analysis (using both dataflow analysis and theorem proving) to allow state changes within specifications. This can be used for specification languages that share the same expression sub-language with an implementation language so that method calls can appear in preconditions, postconditions, and object invariants without violating the soundness of the system.

Original languageEnglish
Title of host publicationEmerging Trends in Information and Communication Security - International Conference, ETRICS 2006, Proceedings
Pages321-336
Number of pages16
DOIs
StatePublished - 2006
EventInternational Conference on Emerging Trends in Information and Communication Security, ETRICS 2006 - Freiburg, Germany
Duration: 6 Jun 20069 Jun 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3995 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Emerging Trends in Information and Communication Security, ETRICS 2006
Country/TerritoryGermany
CityFreiburg
Period6/06/069/06/06

Fingerprint

Dive into the research topics of 'Allowing state changes in specifications'. Together they form a unique fingerprint.

Cite this