We present a novel assertional proof method for reasoning about global invariant properties of active objects in the context of the Abstract Behavioral Specification (ABS) language. The main result of this paper is a formal justification of the proof method which establishes both its soundness and completeness with respect to a formally defined operational trace semantics.
|Title of host publication||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Subtitle of host publication||Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday|
|Editors||Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen|
|Place of Publication||Cham|
|Number of pages||20|
|Publication status||Published - 4 Jul 2022|
|Series||Lecture Notes in Computer Science|