Logic Column 12: Logical Verification and Equational Verification

TL;DR

This paper compares logical verification, which uses logic to specify system properties, with equational verification, which simplifies systems to verify properties, analyzing their relationship through examples like process calculi and regular programs.

Contribution

It explores the relationship between logical and equational verification approaches using practical examples, highlighting their differences and connections.

Findings

Logical and equational verification are related but distinct methods.

Examples demonstrate how each approach verifies system properties.

The relationship between the two methods is clarified through case studies.

Abstract

This article examines two approaches to verification, one based on using a logic for expressing properties of a system, and one based on showing the system equivalent to a simpler system that obviously has whatever property is of interest. Using examples such as process calculi and regular programs, the relationship between these two approaches is explored.