Amazon、Dafnyベースのプログラム検証コースを公開

Amazonは、Dafnyを使ったプログラム検証の教育資料を公開しました。このコースは、Dafnyの基本的なプログラミングにとどまらず、証明支援ツールとしての機能を深く掘り下げています。3つのパートで構成されています。パート1ではDafnyプログラミング言語を紹介し、パート2ではDafnyを証明支援ツールとして扱い、自然演繹などの形式的証明手法を学びます。パート3では、これらの知識をプログラム検証に応用し、関数型、命令型、オブジェクト指向プログラムの検証を扱います。このリソースは、初心者から経験豊富なDafny開発者まで、幅広いレベルの学習者に適しており、プログラム検証への包括的なアプローチを提供します。