SAT/SMTソルバであるz3を使ってCTFの問題を解いてみた、という記事。 m1z0r3内の勉強会でz3を取り扱ったものの、途中で資料作るのがめんどくさくなって問題の解説を放棄してたのでその分ここでwriteupを書きます。 z3pyは導入済みで、大まかな扱い方はわかっ…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。