DNSを形式化して検証できるようにした、という論文。
https://doi.org/10.1145/3704898
DNSではドメイン名の解決途中に名前サーバのアドレスを再帰的に解決する必要がある。そこでこの論文ではスタック付きの状態遷移機械同士が通信し合うという形でDNSを形式化している。また、キャッシュのタイムアウトを表すためにタイマーも持っている。この形式化の元で初期状態から始めて望ましくない状態(増幅攻撃など)に到達し得るかどうかなどを検証している。