Suyeong RHIE

@noxowl@hackers.pub · 7 following · 8 followers

  • Ph.D. student in Japan (M.Phil. in Transdisciplinary Science), working as a research assistant at a Japanese national research institute.
  • Interested in the relationship between information systems and human factors (HCI).
  • Prefers explicit knowledge representation, such as functional programming and strong/safe typing languages.
GitHub
@noxowl
0
1
0
0
0
1
나는행복합니다tv @maka@social.maka.nagoya
Quiet public
Shared by Suyeong RHIE

내가 최근에 충격받은게 대부분 리눅스용 소프트웨어를 배포하는 회사들은 예전부터 데비안/레드햇/타르볼 이 3개를 국룰같이 배포했는데

요즘은 데비안/아치(AUR)/타르볼 이렇게 배포하더라

아치리눅스의 개인 사용자가 압도적으로 많아지기 시작해서 아치도 정말 메이저 반열에 들기 시작했다는 느낌이 듦

0
0
0
0
0
0
0
1
0
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
Suyeong RHIE @noxowl@hackers.pub
Public

실용적인 프로그램을 만들 수는 없겠지만, Maude와 같은 정형 명세 언어도 재미있습니다. 저는 실제 코드를 쓰기 전에 데이터 흐름을 정리하고 추상화 하여 스펙을 명확히 하는데 사용합니다. 단점은 GitHub에서 무슨 언어인지 몰라서 통계가 안 잡힙니다.

The Maude System

maude.cs.illinois.edu

0
1
0
0
1
0