Dr. Diego Marmsoler

Have you ever wondered how to ensure that your formal semantics captures the intended meaning of a language? In our new paper for TAP2022 we describe a novel approach based on grammar-based fuzzying to automatically test your executable semantics against a reference implementation. We demonstrate the approach by applying it to validate our semantics for Solidity. The paper will be presented at the 16th International Conference on Tests and Proofs co-located with STAF 2022.

I am glad to share a preprint of our latest work in which we present a denotational semantics of a subset of Solidity and its implementation in Isabelle/HOL. This is a collaboration with Prof. Achim Brucker and will be presented at SEFM 2021.

Check out the preprint to learn more about the details of Solidity.

The third edition of our Workshop on Formal Methods for Blockchain will be co-located with CAV 2021.

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!

I am very excited to serve on the program committe of TASE 2021. Prepare your papers and submit them until March 7, 2021.

Check out our new paper published in Logical and Algebraic Methods in Programming in which we show how to use FACTum to check architectural constraints for dynamically evolving architectures at runtime.

This year we got 18 high quality submissions for FMBC of which we accepted 10 research papers and 5 additional extended abstracts for lightning talks.

The list of accepted papers and lightning talks is available from the FMBC website: https://fmbc.gitlab.io/2020/program.html

Thanks again at all the authors for submitting a paper to FMBC2020!

FMBC will take place virtually on July 20 and 21 from 6AM-8AM PDT.

There will be a keynote by Grigore Rosu, Professor at University of Illinois at Urbana-Champaign, USA and Founder of Runtime Verification.

Registration to FMBC 2020 is free but required. It is done through the CAV 2020 registration form:
http://i-cav.org/2020/attending/ Please register before July 10, 2020.

I am serving in the Program Comittee of the 13th Interaction and Concurrency Experience co-located with DisCoTec 2020. Prepare your papers and submit them by 1 May 2020!

Two fully funded PhD scholarships for EU/UK applicants are available
in our group at the University of Exeter, UK.

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 second edition of our Workshop on Formal Methods for Blockchain will be co-located with CAV 2020.

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.