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

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

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 302, Iss Proc. VORTEX 2018, Pp 1-15 (2019)

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 de

Externí odkaz: https://doaj.org/article/e44f7e5d117948708eb464eb2889f50e

Integrating ADTs in KeY and their application to history-based reasoning about collection

Autor: Jinting Bian, Hans-Dieter A. Hiep, Frank S. de Boer, Stijn de Gouw

Publikováno v: Formal Methods in System Design

We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and represent Isabelle theorems as user-defined taclets in KeY. As a case study of this n

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a102d6a92916f9fb563bc0cabbc5863e
https://ir.cwi.nl/pub/33148

Verifying OpenJDK's LinkedList using KeY (extended paper)

Autor: Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Stijn de Gouw

Publikováno v: International Journal on Software Tools for Technology Transfer, 24(5), 783-802. Springer Verlag
Hiep, H-D A, Maathuis, O, Bian, J, Boer, F S D & Gouw, S D 2022, ' Verifying OpenJDK's LinkedList using KeY (extended paper) ', International Journal on Software Tools for Technology Transfer, vol. 24, no. 5, pp. 783-802 . https://doi.org/10.1007/s10009-022-00679-7

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.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::18880226742acc0e7fa5a7dc390e03dc
https://research.ou.nl/en/publications/f9120f87-823e-4801-96ca-c3cb59163366

Completeness and complexity of reasoning about call-by-value in Hoare logic

Autor: Hans-Dieter A. Hiep, Frank S. de Boer

Publikováno v: ACM Transactions on Programming Languages and Systems, 43(4), 17.1-17.35
ACM Transactions on Programming Languages and Systems, 43(4). Association for Computing Machinery (ACM)

We provide a sound and relatively complete Hoare logic 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 support contracts and

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6910d7876cfdcb9e2beaf51be12b542b
https://ir.cwi.nl/pub/31200

Symbolic execution formally explained

Autor: Marcello M. Bonsangue, Frank S. de Boer

Publikováno v: Formal Aspects of Computing, 33(4-5), 617-636. SPRINGER

In this paper, we provide a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values.We first i

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4d25e91ec5ce0ec7fc456aaf3d6996b5
https://hdl.handle.net/1887/3273982