Amazon, Dafny 기반 프로그램 검증 과정 공개

Amazon이 Dafny를 사용한 프로그램 검증 교육 자료를 공개했습니다. 이 과정은 Dafny 기본 프로그래밍을 넘어, 증명 보조 도구로서의 기능을 심도 있게 다룹니다. 3개의 파트로 구성되어 있으며, 파트 1에서는 Dafny 프로그래밍 언어를 소개하고, 파트 2에서는 Dafny를 증명 보조 도구로 사용하여 자연 연역 등의 형식적 증명 기법을 배우게 됩니다. 파트 3에서는 이러한 지식을 프로그램 검증에 적용하여 함수형, 명령형, 객체 지향 프로그램의 검증을 다룹니다. 이 자료는 초보자부터 숙련된 Dafny 개발자까지 다양한 수준의 학습자에게 적합하며, 프로그램 검증에 대한 포괄적인 접근 방식을 제공합니다.