Re-evaluation of Logical Specification in Behavioural Verification

TL;DR

This paper empirically evaluates automated logical specification methods for behavioural models, emphasizing their robustness, scalability, and the need for adaptive heuristics to improve automated reasoning efficiency in safety-critical software verification.

Contribution

It systematically reproduces and extends prior results, identifying performance irregularities and proposing the potential for self-optimising solvers to enhance verification processes.

Findings

Theorem provers show variable efficiency depending on problem structure.

Performance irregularities suggest the need for adaptive heuristics.

Self-optimising solvers could improve stability in automated reasoning.

Abstract

This study empirically validates automated logical specification methods for behavioural models, focusing on their robustness, scalability, and reproducibility. By the systematic reproduction and extension of prior results, we confirm key trends, while identifying performance irregularities that suggest the need for adaptive heuristics in automated reasoning. Our findings highlight that theorem provers exhibit varying efficiency across problem structures, with implications for real-time verification in CI/CD pipelines and AI-driven IDEs supporting on-the-fly validation. Addressing these inefficiencies through self-optimising solvers could enhance the stability of automated reasoning, particularly in safety-critical software verification.