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

Differences between VOCs and NOx transport contributions, their impacts on O3, and implications for O3 pollution mitigation based on CMAQ simulation over the Yangtze River Delta, China

Autor: Yangjun Wang, Sen Jiang, Ling Huang, Guibin Lu, Manomaiphiboon Kasemsan, Elly Arukulem Yaluk, Hanqing Liu, Jiaqiang Liao, Jinting Bian, Kun Zhang, Hui Chen, Li Li

Publikováno v: Science of The Total Environment. 872:162118

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::7357b63d060dbf0eae85d4326acd66fa
https://doi.org/10.1016/j.scitotenv.2023.162118

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

Footprint logic for object-oriented components

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

Publikováno v: Formal Aspects of Component Software ISBN: 9783031208713

We introduce a new way of reasoning about invariance in terms of footprints in a program logic for object-oriented components. A footprint of an object-oriented component is formalized as a monadic predicate that describes which objects on the heap c

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

VerifyingOpenJDKsLinkedListUsingKey: Proof files

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

The project files for the article `Verifying OpenJDK’s LinkedList using KeY ` The archive contains two folders: One is the original formal specification of Java’s linked list which is related to our paper for TACAS2020(See https://doi.org/10.5281

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1216468e9a84537db6914cff04fb1d64