What is it about?

A complete framework for compositional verification of concurrent systems using Isabelle/HOL. It provides CSimpl a rich language for the specification of concurrent languages, and a compositional framework for the verification of functional properties on concurrent specifications by using rely-guarantee. It also includes CSim a compositional framework for the preservation of rely-guarantee properties of CSimpl specifications between layers of abstractions.

Featured Image

Why is it important?

The verification of functional properties of complex programs at the implementation level is a hard task. CSim provides a complete inference system for the scalable verification of properties and their preservation between specification levels. Allowing to prove properties in CSimpl at the specification level, and use CSim to check that those properties are preserved in lower layers like design, implementation, or even assembly code, thanks to the versatility of CSimpl, which allows to model the semantics of complex languages like C.

Perspectives

I have hopes that thanks to this article scalable concurrent verification of software can be accessible to other formal methods engineers, and even the industry. It also may set the basis for a more complete verification framework.

David Sanan

Read the Original

This page is a summary of: CSim 2 , ACM Transactions on Programming Languages and Systems, March 2021, ACM (Association for Computing Machinery), DOI: 10.1145/3436808.
You can read the full text:

Read

Contributors

The following have contributed to this page