@inproceedings{1e94359bc6914325be1fe1fdbe3a1cd5,
title = "Allowing state changes in specifications",
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.",
author = "Mike Barnett and Naumann, {David A.} and Wolfram Schulte and Qi Sun",
year = "2006",
doi = "10.1007/11766155_23",
language = "English",
isbn = "3540346406",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "321--336",
booktitle = "Emerging Trends in Information and Communication Security - International Conference, ETRICS 2006, Proceedings",
note = "International Conference on Emerging Trends in Information and Communication Security, ETRICS 2006 ; Conference date: 06-06-2006 Through 09-06-2006",
}