Check out our preliminary program for FMBC: We are looking forward to exciting talks about verification of Smart Contracts and Consensus Protocols. Moreover, our invited speaker Ilya Sergey will give a talk about The Scilla Journey: From Proof General to Thousands of Nodes.
FMBC: List of Accepted Papers
Thanks to all the authors which sent their papers to FMBC: the 1st Workshop on Formal Methods for Blockchains @ FM.
Competition was fierce: we received 20 high-quality submissions out of which we accepted seven regular papers and three additional short papers.
The list of accepted papers is available at: https://sites.google.com/view/fmbc/program
Congratulations to all the authors of accepted papers!
We are looking forward to meeting all of you in October for a day of inspiring discussions on Formal Methods for Blockchains!
Paper accepted @ FM 2019 – APML: An Architecture Proof Modeling Language
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.
Lecturer in Cybersecurity at the University of Exeter
Starting from 01.01.2020 I will be lecturer (Education and Research) at the newly founded Cybersecurity group at the University of Exeter, UK.
Interactive Verification of Architectural Design Patterns in FACTum
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.
FMBC: New Deadlines
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!
A Calculus for Dynamic Architectures
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.
