What do Relational Properties Have to Say About Legal Expert Systems ?
summary
Legal expert systems often lack a formal single-input/specification so correctness is framed relationally by comparing runs; testing finds counterexamples but cannot prove absence of bugs, whereas symbolic execution + SMT solver exhaustively collects path constraints, enumerates pairs of outcomes and either finds a counterexample or proves safety — a toy example yields nine possible violations. Work focuses on a domain-specific Catala verifier for tax rules and on extending temporal relational logics for e‑voting invariance and other robustness criteria.
AI-written summary · about