Showing 1–10 of 10 results for author: de Boer, F S

Dynamic Separation Logic

Authors: Frank S. de Boer, Hans-Dieter A. Hiep, Stijn de Gouw

Abstract: This paper introduces a dynamic logic extension of separation logic. The assertion language of separation logic is extended with modalities for the five types of the basic instructions of separation logic: simple assignment, look-up, mutation, allocation, and de-allocation. The main novelty of the resulting dynamic logic is that it allows to combine different approaches to resolving these modaliti… ▽ More This paper introduces a dynamic logic extension of separation logic. The assertion language of separation logic is extended with modalities for the five types of the basic instructions of separation logic: simple assignment, look-up, mutation, allocation, and de-allocation. The main novelty of the resulting dynamic logic is that it allows to combine different approaches to resolving these modalities. One such approach is based on the standard weakest precondition calculus of separation logic. The other approach introduced in this paper provides a novel alternative formalization in the proposed dynamic logic extension of separation logic. The soundness and completeness of this axiomatization has been formalized in the Coq theorem prover. △ Less

Submitted 24 January, 2025; v1 submitted 16 September, 2023; originally announced September 2023.

Journal ref: Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX (November 23, 2023) entics:12297

Proving Correctness of Parallel Implementations of Transition System Specifications

Authors: Frank S. de Boer, Einar Broch Johnsen, Violet Ka I Pun, Silvia Lizeth Tapia Tarifa

Abstract: The overall problem addressed in this paper is the long-standing problem of program correctness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent)… ▽ More The overall problem addressed in this paper is the long-standing problem of program correctness, and in particular programs that describe systems of parallel executing processes. We propose a new method for proving correctness of parallel implementations of high-level transition system specifications. The implementation language underlying the method is based on the model of active (or concurrent) objects. The method defines correctness in terms of a simulation relation between the transition system which specifies the program semantics and the transition system that is described by the correctness specification. The simulation relation itself abstracts from the fine-grained interleaving of parallel processes by exploiting a global confluence property of the particular model of active objects considered in this paper. As a proof-of-concept we apply our method to the correctness of a parallel simulator of multicore memory systems. △ Less

Submitted 25 January, 2023; originally announced February 2023.

Verifying OpenJDK's LinkedList using KeY

Authors: Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko van Eekelen, Stijn de Gouw

Abstract: As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework. Keywords: Java, standard library, deductive verification, KeY, Java Modeling Language, case study, bug As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework. Keywords: Java, standard library, deductive verification, KeY, Java Modeling Language, case study, bug △ Less

Submitted 11 November, 2019; originally announced November 2019.

Comments: 16 pages, 9 pages appendix

Reasoning about call-by-value: a missing result in the history of Hoare's logic

Authors: Krzysztof R. Apt, Frank S. de Boer

Abstract: We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no… ▽ More We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature. △ Less

Submitted 13 September, 2019; originally announced September 2019.

Comments: 28 pages

Analysis of SLA Compliance in the Cloud -- An Automated, Model-based Approach

Authors: Frank S. de Boer, Elena Giachino, Stijn de Gouw, Reiner Hähnle, Einar Broch Johnsen, Cosimo Laneve, Ka I Pun, Gianluigi Zavattaro

Abstract: Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study.… ▽ More Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study. The approach is based on formal models combined with static analysis tools and generated runtime monitors. As such, it fits well within a methodology combining software development with information technology operations (DevOps). △ Less

Submitted 27 August, 2019; originally announced August 2019.

Comments: In Proceedings VORTEX 2018, arXiv:1908.09302

Journal ref: EPTCS 302, 2019, pp. 1-15

Multi-Threaded Actors

Authors: Keyvan Azadbakht, Frank S. de Boer, Vlad Serbanescu

Abstract: In this paper we introduce a new programming model of multi-threaded actors which feature the parallel processing of their messages. In this model an actor consists of a group of active objects which share a message queue. We provide a formal operational semantics, and a description of a Java-based implementation for the basic programming abstractions describing multi-threaded actors. Finally, we… ▽ More In this paper we introduce a new programming model of multi-threaded actors which feature the parallel processing of their messages. In this model an actor consists of a group of active objects which share a message queue. We provide a formal operational semantics, and a description of a Java-based implementation for the basic programming abstractions describing multi-threaded actors. Finally, we evaluate our proposal by means of an example application. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: In Proceedings ICE 2016, arXiv:1608.03131

Journal ref: EPTCS 223, 2016, pp. 51-66

Verification of Object-Oriented Programs: a Transformational Approach

Authors: Krzysztof R. Apt, Frank S. de Boer, Ernst-Ruediger Olderog, Stijn de Gouw

Abstract: We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulti… ▽ More We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters. △ Less

Submitted 8 November, 2011; v1 submitted 26 April, 2010; originally announced April 2010.

Comments: 49 pages. To appear in Journal of Computer and System Sciences. Stijn de Gouw is now a new author

ACM Class: F.3.1

Modular Verification of Recursive Programs

Authors: Krzysztof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog

Abstract: We argue that verification of recursive programs by means of the assertional method of C.A.R. Hoare can be conceptually simplified using a modular reasoning. In this approach some properties of the program are established first and subsequently used to establish other program properties. We illustrate this approach by providing a modular correctness proof of the Quicksort program. We argue that verification of recursive programs by means of the assertional method of C.A.R. Hoare can be conceptually simplified using a modular reasoning. In this approach some properties of the program are established first and subsequently used to establish other program properties. We illustrate this approach by providing a modular correctness proof of the Quicksort program. △ Less

Submitted 24 July, 2009; originally announced July 2009.

Comments: 21 pages. appeared in: Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday. Lecture Notes in Computer Science 5533 Springer 2009

ACM Class: F.3.1

Proving correctness of Timed Concurrent Constraint Programs

Authors: F. S. de Boer, M. Gabbrielli, M. C. Meo

Abstract: A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior… ▽ More A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs. △ Less

Submitted 28 August, 2002; originally announced August 2002.

ACM Class: F.3.1; D.3.1; D.3.2

Agent Programming with Declarative Goals

Authors: F. S. de Boer, K. V. Hindriks, W. van der Hoek, J. -J. Ch. Meyer

Abstract: A long and lasting problem in agent research has been to close the gap between agent logics and agent programming frameworks. The main reason for this problem of establishing a link between agent logics and agent programming frameworks is identified and explained by the fact that agent programming frameworks have not incorporated the concept of a `declarative goal'. Instead, such frameworks have… ▽ More A long and lasting problem in agent research has been to close the gap between agent logics and agent programming frameworks. The main reason for this problem of establishing a link between agent logics and agent programming frameworks is identified and explained by the fact that agent programming frameworks have not incorporated the concept of a `declarative goal'. Instead, such frameworks have focused mainly on plans or `goals-to-do' instead of the end goals to be realised which are also called `goals-to-be'. In this paper, a new programming language called GOAL is introduced which incorporates such declarative goals. The notion of a `commitment strategy' - one of the main theoretical insights due to agent logics, which explains the relation between beliefs and goals - is used to construct a computational semantics for GOAL. Finally, a proof theory for proving properties of GOAL agents is introduced. Thus, we offer a complete theory of agent programming in the sense that our theory provides both for a programming framework and a programming logic for such agents. An example program is proven correct by using this programming logic. △ Less

Submitted 3 July, 2002; originally announced July 2002.

ACM Class: F.3.1; F.3.2; I.2.5; I.2.4