We are looking for enthusiastic and outstanding Computer Science or
Mathematics students interested in Formal Methods and their application in areas such as Cybersecurity.
For more details, please drop me an EMail or consult the official advertisement at http://www.exeter.ac.uk/studying/funding/award/?id=3887
The workshop aims to discuss and identify possibilities and limitations of Formal Methods to provide a more rigorous approach to Blockchain. We invite authors to submit papers related to the use of FMs techniques and tools for blockchain technology.
Topics include, but are not limited to:
- Formal models of blockchain applications or concepts
- Formal methods for consensus protocols
- Formal methods for blockchain-specific cryptographic primitives or protocols
- Formal languages for Smart Contracts
- Verification of Smart Contracts
We look forward to your contribution!
My colleague Habtom K. Gidey was presenting our second release of FACTum Studio at the 16th International Conference on Formal Aspects of Component Software taking place these days in Amsterdam.
The new version now supports the modeling of behavior for component types in terms of finite-state machines and the verification of corresponding contracts using model checking.
Soon we will provide a preprint of our FACS paper which describes all the extensions in detail and demonstrates them by means of a running example.
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.
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!
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.