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.
Photo by Shahadat Rahman on Unsplash
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.
Read the Original
This page is a summary of: CSim
, ACM Transactions on Programming Languages and Systems, March 2021, ACM (Association for Computing Machinery), DOI: 10.1145/3436808.
You can read the full text:
The following have contributed to this page