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
洪 民憙 (Hong Minhee)

洪 民憙 (Hong Minhee)

@hongminhee@hackers.pub

Hi, I'm who's behind Fedify, Hollo, BotKit, and this website, Hackers' Pub! My main account is at @hongminhee洪 民憙 (Hong Minhee).

Fedify, Hollo, BotKit, 그리고 보고 계신 이 사이트 Hackers' Pub을 만들고 있습니다. 제 메인 계정은: @hongminhee洪 民憙 (Hong Minhee).

Fedify、Hollo、BotKit、そしてこのサイト、Hackers' Pubを作っています。私のメインアカウントは「@hongminhee洪 民憙 (Hong Minhee)」に。

bgl gwyng

bgl gwyng

@bgl@hackers.pub

박준규

박준규

@curry@uri.life