읽을거리 (Reading Materials)

[KihongHeo]

안녕하세요. 오늘 수업시간에 잠깐 이야기한 것과 같이, 아래와 같은 "현실적인"(계산가능한) 검증 도구와 관련된 읽을거리/볼거리를 추가했습니다. 관심이 있는 학생들은 참고자료에 새롭게 추가된 것들을 살펴보세요.

• 증명 보조기 (proof assistant): 완벽한 증명이 가능하지만 사람의 손이 많이 가는 증명 방법. 요즘은 수학자들도 수학 문제 증명에 쓰기도 합니다. 올려준 영상 참고
• 프로그램 분석기 (program analysis): 항상 끝나는 전자동 도구이지만 간혹 틀린 답을 낼때도 있습니다. 현장의 많은 회사에서 널리 쓰이고 있습니다. 올려준 글 참고

---

As briefly mentioned in today’s class, I have added some reading/viewing materials related to “practical” (computable) verification tools below. Interested students can take a look at the newly added references.

• Proof Assistant: A method that allows for perfect proofs but requires significant human intervention. These days, even mathematicians use it for proving mathematical problems. Please refer to the video provided.
• Program Analyzer: A fully automated tool that always terminates, but occasionally gives incorrect answers. It is widely used by many companies in the field. Please refer to the provided article.