異なるコンピュータプログラムの実行結果が等しいかどうかを判定することは、例えばリファクタリングやコンパイラ最適化の正しさを担保することにつながるなど、プログラミングにおいて重要である。部分的に異なるプログラムの等しさを表す概念として文脈等価性があるが、その証明は容易でないことで知られている。本講演ではまず、文脈等価性の新しい証明手法である局所解析手法を簡単に紹介する。その後、この手法の大きな課題点を解決すべくどのような研究の問題を設定し解法を模索してきたかの体験談を紹介する。