In this paper, accepted for presentation at the 23rd International Symposium on Formal Methods, we introduce APML, a sound and complete language to sketch proofs for composition of FACTum contracts in a notation similar to Message Sequence Charts. Moreover, we provide an algorithm to generate Isabelle/Isar proofs out of an APML sketch.
The language is implemented in FACTum Studio which supports the user in the development of correct APML proofs. In addition we also implemented the algorithm in FACTum Studio which allows a user to generate Isabelle/Isar proofs out of an APML sketch.
Starting from 01.01.2020 I will be lecturer (Education and Research) at the newly founded Cybersecurity group at the University of Exeter, UK.
My article on interactive verification of architectural design patterns in FACTum got accepted for Formal Aspects of Computing. It descibes the fundamentals of FACTum and a semantic preserving algorithm to map a FACTum specification to a locale for the interactive theorem prover Isabelle.
The submission deadline for the first workshop on Formal Methods for Blockchain co-located with the 3th Formal Methods World Congress was extended. The new deadlines are as follows:
- Abstract Submission: 2019-06-30
- Paper Submission: 2019-07-07
We are looking forward to your submission!
My new article, accepted for publication in Science of Computer Programming, describes a novel calculus for dynamically adapting architectures. The calculus is shown to be sound and relative complete and it is implemented in Isabelle where it can be used to support the verification of dynamic architectures.
I am looking forward to present my work on Blockchain at FORTE and my work about Runtime Verification at ICE, both held as part of the 14th International Federated Conference on Distributed Computing Techniques in Copenhagen.
My new Paper, accepted for presentation at the 12th Interaction and Concurrency Experience, describes an approach, based on FACTum, to detect Architectural Erosion using Runtime Verification.
My paper, accepted for presentation at the 13th International Symposium on Theoretical Aspects of Software Engineering, describes a denotational semantics for dynamically evolving architectures based on fixed points in lattices.
My new paper, accepted for presentation at the 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, describes a case study in which I applied FACTum to verify persistency of blocks in Blockchain Architectures.
I’m just back from a Lorentz Center Workshop on Dynamics of Multi-Agent Systems where I was presenting my work on the verification of dynamic architectures.