Logic & Formal Verification
명제 및 서술 논리부터 시작하여, 시스템의 올바름을 수학적으로 증명하는 형식 검증 기법을 다루는 학습 노드입니다.
용어5
formal-verification
이 용어로 연결된 기록을 섹션별로 살펴봅니다.
Boolean Algebra & Circuit Logic
이진 상태의 논리 연산을 수학적으로 정립한 불 대수와 이를 하드웨어로 구현한 논리 회로의 설계 및 최적화 원리를 다루는 학습 노드입니다.
Formal Specifications & TLA+
시스템의 상태와 변화를 수학적으로 엄밀하게 기술하는 정형 명세 기법과, 특히 분산 시스템의 설계 결함을 탐지하는 데 탁월한 TLA+의 원리를 다루는 학습 노드입니다.
Program Correctness & Verification
소스 코드 레벨에서 프로그램이 명세대로 동작함을 수학적으로 입증하는 호어 논리와 루프 불변량, 그리고 정적 분석 기법을 통해 소프트웨어 무결성을 다루는 학습 노드입니다.
Propositional & Predicate Logic
컴퓨팅 사고의 가장 원자적인 논리 단위인 명제 논리와 변수 및 양화자를 포함한 서술어 논리를 정의하고, 선언적 스펙 정의와 인공지능 추론의 기초를 다루는 학습 노드입니다.