safety 검증을 초고속으로 하는 방법이 뭐가 있을까..

프로그램 전체에 걸친 invariant를 사용해서 safety를 검증하는건 기존에 많다.

 

이런 방식은 여러 safety 속성에 대해 강화하기도, 약화하기도 하며 검증을 계속 하는 구조로 되어있다.

 

이는 경우에 따라, 하나의 코드에 대해 10일 이상이상 검증이 종료되지 않는다는 것을 의미한다.

 

그래서 검증기들은 보통 timeout을 걸게되고, 이는 10분 내로만 사용한다.

 

그러면 검증기는 10분동안 invariant를 바꿔가며 safety를 검증한다.

 

만약 코드의 크기가 매우 커서, Integer Overflow를 검증해야하나 안전 속성인 NoOverFlow를 invariant로 사용하지 못한다면 검증기는 Unproven을 낸다. 하지만, 정말 안전한 경우일 수도 있지 않나.  NoOverFlow의 비용이 커서 그렇지, 만약 이를 사용했을 때 Proven이 나버리는 경우가 발생할 수 있다.

 

그렇다. 경우에 따라, 관심있는 안전 속성을 사용하여 검증기에 timeout은 너무 짧을 수 있다.

 

그래서, 관심 있는 safety 속성만을 사용하여 검증한다면 어떨까?

오, NoOverFlow를 사용하여 검증은 빨리된다. 하지만, 비용이 너무 커서 검증시간이 많이 걸린다...

 

safety 속성을 임의값부터 시작하는 경우, 빨리 종료된다. 왜냐면, NoOverFlow를 사용하기 전에 60초가 도달하고, 마지막 연산의 비용이 작기 때문에 timeout만큼만 돌아가는 것이다. 완전 할루시네이션이 아닌가..

 

초고속 검증을 하고 싶은데 잘 안된다. 머리 아프네