Reasoning About Active Objects: A Sound and Complete Assertional Proof Method

Frank S. de Boer, Stijn de Gouw*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationLecture 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
EditorsWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen
Place of PublicationCham
PublisherSpringer
Pages173-192
Number of pages20
Volume13360
Edition1
ISBN (Electronic)9783031081668
ISBN (Print)9783031081651
DOIs
Publication statusPublished - 4 Jul 2022

Publication series

SeriesLecture Notes in Computer Science
Volume13360
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Reasoning About Active Objects: A Sound and Complete Assertional Proof Method'. Together they form a unique fingerprint.

Cite this