Computer Science is being increasingly used in medicine to improve quality of care and patient outcome. Clinical Decision Support Systems (CDSSs) that codify clinical Best Practice Guidelines (BPGs) and provide situation-specific advice to physicians CDSSs have shown effectiveness in reducing adverse patient outcomes during clinical evaluations. However, representing both the BPG and the associated physical processes in software is complex and tedious, making CDSSs prone to bugs. This can be mitigated using a modular software architecture that encapsulates computational representation of physical processes for finer-grained development and verification leading to improved comprehensibility, shareability and maintainability. This paper discusses the sources of complexity in CDSSs, and proposes a software architecture that consists of an encoding of the BPG's medical knowledge into executable representations comprising of a patient digital twin, diagnosis and treatment workflows, an adherence monitor, a User Interface (UI) and a middleware for seamless integration with existing Hospital Information Systems. We developed a CDSS for Pediatric Sepsis Management co-designed by physicians using our approach. We use the Fluid Resuscitation therapy of this CDSS as a case study to illustrate the development process.

A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions. Unfortunately, the rise of these technologies has been marred by a series of costly bugs and exploits. Increasingly, the Ethereum community has turned to formal methods and rigorous program analysis tools. This trend holds great promise due to the relative simplicity of smart contracts and bounded-time deterministic execution inherent to the Ethereum Virtual Machine (EVM). Here we present KEVM, an executable formal specification of the EVM's bytecode stack-based language built with the K Framework, designed to serve as a solid foundation for further formal analyses. We empirically evaluate the correctness and performance of KEVM using the official Ethereum test suite. To demonstrate the usability, several extensions of the semantics are presented. and two different-language implementations of the ERC20 Standard Token are verified against the ERC20 specification. These results are encouraging for the executable semantics approach to language prototyping and specification.

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.