A Survey of Comparative Studies of Symbolic Algorithms

Abstract

Symbolic verification is one of the most important techniques used in formal software development. Many approaches have been introduced into this research area, but the problem of state explosion cannot be over emphasized. Therefore, in this article, the use of qualitative analysis (Table-driven) to describe some techniques used for symbolic algorithms and to identify knowledge gap in research for future research questions is presented. Bases of comparison include state space, time complexity, model checking methods, data intensive operations, state explosion problem, class of properties (invariant) and language specification respectively on symbolic algorithms such as Symbolic Model Verifier (SMV), Cadence SMV, A New (NuSMV), Construction Analysis Distributed Processes (CADP), ALLOY, Vienna Development Method Specification Language Analyzer (VDM-SL), TLA+ Model Checker (TLC) and Failure Divergence Refinement (FDR) were examined. From this qualitative analysis investigations, ALLOY algorithm established the best optimal symbolic states exploration in terms of low rate of state explosion problem. It contributes to knowledge by improving the scalability and efficiency of verification, providing insights into symbolic analysis and impacting academic research.