FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023
Mon 15 May 2023 12:00 - 12:30 at Meeting Room 102 - Concurrency Chair(s): Domenico Bianculli

Local variable blocks are a simple but effective program structuring technique. In the context of concurrency, local variables have the added advantage of avoiding interference from threads running concurrently with the thread containing the local variable. To provide mechanised support for verifying concurrent programs in Isabelle/HOL, we have found making use of algebraic properties of programs simplifies the development of refinement laws. The algebraic properties of local variable blocks are similar to those of existential quantifiers in predicate calculus, the algebra of which is Henkin, Monk and Tarski’s cylindric algebra. Hence to support local variables, we make use of a variant of cylindric algebra that allows quantification of a variable over a command, rather than a predicate. The approach allows a local variable to become a shared variable of parallel threads that are local to the block that introduced the variable.

Mon 15 May

Displayed time zone: Hobart change

11:00 - 12:30
ConcurrencyFormaliSE 2023 at Meeting Room 102
Chair(s): Domenico Bianculli University of Luxembourg
11:00
30m
Paper
A Dafny-based approach to thread-local information flow analysis
FormaliSE 2023
Graeme Smith The University of Queensland
11:30
30m
Paper
Transparent Actor Model
FormaliSE 2023
Fatemeh Ghassemi University of Tehran, Marjan Sirjani Malardalen University, Ehsan Khamespanah University of Tehran, Mahrokh Mirani Tehran Institute for Advanced Studies, Hossein Hojjat Tehran Institute for Advanced Studies
12:00
30m
Paper
Using cylindric algebra to support local variables in rely/guarantee concurrency
FormaliSE 2023
Larissa A. Meinicke The University of Queensland, Ian J. Hayes The University of Queensland