temporal-logic

시간 논리를 배우지 않고도 코드를 model checking할 수 있다

Kani 같은 경계 model checker과 Alloy 같은 관계 모델 탐색기는 일반적인 어서션과 제약 조건으로 속성을 검증할 수 있게 한다. 활성 증명을 포기하는 대신, 학습 곡선은 주가 아닌 시간 단위로 측정된다.