[%] Verifiable C 잡솨봐

[다믜(damhiya)]

https://softwarefoundations.cis.upenn.edu/vc-current/index.html

Coq로 C프로그램 검증

저건 걍 linked list로 스택 구현하는 조오오올랭 쉬운 코드인데도 쉽지 않은듯.

사실 검증이 어려운 것보다 여기까지 오는데 엄청 오래 걸리는게 문제임;

C랑 증명언어(Coq)는 당연히 배워야 되고 거기에 호어로직을 배워야 verifiable C를 이해 가능함.

개발환경에 Coq + VST(Verified Software Toolchain) 가 필요한데 이거 nix하고 direnv쓰니까 참 깔끔하게 해결되버림 퍄퍄

nix에 Coq, VST, Compcert 전부다 패키징 되있음 ㅋㅋㅋ

[익명(211.198)]

ㄷㄷㄷ

[프갤공부법(vmrofrhdqnqjq)]

[익명(211.178)]

Predicate 멀로 잡고 하는 건지나 보고 와야겠다

[black7375(8.47)]

많이 무섭다

[black7375(221.168)]

C는 물론 Coq도 같이 작성해줘야 하는거?

[다믜(damhiya)]

ㅇㅇ C로 먼저 프로그램을 작성하고, VST 툴로 이걸 Coq로 작성된 언어 AST로 변환함. 그럼 Coq에서 이 AST에 관한 성질을 표현하고 증명할 수 있음

[black7375(221.168)]

C랑 Coq 코드 동작이 동일하지 않을텐데 신기하넹

[익명(147.46)]

특정 C의 서브셋만 사용하도록 제한, C -> Coq은 올바르게 동작한다고 신뢰. 이런 가정이 추가로 들어가는 거지

[김민성태팬클럽회장(thecoqproofassistant)]