@conference {107,
	title = {An Approach to High-Level Behavioral Program Documentation Allowing Lightweight Verification},
	booktitle = {Proceedings of the 14th IEEE International Conference on Program Comprehension (ICPC06)},
	year = {2006},
	abstract = {<p>Typically, multiple developers are involved in the various stages of the software development and maintenance process. To ensure an optimal transfer of knowledge between these different peers, a reliable human-readable model of the dynamics of a software artefact is needed. Once these models become machine-verifiable, they can be used throughout an application{\textquoteright}s lifetime to check whether the documented behavioral properties continue to hold as the application evolves. Unfortunately, most existing modeling media are inadequate to express human-readable behavioral models which are at the same time machine-verifiable. We therefore propose a declarative platform wherein behavioral program models can be expressed in terms of userdefined high-level concepts and be automatically verified against an application{\textquoteright}s actual behavior. We demonstrate our approach by using it to both document and verify an interpreter for a garbage-collected programming language.</p>},
	keywords = {aspect-oriented programming, behave, documentation, dynamic analysis, logic meta programming, program comprenhension, temporal logic, temporal logic programming, testing, verification},
	isbn = {0-7695-2601-2},
	author = {Coen De Roover and Michiels, Isabel and Kris Gybels and Kris Gybels and Theo D{\textquoteright}Hondt}
}
