We are proud to announce the release of Isabelle/DOF 1.3.0. Isabelle/DOF is a Document Ontology Framework on top of Isabelle 2021-1. Isabelle/DOF allows for both conventional typesetting and formal development.

In our work “A Denotational Semantics of Solidity in Isabelle/HOL” [1] we presented a formal semantics for Solidity, the most common language for implementing smart contracts. Such a formal semantics one of the corner stones of developing a formal verification approach that, mathematically, can prove the absence of certain types of bugs (e.g., such as the Parity Wallet bug that made USD 280mil worth of Ether inaccessible).

But, of course, any verification can only be as good as the underlying semantics. So, how do we ensure that our formal semantics actually captures the behavior of Solidity faithfully? This is the question we answer in our latest paper [2] that will be presented at the International Conference on Tests and Proofs.

A large part of an academic’s life is writing grant proposals that are submitted to funding agencies. One of the UK’s funding agencies that supports research in security, safety, and correctness of systems is EPSRC. EPSRC officially requires proposal to follow a certain layout, that is summarized on the EPSRC website as follows:

We are proud to announce the release of Isabelle/DOF 1.2.0. Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development.

Currently, the UK government pushes a concept called Digital Security by Design (DSbD) that focuses on utilizing novel hardware features to improve the security and trustworthiness of systems. Actually, Digital Security (and Privacy) by Design is a much broader concept focusing on security and privacy of systems right of systems right from the start of their development. And it also links to the - often misunderstood - concept of the Trusted Computing Base (TCB).

As part of the launch of the UK’s new Cyber Security Strategy it has been announced that we are participants of a successful demonstrator project. The project is led by Beam Connectivity.

Several fully funded PhD scholarships for UK applicants are available in the Security and Trust of Advanced Systems Group (Prof. Achim Brucker and Dr. Diego Marmsoler) at the Department of Computer Science of the University of Exeter, UK.

Smart contracts are programs, usually automating legal agreements such as financial transactions. Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly initialized contract was the root cause of the Parity Wallet bug that made USD 280mil worth of Ether inaccessible. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts.