Two recent logic-based verification languages

The algebraic specification tradition keeps producing new formalisms for formal verification. We explore two of them, H and COMP. They are different from each other both in terms of mathematical foundations and in their application domains. While H is based on rather sophisticated institution-theoretic foundations in connection with hybrid modal logics, COMP is based on a form of universal algebra which realizes the behavioural specification paradigm. In the end both languages support forms of (almost) automatic theorem proving.

Razvan Diaconescu

Last modified: Sat Oct 14 17:48:39 EEST 2023