Formal Verification of Questionnaire Logic Using SMT Solvers

Sághelyi, Péter, Bereczky, Péter (2026) Formal Verification of Questionnaire Logic Using SMT Solvers In: Proceedings of the 13th International Conference on Applied Informatics. Eger, Eszterházy Károly Catholic University Líceum Publisher. pp. 227-243.

pdf ICAI2026-pp227-243.pdf Download (680kB) [error in script]

Absztrakt (kivonat)

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.

Mű típusa:	Könyvrészlet - Book section
Szerző:	Szerző neve Email MTMT azonosító ORCID azonosító Közreműködés Sághelyi, Péter NEM RÉSZLETEZETT NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző Bereczky, Péter NEM RÉSZLETEZETT NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző
Kapcsolódó URL-ek:	Befoglaló kötet
Kulcsszavak:	questionnaire verification, SMT solvers, formal methods, Z3, preconditions, postconditions
Nyelv:	angol
DOI azonosító:	10.17048/icai.2026.227
Felhasználó:	Tibor Gál
Dátum:	22 Szep 2026 08:02
Utolsó módosítás:	22 Szep 2026 08:02
URI:	http://publikacio.uni-eszterhazy.hu/id/eprint/9449

Műveletek (bejelentkezés szükséges)

Tétel nézet