久しぶりの論文メモ。今回はプログラム解析のネタ。2 つのプログラムが機能的に同値であるかどうか判定する技術について。プログラムの静的解析は自分の専門だったので、たまに論文読むと里帰りの気分を味わえる。 タイトル ARDiff: Scaling Program Equival…

Z3 ソルバーについてのメモ。 主なトピックは SMT-LIB の define と declare について。 Z3 と SMT-LIB Z3 は言わずと知れた SMT ソルバーである。オープンソースであり、Github のページにインストール手順も載っている。この手順の通りにやれば（少なくと…