Formal Verification of Questionnaire Logic Using SMT Solvers

Sághelyi, Péter and Bereczky, Péter (2026) Formal Verification of Questionnaire Logic Using SMT Solvers. In: Proceedings of the 13th International Conference on Applied Informatics. Líceum Kiadó, Eger, pp. 227-243. ISBN 9789634963271

Preview

Text ICAI2026-pp227-243.pdf - Published Version Download (680kB) | Preview

Abstract

Modern computer aided surveys (CAPI/CATI) can contain hundreds of questions with complex conditional logic. In order to guarantee correctness through all possible traversal paths is a computationally demanding challenge. We propose to replace the traditional imperative, command-based questionnaire design with a constraint-based paradigm where correctness is verified statically rather than through path discovery. This work presents a formal, declarative framework for questionnaire specification and SMT-based verification that enables this separation. We formalize questionnaires as tuples of items with preconditions and postconditions inspired by Hoare Logic, classify item reachability and postcondition feasibility through satisfiability checks, and establish a four-level validation hierarchy with five theorems characterizing the relationships between per-item, global, and path-based analysis. The method is evaluated based on real-world questionnaires.

Actions (login required)

View Item