Verification of Shared-Reading Synchronisers

Autor: Amighi, Afshin, Huisman, Marieke, Blom, Stefan

Publikováno v: EPTCS 272, 2018, pp. 107-120

Synchronisation classes are an important building block for shared memory concurrent programs. Thus to reason about such programs, it is important to be able to verify the implementation of these synchronisation classes, considering atomic operations

Externí odkaz: http://arxiv.org/abs/1806.09851

Verification of concurrent systems with VerCors

Autor: Amighi, Afshin, Blom, Stefan, Darabi, Saeed, Huisman, Marieke, Mostowski, Wojciech, Zaharieva-Stojanovski, Marina, Bernardo, Marco, Damiani, Ferruccio, Hähnle, Reiner, Broch Johnsen, Einar, Schaefer, Ina

Publikováno v: Formal Methods for Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, 172-216
STARTPAGE=172;ENDPAGE=216;TITLE=Formal Methods for Executable Software Models
Lecture Notes in Computer Science ISBN: 9783319073163
SFM

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separ

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a0080b482db1aa0e7dab92acfd519511
https://doi.org/10.1007/978-3-319-07317-0_5

Provably Correct Control-Flow Graphs from Java Programs with Exceptions

Autor: Amighi, Afshin, de Carvalho Gomes, Pedro, Gurov, Dilian, Huisman, Marieke

We present an algorithm to extract flow graphs from Java bytecode, including exceptional control flows. We prove its correctness, meaning that the behavior of the extracted control-flow graph is a sound over-approximation of the behavior of the origi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::4d3975b778d810787d83fe7f2cafcafe
http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-61188

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Formal Specifications for Java's Synchronisation Classes.

Autor: Amighi, Afshin, Blom, Stefan, Huisman, Marieke, Mostowski, Wojciech, Zaharieva-Stojanovski, Marina

Publikováno v: 2014 22nd Euromicro International Conference on Parallel, Distributed & Network-Based Processing; 01/01/2014, p725-733, 9p