
C. Bannister, P. Höfner:
False Failure: Creating Failure Models for Separation Logic. In J. Desharnais, W. Guttmann, S. Joosten (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS '18). Lecture Notes in Computer Science 11194, Springer, 2018.
doi: 10.1007/9783030021498_16
abstract  pdf  bibtex
Abstract:
Separation logic, an extension of FloydHoare logic, finds countless applications in areas of program verification, but does not allow forward reasoning in the setting of total or generalised correctness. To support forward reasoning, separation logic needs to be equiped with a failure element. We present several ways on how to add such an element. We show that none of the `obvious' extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning.
@InProceedings{Hoefner20185,
Author = {Bannister, C. and H{\"o}fner, P.},
Title = {False Failure: Creating Failure Models for Separation Logic},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS '18)},
Editor = {Desharnais, J. and Guttmann, W. and Joosten, S.},
Series = {Lecture Notes in Computer Science},
Volume = {11194},
Pages = {00},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783030021498_16}
}

R.J. van Glabbeek, P. Höfner, D. van der Wal:
Analysing AWNspecifications using mCRL2 (extended abstract). In C.A. Furia, K. Winter (eds.), Integrated Formal Methods (iFM 2018). Lecture Notes in Computer Science 11023, pp. 398418, Springer, 2018.
doi: 10.1007/9783319989389_23
abstract  pdf  bibtex
Abstract:
We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL2 is now available for AWNspecifications. We show that the translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.
@InProceedings{Hoefner20184,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and van der Wal, D.},
Title = {Analysing AWNspecifications using mCRL2 (extended abstract)},
BookTitle = {Integrated Formal Methods (iFM 2018)},
Editor = {Furia, C.A. and Winter, K.},
Series = {Lecture Notes in Computer Science},
Volume = {11023},
Pages = {398418},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319989389_23}
}

C. Bannister, P. Höfner, G. Klein:
Backwards and Forwards with Separation Logic. In J. Avigad, A. Mahboubi (eds.), Interactive Theorem Proving (ITP 2018). Lecture Notes in Computer Science 10895, pp. 6887, Springer, 2018.
doi: 10.1007/9783319948218_5
abstract  pdf  bibtex
Abstract:
The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.
@InProceedings{Hoefner20183,
Author = {Bannister, C. and H{\"o}fner, P. and Klein, G.},
Title = {Backwards and Forwards with Separation Logic},
BookTitle = {Interactive Theorem Proving (ITP 2018)},
Editor = {Avigad, J. and Mahboubi, A.},
Series = {Lecture Notes in Computer Science},
Volume = {10895},
Pages = {6887},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319948218_5}
}

V. Dyseryn, R.J. van Glabbeek, P. Höfner:
Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters, T. Tini (eds.), Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017). Electronic Proceedings in Theoretical Computer Science 255, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.255.2
abstract  pdf  bibtex
Abstract:
In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counterintuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.
@InProceedings{Hoefner20176,
Author = {Dyseryn, V. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Analysing Mutual Exclusion using Process Algebra with Signals},
BookTitle = {Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017)},
Editor = {Peters, K. and Tini, T.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {255},
Pages = {00},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.255.2}
}

R.J. van Glabbeek, P. Höfner:
Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack. In Models for Formal Analysis of Real Systems (MARS 2017). Electronic Proceedings in Theoretical Computer Science 244, pp. 1452, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.244.2
abstract  pdf  bibtex
Abstract:
We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an inbuilt mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
@InProceedings{Hoefner20173,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2017)},
Editor = {},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {244},
Pages = {1452},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.244.2}
}