Formal Aspects of Computing

We introduce a new way of reasoning about invariance in terms of footprints in a program logic for object-oriented components. A footprint of an object-oriented component is formalized as a monadic predicate that describes which objects on the heap can be ...

This article defines embeddings between state-based and action-based probabilistic logics which can be used to support probabilistic model checking. First, we slightly modify the model embeddings proposed in the literature to allow invisible computation ...

Modeling complex system requirements often requires specifying system components in separate models, which can be validated and verified in isolation from each other, and then integrating all components’ behavior in order to validate the operation of the ...

Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational ...

Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing ...