Suyeong RHIE @noxowl@hackers.pub
Public

@bglbgl gwyng 네 직접 논리를 정의해서 쓰시면 할 수 있습니다. 수업에서는 뮤텍스 프로토콜 검증을 위한 증명을 했었고요. GitHub나 논문 발표 선에서 동시성이나 암호화 관련 증명하는데 가끔 보이는 것 같습니다. 저도 인터랙션 플로우를 상상하며 정의할 때 엣지케이스를 미리 시뮬레이션(물론 현실은 쉽지 않음) 해 보는데 활용합니다.

Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ

Verification of concurrent programs is very tough because the proof needs to account for a huge number of interleavings of execution steps of all threads. As concurrent programs are often implemented in C/C++, which do not support garbage collection, program...

link.springer.com · SpringerLink

0
1
0

If you have a fediverse account, you can quote this note from your own instance. Search https://hackers.pub/ap/notes/0195fb9a-7140-70b1-ac2f-43556abdfa42 on your instance and quote it. (Note that quoting is not supported in Mastodon.)