Publications : Papers, Technical Memos, Trip Reports

Papers : Team 1, Team 2, Team 3, Individuals, Research Associates. (Papers in (-year, author's name) order)

Team 1: Leading analysis technology research & development

"SAFEWAPI: Web API Misuse Detector for Web Applications."
SungGyeong Bae, Hyunghun Cho, Inho Lim, and Sukyoung Ryu.
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'14). 2014.

[bibTex | pdf |

API를 사용하는 JavaScript 프로그램의 오류를 검출하는 검출기에 대한 논문이다.또한 정적분석에서 언제나 골칫덩어리로 생각되는 API 모델링을 어떻게 자동으로 잘 해볼 수 있을까에 대한 논문이기도 하다.

같이 연구를 진행한 삼성전자 소프트웨어 센터 분들과 우리의 필요가 맞았기 때문에 좋은 결과가 나올 수 있었던 것 같다. 산학협력을 시작할 때, 우리 연구실에서는JavaScript 분석기를 적용해 볼 대상을 찾고 있던 중이었고, 삼성에서는 Smart TV와 Tizen 프로젝트 등 때문에 JavaScript 프로그램의 품질관리에 눈을 돌리던 시기였다. 우리 입장에서는 JavaScript를 분석하는 것이 어떤 효용성을 가지는 지, 개발자는 어떤 문제를 풀어 주기를 원하는 지를 확인할 수 있는 기회였다고 생각한다.

회사와 같이 일하면서, 처음에는 이해의 수준이 다르거나 문제를 바라보는 관점이 달라서 생기는 소통의 문제 때문에 힘들었던 기억이 있다. 지금 돌아보면 회사에서 던지는 (대답하기 곤란한) 질문들과 (해결하기 어려운) 요청사항들이, 사실은 실제 현장의 요구사항이기 때문에 우리가 미처 생각하지 못했던 좋은 연구 주제가 될 수도 있다고 생각하게 된다.

내공이 부족한 석사생이어서, 논문을 쓰면서 이런 저런 어려움도 참 많았었다. 같은 주제로 처음 썼던 논문은 ECOOP에 제출했다가 너무 삼성에 특화되어 있다고 떨어지기도 했었는데, 같은 문제를 두고 이런 저런 다른 관점으로 바라보면서 어떻게 얘기를 풀어 가는 게 좋을까 고민해 보는 기회가 되었던 것 같다. 같은 글이라도 교수님을 거치면 말끔하게 옷을 갈아 입는 걸 보고 참 신기하기도 했다. '이런 게 바로 교수님의 내공이구나' 하는 감탄이 절로 나왔다. 많은 것을 배울 수 있는 시간이었다.

]

"Slicing Probabilistic Programs."
Chung-Kil Hur, Aditya Nori, Sriram Rajamani, and Selva Samuel.
The 35th ACM Conference on Programming Language Design and Implementation (PLDI'14). 2014.

[bibTex | pdf |

이 논문은 서울대에 자리잡고 처음으로 제출한 논문이자, 나의 첫번째 PLDI 논문이다. 비록 여기 학생들과 연구한 내용은 아니라 아쉽지만 서울대 소속으로 top conference에 논문을 출간하니 더 뿌듯한 기분이 든다.

이 논문에서 우리는 확률적 프로그램(probabilistic programs)에 대한 잘라내기(Slicing) 변환을 어떻게 해야 하는지 제시하였다. 확률이 없는 일반적인 프로그램에서는 자료 의존성(data dependce)과 흐름 의존성(control dependence)만 계산하여, 프로그램의 결과가 의존하지 않는 부분은 잘라내어도 프로그램의 의미에 변화가 없다는 것이 잘 알려져 있다. 우리가 보인것은 확률적 프로그램에서는 이 두가지 의존성외에 추가적으로 관찰 의존성(observe dependence)이라는 것을 계산하여, 이 세가지 의존성이 없는 부분을 잘라내어야만 의미가 변하지 않는다는 것을 보였다. 특히, 우리는 이러한 의미 보전성을 수학적으로 엄밀하게 증명하였는데 이 증명이 상당히 복잡하고 쉽지 않았다.

이 논문은 사실 지난 POPL에 처음으로 제출하였다 실패하였던 논문이다. 하지만 POPL에 제출할 당시 우리가 한 일이 기존의 slicing에 observe dependence만 추가한 것이라는 것을 잘 이해하지 못하여, 기존의 slicing과 어떻게 다른지를 명확히 기술하지 못했었다. 하지만, PLDI에 제출할 때는 이러한 사실을 깨닫고 논문의 초점과 전개방향을 많이 바꾸었고 그 결과는 대 성공이었다. POPL의 리뷰 결과는 CCCB 였던 반면 PLDI의 리뷰 결과는 AAAB 로 극단적으로 바뀌었다.

이번 경험을 통해 확실히 느낀것은 똑같은 일이라도 어떻게 전개를 하느냐에 따라 완전히 다른 논문이 될 수 있다는 것이다. 스스로 자신의 연구 결과에 대해 정확히 이해하고,이를 바탕으로 명확한 초점을 가지고 논문을 전개해야 연구의 우수성을 잘 전달할 수 있다는 것이다.

]

"A Progress Bar for Static Anaylzers."
Woosuk Lee, Hakjoo Oh, and Kwangkeun Yi.
21st International Static Analysis Symposium (SAS'14). 2014.

[bibTex | pdf |

정적 분석기의 진행정도를 어림잡는 일반적인 방법에 관한 내용이다. 새 프로그램을 분석할 때마다 얼마나 걸릴지 모르겠어서 답답했다. 만들어봐야겠다고 결심했다.

사실 분석 진행율 예측은 생각만큼 간단치 않다. 왜냐하면 분석시간이 프로그램의 크기에 비례하지 않고 "의미적"복잡도에 비례하기 때문이다. 그런데 의미적 복잡도는 분석을 해보기 전에는 얼마나 큰지 알 수 없다.

핵심적인 아이디어는 학주 형과 이광근 교수님이 주셨다. 처음에 방향을 못잡고 막막할 때, 이광근 교수님이 래티스 높이를 기반으로 한 프로그래스 바에 대한 아이디어를 주셨다. 최종 분석결과의 래티스 높이는 전분석으로 어림잡고, 기계학습으로 오차를 보정하면 어떻겠냐고 하셨다. 그때는 그게 가능할까하고 의문이 들었던 것도 사실이다. 그런데 결국엔 그렇게 작동하게 되었다. 처음에 교수님 말씀대로 프로그래스 바를 만들고 보니, 바가 일정하게 증가하지 않았다. 래티스 높이가 꼭 계산량에 비례하는건 아니기 때문이다. 프로그래스 곡선을 찍어보니 첨에 빨리증가하고 나중에 천천히 증가했다. 만약 프로그래스 곡선이 이런식으로 변화할 것이란걸 미리 알 수 있다면 일정하게 증가하도록 조정할 수 있지 않을까? 학주 형이 던진 질문에서 시작해서 전분석 정보를 이용, 일정하게 증가하는 바를 만들었다.

이 연구는 진행하면서 재미있기도 했지만 처음부터 끝까지 막막하기도 했다. 연구 방향설정부터 결과물 평가방법까지 손에잡히는 것이 없었다. 좋은 프로그래스 바가 무엇인가? 에 대한 개념이 다소 명확하기 어려운 성질의 것이기 때문이다. 아이디어를 하나하나 내면서 진행해왔더니, 그래도 사람들이 재미있어 하는 결과가 나와서 다행이다.

]

"Global Sparse Analysis Framework."
Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Daejun Park, Jeehoon Kang, and Kwangkeun Yi.
ACM Transactions on Programming Languages and Systems (TOPLAS'14). 36 (3). 2014.

[bibTex | pdf |

PLDI 2012에서 발표했던 논문(Design and Implementation of Sparse Global Analyses for C-like Languages)의 스파스 분석 프레임웍을 확장한 것이다. PLDI논문에서 안전한 스파스 분석을 디자인 하는 프레임웍을 제시했었지만 몇 가지 제한이 있었다. 프로그램의 실행 흐름(control flow) 정보가 실행전에 주어진다고 가정하였고, 대상 분석이 특정한 실행 흐름 분할 기법(trace partitioning)을 기반으로 설계된다고 가정하였다. 확장된 버전에서는 이 두가지를 모두 일반화하였고, 스파스 분석 프레임웍이 옳다는 것을 엄밀히 증명하였다. 확장과 증명작업은 PLDI에 논문이 accept된 직후부터 시작했지만 당초 계획보다 쉽지 않아서 모두 마무리 하는데 1년이 넘게 걸렸다. 2012년 봄, 여름에 걸쳐 대준이형과 확장작업을 진행했는데 문제를 푸는 과정에서 매우 즐거웠던 기억이 많다. 확장한 후 증명에서도 몇달간 난항을 겪었는데 지훈이의 도움으로 마무리 할 수 있었다. 오랫동안 작업했던 일을 최종 마무리 하는 논문이고 리뷰과정도 매우 길었던 논문이라 출판이 되고 나니 매우 뿌듯하고 후련했다.

]

"Selective Context-Sensitivity Guided by Impact Pre-Analysis."
Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi.
The 35th ACM Conference on Programming Language Design and Implementation (PLDI'14). 2014.

[bibTex | pdf |

정적 분석의 정확도를 적은 추가비용으로 향상시키는 방법에 대한 논문이다.

대학원 초기, Sparrow 개발에 참여하면서 좌절했던 기억이 있다. 프로그램에 존재하는 모든 버그를 자동으로 찾아준다는 정적 프로그램 분석. 솔깃했지만 현실은 이상과 큰 차이가 있었고 안전한(sound) 정적 분석은 실제 세계 앞에서 무용지물에 가까웠다. 분석비용이 커서 웬만한 프로그램은 통째로 분석하는 것이 불가능했고, 가능하다 하더라도 수시간 혹은 수일을 기다려 얻게되는 결과는 수많은 허위경보 뿐이었다.

당시에는 실망했지만 지금 생각하면 오히려 운이 좋았다는 생각이 든다. 정적 분석 분야에서 실전 문제를 경험하는 것은 세계적으로도 흔치 않은 기회이기 때문이다. 직접 겪은 문제들은 자연스레 나의 연구주제가 되었고 박사과정동안에는 분석 비용을 줄이는 연구에 집중했다. 박사후과정에서는 정확도를 높이는 연구를 진행하고 있다. 이 논문은 정확도 향상 연구에 있어서 첫번째 결과물이다.

아이디어는 간단하다. 요약해석(abstract interpretation)이론에 따르면 임의의 원하는 수준으로 정확도를 가지는 분석을 디자인하는 것이 가능하지만, 보통 분석 비용이 크게 증가하기 때문에 함부로 정확도를 높일 수 없다. 따라서 필요한 곳에만 알맞게 높은 정확도를 적용하는 방법이 필요한데, 문제는 필요한 곳을 어떻게 찾느냐는 것이다. 이 논문에서 우리는 대상 정확도를 최대로 가지지만 나머지는 과감히 요약된 전분석을 돌려봄으로써 높은 정확도가 필요한 부분을 예측하는 아이디어를 제시했다. 즉, 대상 정확도의 영향을 전분석을 통해서 어림잡아 보는 것이다.

간단하지만 신선한 아이디어라는 확신이 있었다. 하지만 POPL 2014에 도전했을때 돌아온 리뷰는 한결같이 아이디어가 너무 단순하다 것이었다. 간단한건 맞지만 리뷰어가 논문의 핵심을 파악하진 못했다는 인상을 받았다. 핵심 아이디어가 더욱 명료하게 드러나도록 하고 내용을 보강하여 PLDI에 제출했다. 이번에는 네 명의 리뷰어로부터 모두 아이디어가 참신하다는 평가를 받았다.

이번 논문 역시 즐거운 경험이었다. 양홍석 교수님께 엄밀함을 이광근 교수님께 명료함을 훈련받을 수 있었다. 함께 연구를 진행했던 원찬, 기홍이와의 협업도 기억에 남는다. 이 논문은 2012년에 이어서 PLDI에 게재한 논문이다. 무엇보다 우리의 연구로 프로그래밍 언어 분야에서 세계와 어깨를 나란히 하는 것이 그리 어렵지 않겠다는 자신감이 생겼다.

]

"Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing."
Hyunha Kim, Kyung-Goo Doh, and David A. Schmidt.
20th International Static Analysis Symposium (SAS'13). June 2013. pp. 194-214.

[bibTex | pdf |

2009년 SAS에 abstract parsing을 소개하는 논문을 발표하고 나서 들떠 있었다. 응용분야가 많이 보였기 때문이다. 그렇지만 길이 바로 뚫리진 않았다. 범용 도구의 구현 등 넘어야 할 산이 많았다. 그 중 하나가 의미분석이었다.
실행 중에 만들어낼 문자열의 의미까지 미리 파악할 수 있으면 유용하게 쓸 곳이 많아 보였기 때문이다. 속성문법처리 기법으로 의미를 처리할 수 있겠다는 생각이 바로 들었다. 아이디어는 2011년 Carolyn Talcott Festschrift 헌정 논문에서 언급했지만, 실제로 적용하여 실험해 볼 수 있는 사례를 찾기는 쉽지 않았다. 결국, 오랜 고민 끝에 HTML DTD를 LR(k)로 표현할 수 없다는 점에 착안하여, LR(k)로 표현할 수 없는 부분은 모두 속성으로 표현하여 HTML LR(1) 속성문법을 완성하여 실험 준비를 완료하였다. 그리고 의미 속성을 파싱과 동시에 처리할 수 있도록 abstract parser를 확장하였다. 결국 생성문자열의 구문 및 의미 분석이 동시에 가능하다는 사실을 실제 사례로 입증했을 뿐 아니라, 애플리케이션이 생성할 HTML문서의 정적 검증을 범용 도구로 할 수 있음을 보임으로써 두 마리 토끼를 동시에 잡은 셈이 된 것이다. 구현에 시간이 오래 결렸지만 실험 결과가 잘 나와서 SAS에 발표할 수 있게 되었다.

]

"Sound Non-Statistical Clustering of Static Analysis Alarms."
Woosuk Lee, Wonchan Lee, and Kwangkeun Yi.
Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'12). 2012.

[bibTex | pdf |

정적 분석기 사용자 편의성을 증대시키는 일반적인 방법에 관한 논문입니다. 제 첫번째 학회논문이고, 실제 산업 현장에서 문제를 찾은 연구입니다. 문제는 제가 인턴을 하면서 발견했습니다. 저는 여름방학에 연구실의 분석기 Sparrow를 상용화한 파수닷컴에서 인턴을 했었습니다. 파수닷컴은 분석기를 다른 소프트웨어 회사에 팔면서 알람 분류(분석 결과 중 실제 오류들만 찾는 일) 서비스도 제공하고 있었습니다.

저는 인턴을 하면서 종종 그 일을 도왔는데 재미도 없고 힘이들었습니다. 왜냐하면 알람이 일반적으로 많이 나오고, 그 중에 허위 경보도 섞여있는 가운데 진짜 오류를 찾는 것은 귀찮은 노동의 연속이었기 때문입니다. 알람을 빨리 검사하면 하루 종일 100개 정도를 봤는데, 분석 결과 몇백개의 알람이 나오는 일도 허다했습니다. 그래서 이 일을 어떻게 하면 편하게 할까 고민하다가, 같은 원인을 공유하는 비슷한 알람들이 많다는 걸 알았습니다. 이 중 안전하게 일부만 보여주는 일을 자동화시킬 수 있겠다 싶어서 당시 연구실에 계시던 김유일 박사님과 함께 이 일을 시작했습니다.

처음엔 간단한 일 같았지만 생각보다 해결해야 될 문제들이 많았습니다. 초반에는 알고리즘을 어떻게 설계해야 하는지 알기 위해서, 나중에는 구현이 제대로 되었나 확인하고 예제들을 찾기 위해 알람을 수천개는 본 것 같습니다. 일을 진행하는 동안 시간은 거의 1년이 지나면서 파트너는 김유일 박사님에서 이원찬 연구원으로 바뀌었습니다. 내용을 정리해서 VMCAI에 내게되었고, 감사하게도 이것이 제 첫번째 학회 논문이 되게 되었습니다.

]

"GMeta: A Generic Formal Metatheory Framework for First-Order Representations."
Gyesik Lee, Bruno C. d. S. Oliveira, Sungkeun Cho, and Kwangkeun Yi.
Proceedings of the European Symposium on Programming. 2012.

[bibTex | pdf |

석사 1년차에 여러 박사님들과 함께 연구를 할 수 있었다는 것은 아주 큰 행운이었습니다. 이 기간에 많은 것을 배울 수 있었습니다. 먼저 증명 보조기인 Coq에 대해 배우고, 데이터 타입이 정해지기 전에, 미래에 정해질 데이터 타입의 값에 대해 적용 가능한 함수를 정의하는 DGP(Datatype Generic Programming)에 대해 배웠습니다.

'내가 연구에 도움이 될 수 있을까?'

여러 박사님들과의 연구는 저에게 작지 않은 부담으로 다가왔습니다. 먼저 연구에 참여하기 위해서는 Coq 프로그래밍이나 DGP에 대한 개념을 갖추어야 했습니다. 아직 완벽히 작성되지는 않은 논문과 지금까지 이계식 교수님께서 만드신 GMeta 라이브러리를 참고하며 라이브러리 확장을 시작했고, 그렇게 부딪히며 연구에 대한 이해가 깊어짐을 느낄 수 있었습니다.

이 연구는 프로그래밍 언어를 Coq과 같은 증명보조기에서 표현/증명할 때 필요한 성가신 infrastructure들의 자동생성을 목표로 하고 있습니다. 손으로 증명할 때에 이런 infrastructure들을 가정하고 넘어가는 경우가 많은데, 증명 보조기를 이용할 때엔 이것들이 모두 증명되어야 하는 부담이 있습니다. GMeta를 이용하면 이런 부담을 줄여줌으로써 사용자는 좀 더 중요한 부분의 증명에 집중할 수 있게 됩니다.

이 연구가 accept되기까지 2년이라는 짧지 않은 시간이 걸렸습니다. 여러 번의 reject이 있었습니다. POPL, ICFP, CPP. 분명 문제도 명확하고, 해결법도 아름다우며, 결과도 나쁘지 않았지만, 좋은 평가를 받지는 못했습니다. 논문을 새로 제출할 때마다 어떻게 하면 연구의 내용을 잘 전달할 수 있을지 고민하고 수정하였습니다. 결국 2년만에 ISOP의 리뷰어들로부터 좋은 리뷰를 받을 수 있었습니다.

리뷰 중
"Not only does it provide a new application of datatype-generic programming, but it solves a real problem in mechanized metatheory."

"For a reader like me who has suffered from exactly the problem of tedious boilerplate infrastructure for programming-language proof developments that is addressed here, this is very welcome work."

이번 경험을 통해 우리 주변의 문제를 해결하는 것이 좋은 연구라는 사실을 다시 한 번 확인할 수 있었습니다.

2009년 무더운 여름이 지나갈 무렵 Bruno가 ROPAS 그룹에 합류했다. 처음에
서로 소개를 하면서 generic programming과 Haskell이 주 전공이라
말하기에 논리와 Coq을 주로 다루는 나와는 좀 거리가 있다 싶었는데 어느 날
Bruno가 generic programming과 Coq을 접목시킬 수 있는 아이디어가 있는데 한 번
들어보겠냐고 물었다.

GMeta의 시작이었다. 이후 우리들은 처음의 아이디어를 구현하려고 하면서
서로 배움을 주고 받았다. 나는 generic programming을, Bruno는
Coq을. 잠시 후 프로젝트에 합류한 성근이는 generic programming과 Coq
모두를 익혀야 해서 보다 많은 에너지를 필요로 했다.

처음엔 Coq에서 어떻게 구현할 것인가에 집중하면서 많은 테스트를 할 수
밖에 없었다. 시간과 노력이 조금씩 쌓이면서 원하는 형태의
모습을 갖출 수 있었으며, variable binding에 관한 나의 경험을 바탕으로
해서 GMeta 라이브러리를 구현하기 시작하였다.

논문을 학회에 처음 제출하기까지 약 10개월여 준비하면서 마지막 석 달은 정말로
정신없이 구현에만 몰두하였다. Bruno는 이론과 논문 작성을 담당하고
Coq 구현은 나와 성근이가 전담하는 식으로 역할을 분담하였는데 성근이의
도움이 있었기에 기한에 맞추어 구현을 일단락 지을 수 있었다.

GMeta 이야기를 하다보니 Bruno, 성근이와 토론을 하며 보낸 많은 시간들이
소록소록 떠오른다. 내겐 아주 소중한 경험이다.

]

"Vigilare: Toward Snoop-based Kernel Integrity Monitor."
Hyungon Moon, Hojoon Lee, Jihoon Lee, Kihwan Kim, Yunheung Paek, and Brent Byunghoon Kang.
Proceedings of the 2012 ACM Conference on Computer and Communications Security(CCS'12). New York, NY, USA. 2012. pp. 28-37.

[bibTex | pdf |

저희 연구그룹이 강병훈 교수님을 처음 만난 것은 2011년 6월의 워크샵이었습니다. 처음에는 관심사와 배경지식의 차이가 커서 서로 의견을 교환하고 논의를 진행하는 것이 쉽지는 않았지만, 같은 이유로 흥미로운 연구방향들이 나오기도 했습니다. 그러한 일련의 만남과 논의 끝에, 그 해 여름이 끝나기 전에 “프로세서와 메모리의 통신 내용 감시를 통한 시스템 무결성 검사” 라는 Vigilare의 기본 아이디어를 정립할 수 있었습니다.
개념적으로는 간단한 시스템이었지만, 그 구현 이 그리 간단하지만은 않았습니다. 다행히 그 동안 저희 연구그룹 내에서 개발해온 플랫폼이 있어 플랫폼을 처음부터 구성하는 수고는 덜 수 있었지만, 구현하고자 하는 하드웨어의 특이성 때문에 그 플랫폼을 그대로 사용할 수는 없었습니다. 이를 위해 여름부터 저희 연구그룹의 이지훈연구원이 참여하여 저희 아이디어를 검증할 플랫폼을 만들고, 거기에 저희가 구현한 하드웨어 모듈들을 추가하였습니다.
하드웨어 구현 외에도 저희 아이디어를 검증하기 위해 감시의 대상으로 삼았던 리눅스 커널을 분석하고 공격 샘플을 구현할 필요가 있었습니다. 이를 위해 강병훈교수님 연구그룹의 이호준, 김기환연구원이 참여하여 리눅스 커널 분석을 통해 감시의 대상을 정의한 뒤, 저희 아이디어를 검증하기 위한 샘플 공격 코드를 만들었습니다.
이와 같은 조각들이 하나 둘 맞추어져 가던 2012년 1월, 제가 강병훈교수님께서 당시 계시던 미국 조지 메이슨 대학으로 갔습니다. 그곳에서 여러 조각들을 모아 아이디어를 검증하기 위한 일련의 실험들을 진행하고, 함께 진행 중이던 논문작업 또한 진행할 수 있었으며, 3월에는 어느 정도 틀이 잡힌 논문을 가지고 귀국할 수 있었습니다. 한달 반 정도의 검토기간을 거친 후, 1년에 가까운 연구 끝에 5월에 그 결과를 CCS에 투고할 수 있었고, 최종적으로 논문이 받아들여짐으로써 그 결실을 맺게 되었습니다.
당시에도 생각했고 지금도 그렇게 생각하지만, 한 사람이라도 없었다면 진행되기 힘들었을 진정한 의미의 공동연구였던 것 같습니다.

]

"Design and Implementation of Sparse Global Analyses for C-like Languages."
Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi.
The 33rd ACM Conference on Programming Language Design and Implementation (PLDI'12). 2012.

[bibTex | pdf |

이 논문은 박사과정 기간동안 100만 라인 프로그램 분석에 도전했던 연구의 최종 결과로써 순수 국내 연구로는 최초로 PLDI(Programming Language Design and Implementation)에 채택된 논문이다. PLDI는 POPL과 더불어 프로그래밍 언어 분야 최고의 학회이다.

스패로우를 개발하던 때(2006~7년)에는 100만라인 분석은 상상하기 힘든 일이었다. 당시에는 전체분석으로 1만라인 정도 분석하는데에도 비용이 상당했고 3만라인 달성이 목표였기 때문이다.

문제 해결의 실마리는 스파스 분석(sparse analysis), 즉 필요한 프로그램 지점을 필요한 메모리 영역만 가지고 분석하는 기법을 적용하면서 얻어졌다. 2009년 가을에 Lucas Brutschy가 인턴을 왔고 함께 초기 아이디어를 구현했다. 하지만 Lucas 버전은 몇가지 문제가 있었는데, 어떻게 해야 올바른 구현이 되는지 확신할 수 없었고 (때문에 안정화가 안된채 버그가 많았고) 아직 큰 프로그램을 분석하지 못했다. Lucas가 돌아간 후 윤석이형, 기홍이와 함께 팀이되어 1년넘게 구현 안정화 작업을 했고, 그러던 중에 기존의 연구에서는 발견하지 못했던 올바른 스파스 분석을 설계하기 위한 일반적인 이론적 기반을 찾아냈다. 2011년 여름이 되니 이론적 기반과 함께 구현체가 완성되었다.

내용에는 자신이 있었지만, 늘 그렇듯 논문마감에 맞춰 쓰기에는 시간이 너무 부족했다. 이때 원찬이와 우석이가 합류해서 깔끔한 이론과 함께 더욱 튼튼한 실험결과를 얻었다. 하지만 특히 논문의 전체적인 방향을 잡기가 쉽지 않아서, 1달을 넘게 뚜렷한 성과없이 시간을 보냈고, 제대로 쓰기 시작한것은 논문 마감 두 주 전이었고 모든 내용을 가까스로 완성하고 나니 제출이 삼십분 남아 있는 상황이 되었다.

사실 제출하고 나서는 논문이 채택된다는 것을 생각못했다. 왜냐하면, 제출 후 바로 이론상의 오류가 발견되었고, 철자, 문법 등 틀린것들이 허다했기 때문이다. 전혀 기대 하지 않고 있었는데, rebuttal 기간에 드래프트 리뷰가 왔는데 생각보다 호의적이었다. 스파스 분석의 이론적인 틀과 좋은 실험결과 모두를 보였다는데 평가가 좋았다. 하지만 역시 논문의 구성 및 오류 등에 대해서 의문을 제시하면서 세 명의 리뷰어가 모두 B (weak accept)를 주었다. 의문들에 대한 반박문을 작성해서 보냈다. 주로논문내용보다는 실험환경이나 구현의 올바름에 대한 의문이 많아서 구현의 신뢰성에 대해서 충분히 설명하였다. 그로부터 1달후에 최종 채택 통보가 왔다. 내심 기대는 했지만, 채택되었다는 얘기가 믿기 어려웠다. 우리의 반박문이 효과가 있어서 세 명중 두명이 A (strong accept)로 바꾸었고, 새로운 리뷰가 하나더 와서 AABB로 채택되었다.

무엇보다 오랜기간동안, 여러사람들과 함께 연구한 내용이 좋은 결과로까지 이어져서 기뻤다. 2008년 PLDI에 논문을 내고 CCCD를 받고 처참하게 떨어진 기억이 있다. 또한 당시 PLDI에 참가했는데 논문들이 너무 훌륭하고 발표도 잘해서 나도 몰래 이곳은 나와 인연이 없다고 생각해왔던것 같다. 그랬기 때문에, 교수님께서 이번 PLDI에 내보자고 하셨을때에도 사실 자신이 없었다. 하지만, 논문이 채택되었고 우리나라에서 우리만의 연구로 세계적으로 인정받았다는 사실이 뿌듯했다.

- 오학주

마음이 일었었다. 두어개 8000미터 봉우리를 오르고나니 다른 8000미터급
봉우리들은 어떨까, 라는.

다보탑 꼭지에 올라본 난장이라면 그 옆 석가탑에도 욕심을 내는 법인가.
프로그래밍언어 분야에는 양대 봉우리가 있다. 이론의 POPL과 실제의
PLDI. POPL에는 국내연구로 두 번 등정해보았다. 옆에 선 PLDI는?

당장 유치한 꺼리리라 생각했다. 이솝우화 여우의 심리 그대로였다.
높은 넝쿨에 탐스럽게 매달린 포도, 딸 수 없는 능력을 위로하는
심리적인 면역시스템. 따먹어봤자 시고 맛없을거야.

유치한 마음 유치하게 접고 대신 우리는 원래 목표에 집중했다.
정확히(precise) 실행상황을 모두 포섭하면서(sound) 초대형
프로그램을(scalable) 한꺼번에 분석하기(global analysis).
누구도 달성 못 한 이 목표를 포기하지 말자, 이런 연구를 위해서 우리만큼 제대로 된
워크벤치(Sparrow system)를 갖춘 연구그룹은 전세계에서 드믈다, 준비가
무르익었다. 독려하고 자신감을 심고 기회임을 상기시켰다. 슬로건은 "100만라인 통째분석."

이 여정에서 오학주박사는 묵묵히 끈질긴 걸음으로 맨 앞에서 루트를 개척했다.
4년간 집중한 박사과정 내내였다. 그 루트의 궤적은 APLAS'09, SPE'10,
VMCAI'11, APLAS'11, VMCAI'12의 논문들이었다. 상용화된 분석기의 기본 엔진보다
무려 1500배로 분석성능을 급격하게 증가시키는 성과들을 쏘아올렸던 궤적.
놀랍고 흥분되는 스토리를 만들어갔다.

정상에 오른 날은 2011년 9월23일 금요일이었다. 오학주군과 팀멤버들이 미팅에서
담담히 내밀었다. 100만라인 C프로그램 통째분석을 달성한 성능결과였다.

갈고닦은 아이디어는 담백했고 강했다: "필요한 부분만, 필요한 순간에."
프로그램 텍스트에 쓰인 문장들을 무턱대고 분석하지 않고, 그
실행의미 속에 숨어있던 고속통로를 낱낱히 발굴해서 이용한 것이다.
A 문장 다음에 B 문장이 있지만, A 문장의 의미가 B 문장과 관계없다면
두 문장의 분석은 순서가 없어도 된다(temporal localization). 그리고 한
문장을 분석하는 데는 그 문장의 의미에 필요한 기계상태의 조각만 있어도
된다(spatial localization).

일부분 비슷한 시도(sparse analysis)가 여럿 있었지만 모두
초보적이었다. 우리는 단단한 최초의 성능결과뿐 아니라, 일반적인 이론까지
제시하였다. 어떤 수준의 정적분석이더라도 그 정확도를 떨어뜨리지 않고
고속통로를 이용하는 분석기로 변환하는 이론.

이 연구에서 다시 한 번 확인한 것은 튼튼한 등산장비(이론)의 힘이다.
과거에 등정했던 팀들이 사용한 장비들, 그 생각의 틀은 약했다. 허술한 카우보이식
정적분석이론 말고 가장 일반적이고 튼튼한 분석이론으로 채비를하고
나섰다. 그 덕택에 중간 중간 우리의 방법들을 일반화시켜 이해하고 정비할 수
있었다. 리뷰의 한 토막이 즐겁다:

"An important strength of the paper is that the theoretical result is
very general. It could be applied to many other analyses. PLDI papers
have been accepted that were simply instances of this framework. The
result should be highly influential on future work in sparse analysis."

- 이광근

]

"The Implicit Calculus: A New Foundation for Generic Programming."
Bruno C. d. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi.
The 33rd ACM Conference on Programming Language Design and Implementation (PLDI'12). 2012.

[bibTex | pdf |

작년 9월이었다. 브루노(Bruno C.d.S Oliveira)가 이번에는 암시적 프로그래밍(Implicit Programming) 이라는 카드를 들고나왔다. 프로그램 코드에서 자명한 부분을 생략하면 프로그래밍 시스템이 타입을 토대로 유추하여 구멍을 자동으로 채워주는 기술을 암시적 프로그래밍이라고 부른다. 불필요한 코드를 줄이는데 도움이 되기 때문에 많은 언어가 (예를 들어, C++, Scala, Haskell) 암시적 프로그래밍을 지원한다. 그러나 각자 자신들의 구현에만 관심이 있을 뿐 핵심을 찾고자 하는 시도는 미비했다.

이광근 교수님이 브루노와 톰(Tom Schrjivers, University of Gent)과 이원찬 연구원으로 구성된 첫번째 팀을 꾸렸다. 나는 한달 뒤에 팀에 합류했다. 목표는 암시적 프로그래밍의 핵심을 정확하게 드러내고 Haskell과 Scala의 핵심적인 예제를 포섭하는 작은 calculus를 만드는 것이었다.

첫 단계로 브루노가 수집한 예제에서 Scala와 Haskell의 껍질을 벗겨냈다. 언어의 형식적인 껍질은 예상보다 두꺼웠다. 작업 결과물에 우리에게 익숙한 언어의 껍질이 덧입혀지기도 했다. 약 4개월간 갈아낸 끝에, 우리의 implicit calculus는 네 가지 부품만을 가지게 되었다. Haskell과 Scala의 모든 예제가 이 네 가지 부품과 lambda calclus로 간명하게 표현되었다.

다음 단계로 강력하면서도 결정가능한(decidable) 타입시스템을 찾아 나섰다. implicit calculus의 타입시스템은 Haskell과 Scala의 예제를 포섭할 만큼 강력해야 한다. 그렇다고 너무 강력해지면 타입검사(Type Checking)가 결정불가능(undecidable)해진다. 여기에 어려움이 있다. 작은 수정에도 타입시스템은 결정불가능해졌다가 다시 쓸모없어지기를 반복했다. 양 극단을 수차례 넘어다니며 점차 중간을 찾아갔다. 작업 속도를 높이기 위해 톰이 서울대를 찾아와 열흘 가량 머물기도 했다. POPL 마감을 한 달 앞두고 마침내 타입시스템이 자리를 잡았다.

마지막 난관은 논문을 쓰면서 찾아왔다. 우리는 담고 싶은 것은 너무 많았다. 브루노와 톰은 System F로의 변환을 통해 실행의미를 설명하고자 했다. Haskell 커뮤니티에서는 익숙한 방법이라고 했다. 이광근 교수님과 나, 이원찬 연구원은 과정을 드러내는 실행의미(Dynamic Semantics)를 갖추길 바랐다. 변환으로 실행의미를 정의하는 것이 익숙치 않을 수 있는 우리 분야 사람들에게까지도 잘 전달됐으면 했다. 이와 무관하게 Haskell과 Scala로 작성된 프로그램을 implicit calculus로 변환하는 방법도 보여야 했다. 욕심을 버리지 못하고 모든 것을 담은 첫 논문은 빡빡하고 거칠었다. 결국 POPL에는 채택되지 않았다. 리뷰중 아이디어를 깊이 이해한 듯 보이는 사람은 한명 뿐이었다. 설명이 직관적이지 않다는 증거였다. 아이디어 자체를 평가 받자는 취지로 내용을 줄이고 쉽게 쓴 버전을 PLDI에 제출하였다. 피드백을 취합해 논문을 재정비할 생각이었다. 놀랍게도 이번에는 굉장히 좋은 리뷰와 함께 채택되었다. 리뷰중

"The paper is well-written, if rather dense"

라는 구절에서 부끄러워졌다. 내용을 줄이고 풀어쓴 논문이 빡빡하게 느껴졌으면 첫번째 논문은 오죽했을까. 논문의 기본은 커뮤니케이션이다. 처음부터 읽는 사람이 받아들이기 좋은 만큼 담아야 하지 않았을까.

다음 리뷰가 좋았다. 최초의 야심찬 목표를 향해 한걸음 나아간 것은 확실하다.

"The paper brings clarity to a murky area of language design"

"Implicit programming"? 센터 연구교수로 있던 브르노가 나와의 미팅에서 꺼내놓았다. 이 프로그래밍 방식이 여러 언어에 도입되고 있지만 너무 중구난방이다, 잘
정리해서 그게 과연 무엇인지 그리고 그 맹수를 프로그래머가 안전하게
다루게 도와주는 방법(타입시스템)을 탐구해보고 싶다.

안돼에! 라고 반응하려는데 구으뤠? 로 바뀐것은 몇번의 미팅이후다.
연구를 위한 연구는 않된다, 그 연구동기가 실질적이면 좋겠다고 채근했다.
들어보니, 그런 프로그래밍 방식은 Haskell에서만 쓰이는 것이 아니고
Scala(Twitter 구현언어)에서도 쓰이고, 심지어는 C++의
거푸집 프로그래밍(template programming)에서 지원하려고 안달인 것이
결국은 "implicit programming"이었다.

암시적 프로그래밍(implicit programming)은 크게보면 당연한
방향이었다. 프로그래밍은 점점 상위의 레벨로 오른다. 프로그래밍에서
지루한 코딩의 과정을 줄이려는 노력이 프로그래밍의 발전 단계가
아니던가. 프로그래밍 과정에서 컴퓨터가 자동으로 해 주는 일이 점점 많아지고 있다.
암시적 프로그래밍은 컴퓨터가 자동으로 프로그램 코드를 메꿔준다.
일종의 "computer-aided programming"이다.

몇 번의 미팅끝에 암시적 프로그래밍의 핵심을 정리하게 되었다:
암시적 프로그래밍은 필요한 타입의 데이터를 만드는 코드를 자동
생성하기. 이러한 자동 코딩 과정은 단순한 논리과정으로 가능한
정도만으로 한정되었다.

그러고는 본 게임이 시작되었다. 있을 수 있는 문제와 그 가능성의 끝을
파악하는 작업. 암시적 프로그래밍의 모델을
가지고 놀아보자. "Implicit Calculus"를 정의해 갔다. 팀원들은 미팅중에
여러 아이디어들이 충돌했다. 그 언어모델의 문법구조(syntax)부터 서로 의견이 달랐다. 그 의미구조(semantics)를 정의하는 데도 이런 저런 의견이
부닥쳤다. 브르노는 전통적이지 않은 방식으로 접근하는 데
익숙했다. 학생들과 나는 전통적인 방식으로 접근하려고 했다.
브르노와 학생들이 다른 의견으로 분분할 때 어느 한 쪽의
손을 들어줘야 하는 난감한 시간이 몇번 있었다. 나는 전통적인
방향의 것에 기울었다. 내용도 그렇게 채워지고 있었다.
중간에 브로노의 제안으로 팀 슈라이버 교수가 벨기에에서 합류했다. 이미
이쪽으로 많이 탐구한 친구였다.

우선 POPL논문 마감에 맞추어 박차를 가했지만 논문은 낙방했다.
전통적인 방식으로 구성한 논문 버전. 지치고
허탈해서 내버려두려 했는데, 브로노가 PLDI에 내자고 했다. 자신이
주장하는 방식으로 각색하면 될 것 같다고, 그 방식을 선호하는 연구진이
프로그램위원회에 많이 있다고. 그래보라고 맡겼다.

보란듯이 이번에는 PLDI에 게재승인되었다. 이 논문을 "champion"하겠다는 리뷰어가 4명중
3명이었다. 올해 PLDI에 우리나라 논문은 최초다. 그것도 이 논문과 함께 두
편이 한꺼번에. 경사였다.

]

"Type Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance."
Eric Allen, Justin Hilburn, Scott Kilpatrick, Victor Luchangco, Sukyoung Ryu, David Chase, and Guy L. Steele Jr..
The Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'11). 2011.

[bibTex | pdf |

Fortress 프로그래밍 언어는 다양한 기능을 제공하고 있는데, 여러 가지 기능을 안전하게 지원하기 위해서 타입 검사가 복잡해집니다. 특히 같은 이름을 갖는 여러 함수들을 정의하고 함수 호출 시에 동적인 타입을 이용해 함수를 선택하면서, 동시에 다중 상속을 지원하는 경우에는 모듈별로 타입 검사하는 것이 까다롭다는 것이 잘 알려져있습니다. 현재까지는 같은 이름을 갖는 여러 함수의 인자 타입이 상대적으로 간단한 경우만을 다룰 수 있었는데, 이 논문에서 처음으로 다형 타입을 갖는 경우로 확장하였습니다. 확장된 타입 시스템을 엄밀하게 정의하고 구현하여, 현재 Fortress 컴파일러에서 사용하고 있습니다. 2010년 여름 두 달 동안 Fortress 팀이 있는 보스턴 근교에서 같이 공동연구하고 논문 작업한 기억이 좋은 논문으로 마무리되어 기쁘게 생각합니다.

]

"Static Analysis for Multi-Staged Programs via Unstaging Translation."
Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta.
Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11). 2011.

[bibTex | pdf |

벽같은 문제였다. 프로그램이 프로그램을 만들고 실행시키는 경우(다단계 프로그래밍 multi-staged programming) 정적분석이 가능할까? 임의의 단계로 도망가며 다이나믹하게 생성되는 프로그램 텍스트들을 추적하면서 그 실행 의미를 어떻게 미리 분석할 수 있을까? 이 문제를 만나게 된 건 2006년도 POPL논문 덕택이었다. 다단계 프로그램의 타입 시스템을 고안하고 나서 든 의문이, 타입유추이상의 일반적인 정적분석은 어떻게 해야 할까? 였다.

석사과정이던 원태에게 이 문제를 던졌다. 벅찼겠지만 흥미있어 했다. 몇 달 간은 간단한 수준에서만 맴돌았다. 다이나믹하게 만들어지는 프로그램 텍스트를 예측하는 것은 되지만, 텍스트를 넘어서 그 실행의미까지를 예측하는 방법까지는 잡히지 않았다.

결정적인 날은 2009년 5월 29일이었다. UIUC에서 박사논문을 막 마친 Baris Aktemur가 자신의 학위논문을 내게 이메일했다. 우리의 2006년 POPL논문에 기초한 것이니 한 번 읽어달라고. 그의 박사논문은 다단계 프로그램을 보통의 프로그램으로 변환하는 부분이 주요 내용이었다. 무릎을 쳤다. 이게 가능했구나. Baris를 2009년 9월초 초대했다. 우리의 연구목표에 그의 변환이 핵심으로 쓰일 수 있다는 것을 논의하고 확인했다. 다단계 프로그램을 직접 분석하는 방법 대신에, 일단 보통의 프로그램으로 변환하고 기존의 분석기술로 분석한 후, 그 분석결과를 원래의 다단계 프로그램에 대한 것으로 바꿔주면 될 것이었다.

원태와 Baris가 디테일을 파보니 학위논문의 변환을 그대로 쓰기에는 헐렁한 점들이 발견되었다. 원태와 Baris가 그 헛점들을 메꾸기 위해 분투했다. 변환이 타입을 보존한다는 증명만으로는 부족했다.

원래 프로그램의 모든 실행과정이 변환후에도 그대로 보존되야 했다. 원태와 Baris는 고달픈 증명과정을 밟아갔다. 나는 원태에게

“증명의 모든 줄은 진심으로 확신하고나서 넘어가라”

는 원칙을 반복하며 독려했다. 2010년 1월 원태를 Madrid의 POPL에 데려가 Baris와 만나 연구진행을 확인하도록 했다. 모든 증명이 서서히 마무리 되어감을 느꼈다. 2010년 3월에는 순수남 Makoto Tatsuda 교수가 방문했다. 매년 봄이면 한국이 좋다고 식구들과 서울을 방문하는 친구였다. 우리의 변환장치를 보여주었다. 재미있어 했다. 돌아가서는 타입보존 증명을 들고 5월에 다시 찾아왔다. 우리의 증명보다는 약한 결과였지만 유용했다. 증명의 스타일도 좋았다.

한편 나는 분석결과를 변환이전의 프로그램에 대한 것으로 되돌리는 데 필요한 조건을 찾아보았다. 요약해석 이론의 틀속에서 쉽게 찾아졌다. 예제를 만들어 확인해 보았다. 작동했다.

이로써 모든 내용이 준비되었고 논문으로 엮는 것만 남았다. 하지만 원태와 Baris가 준비한 초고는 변환 파트 이외에는 미숙했다. 논문 제출 2-3주 전이었다. 논문쓰기에 석사생을 담금질하며 소모할 시간이 없었다. 내가 나섰고, 맹장수술 후 발목의 통풍이 한 달 이상 날 괴롭혔던 2010년 6-7월의 여름이었다. 논문을 꿰어가며 견디던 여름밤들이 지금은 추억이다. 의족을 사용하는 원태도 힘든 여름이었을 것이다. 날카로웠던 나였다.

2006년의 POPL 논문과 이번 논문으로 “다단계 프로그램”의 분석에서는 어느새 우리가 세계를 선도한다는 느낌이 들었다. 논문 리뷰의 한 구절도 그랬다:

“Thus, this paper can serve as a standard reference for further studies of static analysis of multi-staged programs.”

]

"Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference."
Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi.
Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11). 2011.

[bibTex | pdf |

여러 사람들과 어울려 연구하는 기쁨을 알게해준 내 첫 번째 학회 논문이다. 지난 7월 왕교수님이 다시 ROPAS를 방문하셨다. 학습 알고리즘을 사용한 반복문 불변식 유추 기법을 보강하기 위한 아이디어를 들고 오셨다. 구체화 하기 위해 처음 이 일을 시작했던 정영범, 공순호 연구원이 뛰어들었다. 그러던 중 유학으로 바빠진 공순호 연구원을 대신해 내가 참여하게 되었다. 선배님들의 훌륭한 팀웍을 익히 알고 있었던 터라 누가 되지 않도록 최선을 다했다. 팀 분위기에 녹아 들면서 연구가 점차 즐거워 졌고 좋은 결실을 맺을 수 있었다. 논문은 TACAS에 채택되었는데 유럽의 CAV라고 불리는 시스템 검증 분야의 최고 학회 중 하나다.

논문의 핵심은 반복문 불변식에 필요한 부품식(predicate)을 자동으로 유추하는 방법이다. 팀에서 불변식을 찾는 새로운 기법에 대한 논문을 지난 VMCAI 2010에 개제한 바 있다. 주어진 부품식의 조합을 탐색해서 그 가운데 불변식이 될 수 있는 것을 찾는 방법이다. 부품식 탐색에 학습 알고리즘을 사용한 참신한 발상으로 호평을 받았다. 논문에서 한 가지 다루어지지 않은 것은 부품식을 생성하는 방법이다. 필요한 부품식이 모두 프로그램 텍스트에 나타는 것이 아니기 때문에 특별한 방법이 필요했다. 아이디어는 서로 함축(implication) 관계에 있는 두 명제 A, B로부터 새로운 명제 I를 알아내는 내삽법(interpolation)을 이용하는 것이다. 부품식의 조합이 불변식이 되기 위한 여러 조건을 내삽하여 새로운 명제를 알아내고 그 명제에 포함된 부품식을 다음 탐색에 활용하도록 했다.

8월 한 달을 준비했던 VMCAI 2011에서는 고배를 마셔야 했다. VMCAI 2010의 후속 연구의 색깔이 짙어 이번에도 채택 되었으면 했다.허나 준비가 부족했던 탓인지 안타깝게도 떨어지고 말았다. 리뷰는 주로 지난 VMCAI 2010에 제안된 기법 자체를 의문시 하는 내용이었다. 왕교수님은 리뷰가 지난 논문에 대한 것이었다면 받아들이겠지만 이번 것과는 상관없어 보인다시며 안타까워 하셨다.

심기 일전하여 도전한 TACAS 2011에서는 기분 좋은 소식이 기다리고 있었다. 논문을 수정하면서 BLAST와 비교하는 실험 결과를 포함시켰던 것이 유효했던 것 같다. TACAS는 모델 검증 논문이 많이 채택되는 학회라 사람들이 BLAST와의 비교를 관심있어 할 것이라고 예상했기 때문이다. 같은 프로그램에 대해 우리의 방법이 BLAST보다 더 적은 수의 부품식으로 불변식을 찾는 것을 보고 확신이 들었다. 초조해하며 기다리던 지난 12월, 논문이 채택되었다는 메일을 받았다. 거절(reject)하는 리뷰 없이 세 리뷰 모두 호의적이어서 더욱 기뻤다.

센터에 합류하고 처음으로 채택된 학회 논문이라 오래도록 기억에 남을 것 같다. 새벽까지 결과를 기다리며 메일 프로그램의 새로 고침 버튼을 수도 없이 누르던 기억이 아직도 생생하다. 채택 메일을 받고 건물이 떠나가도록 소리 질렀던 모습이 글을 쓰면서 떠올라 얼굴이 화끈거린다. 하지만, 이런 기쁜 일이 자주 있었으면 좋겠다.

- 연구원 이원찬 -

]

"FortressCheck: Automatic Testing for Generic Properties."
Seonghoon Kang and Sukyoung Ryu.
The 26th Symposium on Applied Computing. 2011.

[bibTex | pdf |

Haskell 언어의 랜덤 테스팅 라이브러리인 QuickCheck에 대해서는 익히 들어 알고 있었는데, 올 봄에 일본에서 열린 IFIP Working Group 2.8 미팅에서 John Hughes 교수님의 강연을 듣고 Fortress에 적용해보면 재미있겠다는 생각이 들었습니다. 학교로 돌아와 이제 막 연구실에 배정받은 강성훈 학생에게 Fortress와 QuickCheck에 대해서 이야기하고 몇 가지 아이디어들을 나누었습니다. 강성훈 학생은 Haskell, QuickCheck, Fortress에 대해서 하나씩 배워가면서, Haskell과 다른 Fortress 언어의 특징인 두 가지 polymorphism (subtype polymorphism과 parametric polymorphism)을 테스트하는 방법에 대해서 방향을 잡아가기 시작했습니다. 여름 동안 제가 보스턴에서 지내면서 원격으로 논문 작업을 같이 하고 ERC 여름 웍샵에서 막바지 작업을 마치고 제출한 논문입니다.

]

"MeCC: Memory Comparison-based Clone Detector."
Heejung Kim, Yungbum Jung, Sunghun Kim, and Kwangkeun Yi.
The 33rd International Conference on Software Engineering (ICSE'11). 2011.

[bibTex | pdf |

순수 국내 연구로는 최초로 소프트웨어공학 최고의 학회인 ICSE 연구 분야 (research track)에 채택된 논문입니다. 의미 분석을 통해 소프트웨어에 있는 코드 유사쌍들을 찾는 새로운 방법을 제안하는 논문입니다.

오랫동안 하고 싶어했던 연구를 좋은 사람들과 함께하고 좋은 결과도 얻어서 보람 있는 논문입니다. 2008년 겨울, 성균관대학교에서 열린 한국정보과학회 프로그래밍 연구회에 논문을 발표하러 갔었습니다. 한양대의 이욱세 교수님께서 소프트웨어 표절에 대해서 발표를 하실 때 질문을 했습니다. 표절을 찾는데 정적 분석기를 이용하는 연구는 없었냐고, 대답은 없다였습니다. 저는 함수가 일으키는 메모리 변화를 요약하여 메모리 누수를 탐지하는 분석기를 발표했었습니다. 그 함수 요약을 가지고 표절인지 여부를 판단하면 어떻겠냐고, 이욱세 교수님께 같이 연구하자고 제안했지만 거절당했습니다. 이유는 요약 정보가 너무 헐렁해서 함수 대부분이 비슷하다고 잘못 판단할 것 같다는 것이었습니다. 더 좋은 아이디어가 생기면 같이 하자고 했습니다.

2009년 삼성전자에서 김희정 학생이 연구실로 왔습니다. 회사에서 개발중인 소프트웨어에는 코드 유사쌍 (code clone)이 많이 있는데 소프트웨어 유지 보수를 위해 그런 유사쌍을 없애는 연구를 하고 싶어했습니다. 문제는 기존의 도구들은 코드의 생김새가 비슷한지만 검사를 할 수 있다는 것이었습니다. 소프트웨어 표절을 찾는데 분석기를 적용하고 싶어하던 저와 목적은 다르지만 연구 방향은 같을 수 있겠다 생각하여 그 해 10월부터 본격적으로 연구를 시작했습니다. 홍콩과기대의 김성훈 교수님께서도 소프트웨어공학 분야의 폭넓은 지식으로 도와주셨습니다.

처음에 함수의 메모리 변화 요약으로 비교를 하니 역시나 너무나 많은 함수들이 코드 유사쌍이라고 나왔습니다. 아예 요약 메모리 상태를 기억해서 비교하기로 했습니다. 비교 시간이 꽤 걸리긴 하지만 정확하게 나왔습니다. 비교 시간을 단축시키는 방법을 고안하여 구현했더니 분석 시간에 비해 상대적으로 무시할만한 시간에 비교를 할 수 있었습니다.

겨울 동안 논문을 써서 FSE 2010에 제출했습니다. 리뷰가 왔는데 제가 그동안 받아본 리뷰 중의 최고였습니다. 점수는 공개가 안 되었습니다.

다음은 2번째 리뷰의 결말 부분입니다.

Overall, a very good paper.
Point is favour:
   - novel approach
   - implementation done in a publicly available tool
   - data is publicly available
Points against:
   - nothing, really

리뷰가 좋게 왔는데 떨어지니까 별로 리뷰가 도움이 되지 않았습니다. 실험을 더 강화하고, 우리 기술의 응용 방법을 더 추가하여 ICSE에 도전했습니다. 리뷰를 받았는데 붙을 건지 아닌지 확신을 할 수 없었습니다. 반박 (rebuttal)문을 준비해서 보내고 난 후에 희정 학생이 꿈을 꾸었는데, 제가 세 명의 남자를 때려눕혔답니다. 꿈 내용을 전해 들으신 이광근 교수님께서 ICSE에 붙는 꿈이라고 하셨습니다. 리뷰어가 세 명이었습니다. 교수님께서 예상하신 대로 ICSE에 붙었습니다. 재밌게도 김성훈 교수님께서 ICSE에 낸 논문 중에 세 편이 채택되었습니다.

- 박사과정 정영범 -

]

"Memory access optimization in compilation for coarse-grained reconfigurable architectures."
Yongjoo Kim, Jongeun Lee, Aviral Shrivastava, and Yunheung Paek.
ACM Transactions on Design Automation of Electronic Systems (TODAES). 16 (42). 2011.

[bibTex | pdf |

이 논문은 2010년에 게재한 LCTES 학회 논문을 확장한 논문입니다. CGRA가 포함된 아키텍쳐는 메인 프로세서와 공유하는 메인메모리 이외에도 CGRA가 독자적으로 사용하는 로컬 메모리를 가지고 있습니다.LCTES 논문에서는 이 로컬 메모리에 데이터를 로드하였을 때 최대한 많이 재사용을 하는 것을 목표로 하여 논문을 작성하였습니다. 이 논문에서는 로컬 메모리에서 CGRA의 Processing Element (PE) 로 로드한 경우 한번 로드했을 때 최대한 많이 재사용을 하는, 즉 데이터를 재사용을 하는 granularity 을 꿔서 CGRA의 데이터 재사용 기법을 연구하였습니다.

결과는 대 성공이였습니다. 기존의 로컬 메모리에서 데이터를 재사용하는 기법을 통해서 bus traffic을 줄이는 것에, 추가로 로컬 메모리에 access하는 횟수를 줄임으로서 생성되는 코드의 사이즈를 줄이고 성능을 향상 시킬 수 있었습니다. 이 기법을 추가로 적용함으로써 CGRA에서의 데이터 재사용 기법에 대한 연구를 마무리 할 수 있었고 좋은 저널에 기제할 수 있었습니다.

]

"High Throughput Data Mapping for Coarse-Grained Reconfigurable Architectures."
Yongjoo Kim, Jongeun Lee, Shrivastava, A., Yoon, J.W., Doosan Cho, and Yunheung Paek.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 30 (11). November 2011. pp. 1599 - 1609.

[bibTex | pdf |

몇년전 UNIST에 이종은 교수님을 방문할 일이 있었습니다. 당시 제는 CGRA를 사용한 데이터 관리를 연구하고 있었는데, 수행하고자 하는 코드에 loop-carried dependency가 있을때의 처리방법에 대해서 골머리를 안고 있었습니다. 마침 이종은 교수님도 CGRA에 대한 연구를 같이 진행해 본 경험이 있었기 때문에 이 문제에 대해서 의견을 여쭤 보았었습니다. 아무런 기대도 하지 않고 했던 질문이였지만 이종은 교수님께서는 CGRA의 수행방식에 다른 견해를 가지고 계셨기 때문에 활발한 논의를 할 수 있었습니다. 당시 나는 모든것을 소프트웨어 적으로, 즉 컴파일러에서 모든것을 처리하려고 했었습니다. 하지만 이종은 교수님께서는 하드웨어를 약간 수정하는 방법을 제안을 하셨고, 결국 하드웨어에서 약간의 지원만 해 준다면 컴파일러에서 쉽게 처리할 수 있다는 결론에 도달할 수 있었습니다. 이후 일은 일사천리로 진행되어 논문 작업을 잘 마무리할 수 있었습니다.

이번 경험을 통해 연구는 혼자 하는 것이 아니라는 것을 깨달을 수 있었습니다. 혼자서도 해법을 제시할 수 있겠지만, 다른 사람과 논의를 통해 다양한 관점에서 접근한다면 훨씬 쉽게 그리고 더 좋은 해법을 찾을 수 있다는 것을 배웠습니다.

]

"Access-analysis-based Tight Localization of Abstract Memories."
Hakjoo Oh, Lucas Brutschy, and Kwangkeun Yi.
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11). 2011.

[bibTex | pdf |

연구실에서 상용화한 프로그램 분석기인 Sparrow의 성능을 올리는 방법에 대한 논문입니다. 분석기의 동작은 실제 발생가능한 모든 메모리 상태를 모두 포섭하는 요약 메모리 상태를 가지고 프로그램을 요약해서 실행하는 것이라고 볼 수 있습니다. 그런데 실제 프로그램들을 분석할때는 이러한 요약 메모리의 크기가 굉장히 커지는데, 이것이 분석기를 느리게 만드는 주요 원인중 하나입니다. 필요한 것만 가지고 다니면 될 텐데, 문제는 분석해 보기 전에는 무엇이 필요한지를 미리 정확히 알아낼수가 없습니다. 따라서 무엇이 필요한지를 안전하게 예측하는 방법들을 사용하여 불필요 한 부분들을 잘라내는 방법을 써야 합니다.

이 논문은 기존의 방법들보다 필요한 부분들을 더 정확히 알아내는 방법에 대한 것입니다. 사실 매우 간단한 아이디어지만 작은 프로그램을 분석할때는 잘 드러나지 않고 제법 큰 실제 프로그램들을 분석해 보아야만 드러나는 문제이기에 그 문제와 해결책을 처음으로 제시할 수 있었습니다. 지도교수님께서 늘 주변의 문제를 잘 해결하면 독창성은 따라오는 것이라고 말씀해 주셨는데 이를 직접 경험하게 해 준 논문입니다.

하지만 논문을 작성하는 것은 역시나 많은 에너지가 필요한 작업임을 다시 깨달았습니다. 디테일들을 나열하는 것은 쉬웠지만 그것을 한단계 위에서 정리하는 법, 그리고 딱 알맞은 정도로 표현하는 능력, 영어실력 등등의 부족함으로 인해 오랜시간이 걸렸고 또한 게재불가판정(reject)도 여러번 받았습니다. 그래도 돌이켜보면 이런 부족함들로 인해 많은 것을 배운 기회였고 많은 정성을 들인 논문이라 뿌듯합니다.

리뷰중:

“Overall, the paper is quite readable. The formulation is sufficiently but not overly formal. The theory balances well with the experimentation. And, the main idea is simple, easy to grasp and remarkably effective.”

]

"Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction."
Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwangkeun Yi.
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10). Madrid, Spain. January 2010.

[bibTex | pdf |

지난 7~9월간 센터를 방문했던 Bow-Yaw Wang 교수(Academia Sinica,
Taiwan)와의 공동연구 이야기입니다. 좋은 연구를 짧은 기간에 같이하게 된
아주 즐거운 경우였습니다.

Algorithmic Learning이라는 분야를 프로그램 검증에 사용할 수 있는 시초를 만든 연구를 같이 하고 갔습니다. 키워드는 algorithmic learning, randomness, invariant inference입니다. 정영범, 공순호 학생과의 팀웍이 완벽했습니다.

연구를 하면서 “이거다”싶은 느낌이 가끔 있습니다. 그 경우였습니다. 내년 1월 VMCAI(Verification, Model Checking, Abstract Interpretation) 학회에서 발표합니다. 논문리뷰중에

"The paper presents a fresh/novel perspective to invariant inference and has a potential to lead to a new line of subsequent work in this direction."

라는 평을 받았습니다. 드문 리뷰 기분 좋았습니다. 논문 마지막 손보기위해 모여 앉았던 이른 아침의 캠퍼스 벤치, 그 추억이 소중합니다.

키워드: invariant inference, algorithmic learning, randomization

]

"Operation and Data Mapping for CGRAs with Multi-Bank Memory."
Yongjoo Kim, Jongeun Lee, Aviral Shrivastava, and Yunheung Paek.
Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems. 45 (4). 2010. pp. 17-26.

[bibTex | pdf |

재구성형 프로세서는 작은 크기에 적은 파워를 소모하면서도 강력한 성능을 낼 수 있는 프로세서이다. 하지만 이런 장점이 있음에도 이 프로세서를 직접 사업화 하고 있는 회사는 생각보다는 많지 않다. 이점에 대해서 왜 그럴까를 생각하던 중 프로세서 자체보다는 프로세서를 둘러싸고 있는 환경에 문제가 있을 수 있다는 생각을 하게 되었다.

전체적인 시스템 환경을 구성하고 난 후 전체 수행을 시뮬레이션 해보니 프로세서에서 필요한 데이터를 원활히 공급해 주지 못해서 프로세서가 자꾸 멈추게 되는 현상을 발견하였다. 이 점에 착안하여 데이터 전송을 최소화 하기 위한 기법을 고안하게 되었고 데이터 재사용 기법을 개발하게 되었다.

이 논문에서는 재구성형 프로세서에서 성능의 최적화를 위해 재구성형 프로세서 내부의 메모리의 구조를 컴파일 타임에 고려하는 기법에 대해서 고려하고 있다. 이전까지의 논문에서는 data의 위치에 대한 고려없이 operation만의 mapping을 고려해서 데이터가 재활용 될 수 있는 기회를 없애버렸다. 이로인해 불필요한 데이터 전송이 과도하게 늘어나는 단점이 있었는데 이 논문에서는 이 문제에 착안하여 데이터의 위치를 opeartion mapping때 같이 고려해서 풀어냄으로써 성능 향상을 이끌어 냈다.

이 논문이 더 재미있는 점은 메모리 접근 오류 분석기를 적용하여 더욱 더 복잡한 데이터 접근 형태 분석이 가능하다는 점이다. 이 논문에서는 간단한 데이터 접근 분석에서 끝났지만 메모리 접근 오류 분석기를 통해 여러가지 접근 패턴을 분석하고 반영한다면 더욱 뛰어난 최적화 기법을 도출해 낼 수 있을 것이다. 또한 재구성형 프로세서는 프로세서 특성상 수작업 디버깅이 거의 불가능한데 컴파일러에서의 분석은 디버깅에 상당한 도움이 될 것이다. 이 작업은 다음 연구대상이다.

교수님께서는 항상 "문제를 푸는 것보다 문제점을 찾아내는 것이 훨씬 중요하다" 고 말씀하셨었는데 이번 논문을 쓰면서 그 점을 깨닫게 되어 더욱 보람있는 연구였다.

- 박사과정 김용주

]

"LR Error Repair Using the A* Algorithm."
Ik-Soon Kim and Kwangkeun Yi.
Acta Informatica. 47 (3). 2010. pp. 179-207.

[bibTex | pdf]

"An Algorithmic Mitigation of Large Spurious Interprocedural Cycles in Static Analysis."
Hakjoo Oh and Kwangkeun Yi.
Software - Practice and Experience. 40 (8). 2010. pp. 585-603.

[bibTex | pdf |

APLAS'09 논문을 저널버전으로 확장한 것이다. 컨퍼런스 논문에 페이지 제한으로 미처 싣지 못한 내용과 비슷한 효과를 내면서 좀 더 구현이 쉬운 알고리즘, 그 실험결과를 추가했다. 첫 논문이고 오래도록 준비했던터라 기억에 많이 남는다. SPE에서 리뷰를 두 개 받았는데 모두 긍정적이었다.

논문 리뷰 중에서:

"The paper makes a useful contribution on an issue that has not been addressed adequately in the literature…"

"The paper is also reasonably well written with examples showing up at the places where they are warranted…"

]

"Register Coalescing Techniques for Heterogeneous Register Architecture with Copy Sifting."
Minwook Ahn and Yunheung Paek.
ACM Transactions on Embedded Computing Systems. 8 (2). 2009. pp. 1-37.

[bibTex | pdf]

"Adaptive Scratch Pad Memory Management for Dynamic Behavior of Multimedia Applications."
Doosan Cho, Pasricha, S., Issenin, I., Dutt, N.D., Minwook Ahn, and Yunheung Paek.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 28 (4). April 2009. pp. 554-567.

[bibTex | pdf |

본 논문은 프로파일링을 이용한 메모리 접근 패턴 최적화와 관련된 것으로 주어진 메모리 아키텍처에 맞게 코드를 최적화하거나 설계단계에서 주어진 어플리케이션에 맞게 하드웨어를 최적화하는데 활용될 수 있는 기법을 제안하고 있다.

제안하는 기법은 미국UCI대 Nikil Dutt교수진이 벨기에의 유명 연구소인 IMEC과 공동연구를 진행했던 결과에 기반하고 있다. 본래 UCI의 연구는 정교한 소스레벨 분석을 통한 코드 최적화에 있으며 이러한 기술은 소스단계에서 메모리 접근 오류 분석에 활용하는 것이 가능하다. 최적화 관련된 분석기술을 오류검출도구로 응용하는 것은 매우 흥미로운 작업이 될 것으로 기대하고 있다.

]

"Abstract Parsing: Static Analysis of Dynamically Generated String Output Using LR-Parsing Technology."
Kyung-Goo Doh, Hyunha Kim, and David A. Schmidt.
16th International Static Analysis Symposium (SAS'09). August 2009. pp. 256-272.

[bibTex | pdf |

학자에는 좋은 연구꺼리를 찾는게 가장 큰 고민거리 중 하나다. 그런데 우연히 운 좋게도 평소에 잘 알고 지내던 소프트웨어관리도구 개발업체 사장과 차 한잔하면서 잡담하다가 연구꺼리가 하나 굴러들어왔다. 프로그램 실행 중에 만들어지는 문자열을 실행해보지 않고 이해해보고 싶다고 했다. 내가 즉흥적으로 한 대답은 "허! 그거 간단해요. 문자열 데이터 흐름 분석하면 바로 답이 나와요."였다.

그런데 전통적인 방식으로 분석해보니 기껏해야 정규표현식 정도의 정밀도로 문자열을 요약할 수밖에 없었다. 나름대로 회사에서 원하는 정도의 정보를 얻기에는 충분했으나, 그래가지고는 실행중에 만들어내는 문자열의 구문구조는 이해할 수 없었다. 누가 해놓은 연구가 없는지 뒤져보았으나 다른 사람이 해놓은 것도 같은 한계에 직면하고 있었다. 별로 돌파구가 보이지 않는 듯 했다.

그러던 중 우연히 Dave Schmidt 교수와 만나서 이 문제를 이야기했고, 얼마 후 파싱이론을 적용해보면 어떨까하는 제안을 해왔다. 쌓아놓은 도가 웬만큼 깊지 않고는 쉽게 생각해낼 수 없는 발상이었다. 그 순간. 아! 바로 이거다 싶었다. 오래 묵은 LR(k) 파싱알고리즘을 적용했더니 문제가 술술 풀렸다. 파싱이론을 정립해놓은 선구자들이 위대해 보였다.

실행중에 만들어내는 문자열의 구문구조를 이해할 수 있으니 이제 의미구조의 이해에 도전할 차례다.

논문심사평 중에서 좋은 말 몇 마디 붙이면...

하나,
This paper is an innovative step forward in string analysis with many applications. The use of parsing stack as an abstract domain has other static analysis applications in estimating values that can be characterized by LR(k) grammars.

둘,
First notion of "analyze-and-parse" style string analysis and use of the set of parsing stacks as the abstract domain.

]

"An Action Semantics Based on Two Combinators."
Kyung-Goo Doh and David A. Schmidt.
Lecture Notes in Computer Science, vol. 5700. September 2009. pp. 274-296.

[bibTex | pdf |

Jens Palsberg 교수로부터 이메일이 왔다. 금년이 Peter D. Mosses 교수의 60세 생일이 되는 해란다. 그래서 제자로서 스승의 평생 연구업적을 기릴 헌정논문집(festschrift)을 기획하고 있으니 적극적인 참여를 바란다고 했다. 나도 오래동안 쌓아온 인연이 있기에 뭔가 공헌하고 싶은 마음이 생겼다. 그래서 쓰게된 논문이다. 논문을 만들면서 "Mosses abstraction"이란 신조어도 만들었다. 정말 괜찮은 환갑 선물이다. 영향을 받은 한 학자로서 보답을 했다는 뿌듯함도 느낄 수 있었다.

]

"Improving Bug Triage with Bug Tossing Graphs."
Gaeul Jeong, Sunghun Kim, and Thomas Zimmermann.
Proceedings of the European Software Engineerin Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE'09). Amsterdam, The Netherlands. 2009. pp. 111-120.

[bibTex | pdf |

이광근 교수님의 지도 및 조언, 김성훈 박사님의 아이디어 및 추진력, Thomas Zimmermann의 경험 그리고 나의 실험이 잘 조화를 이루었던 연구다.

당시 “This is a quite good paper, based on a simple but clever idea, and with practical applicability.” 라는 논문 리뷰가 있었다. 리뷰가 이야기하는 것처럼 우리의 아이디어는 작고 단순했지만, 신선하고 분명한 방안을 제시함으로써 좋은 결과를 얻어낼 수 있었다. 나는 이 논문을 볼 때마다 버스에서 문득 떠오르는 생각들, 깊은 밤 잠들기 전에 번뜩이는 아이디어들을 소중하게 여겨야겠다고 새삼 다짐하게 된다.

이 논문은 내가 대학원에 입학해 처음 참여했던 논문이자 처음으로 채택되었던 논문이다. 또한 이 논문을 통해 처음으로 국제학회에서 발표할 기회를 가질 수 있었다. 이제 시작이라는 기분이 든다. 앞으로 더 많은 모험이 나를 기다리고 있다는 사실이 나를 설레게 한다.

]

"Test Coverage Metric for Two-staged Language with Abstract Interpretation."
Taeksu Kim, Chunwoo Lee, Soohyun Baik, Kwangkeun Yi, and Chisu Wu.
Proceedings of the 16th Asia-Pacific Software Engineering Conference (APSEC'09). Dec. 2009. pp. 301-308.

[bibTex | pdf |

multi-staged language에 대한 다양한 연구가 이루어지고 있지만 소프트웨어 공학의 주제와 접목시키는 연구는 새롭게 도전할 만한 부분이 많다. 이번에 test coverage를 확장하는 연구도 그러한 일환으로써 정적 분석을 활용하여 흥미로운 연구를 진행할 수 있었다. 현재 ‘09 Asia-Pacific Software Engineering Conference에 accept되어 많은 주목을 받고 있다.

키워드 : multi-staged language, test coverage, static analysis

]

"GeneShelf: A Web-based Visual Interface for Large Gene Expression Time-Series Data Repositories."
Bohyoung Kim, Bongshin Lee, Susan Knoblach, Eric Hoffman, and Jinwook Seo.
IEEE Transactions on Visualization and Computer Graphics. 15 (6). 2009. pp. 905-912.

[bibTex | pdf |

정보의 홍수로부터 생의학 연구자들을 구하자

최근 10여 년 동안 생의학 연구는 첨단 유전자 분석 기술의 발달로 눈부신 발전을 이루었다. 하지만 값비싼 첨단 장비를 이용하여 만들어낸 방대한 데이터들은 아직 효과적으로 공유되고 활용되지 못하고 있는 실정이다. 본 논문에서는 전 세계 생의학 연구자들이 유전자 칩 실험 결과를 공유하는 웹상의 데이터베이스에서, 유전자 발현에 관련된 방대한 시계열 자료를 효과적으로 열람/검색할 수 있는 시각적 인터페이스를 제시하였다. 특히 timeline과 bar chart를 자연스럽게 통합한 새로운 시각화 도구인 nTimeLines를 제안하여 다음과 같은 아주 긍정적인 리뷰 코멘트를 받았다.

“The described software is innovative and I have no doubt that it will be appreciated by its targeted audience of biologists working with database repositories of microarray data. I agree that a lightweight visualization tool is much needed.”

“The software provides a nice-looking and easy to use interface for visualizing the behaviour of top changing genes and pathways across treatments and time points.”

]

"Abstract Parsing for Two-staged Languages with Concatenation."
Soonho Kong, Wontae Choi, and Kwangkeun Yi.
Proceedings of the 8th International Conference on Generative Programming and Component Engineering (GPCE'09). Denver, Colorado, USA. 2009. pp. 109-116.

[bibTex | pdf |

다단계 언어는 서울대학교 프로그래밍 연구실에서 흥미를 가지고 꾸준히 연구하는 주제다. 2008년 11월에 있었던 첫 번째 ROSAEC 워크숍에서 도경구 교수님의 Abstract Parsing 발표를 듣고 우리는 이것을 이용해 다단계 언어의 분석에 도전해보기로 하였다.

본격적으로 연구를 시작하기에 앞서 사용할 무기를 이론적으로 정리하고 다듬기 시작했다. 3개월 정도에 걸쳐 Abstract Parsing을 요약 해석의 틀 안에서 이해하고 정리하여보니 이것만으로도 작고 단단한 결과물이 되었다. 이것을 GPCE'09 학회에 제출하였고 논문이 채택되었다.

아쉽게도 다단계 언어를 공략하는데 지금은 Abstract Parsing이 아닌 다른 방법을 사용하는 연구를 진행하고 있다. 하지만, 초보연구자인 우리(공순호, 최원태)는 목표를 향해 갈 때 신중하게 내디딘 발자국은 그것만으로 가치가 있다는 배움을 얻을 수 있었다.

키워드 : 요약 해석(Abstract Interpretation), 다단계 언어(Multi-staged Language), 프로그램 분석(Program Analysis) 구문 분석(Parsing), 문법(Grammar)

]

"PCC Framework for Program-Generators."
Soonho Kong, Wontae Choi, and Kwangkeun Yi.
Workshop on Proof-Carrying Code and Software Certification (PCC'09). Los Angeles, California, USA. 2009. pp. 18.

[bibTex | pdf |

한 연구의 응용에서 다른 연구에 대한 출발점을 이어준 연구이다.

Abstract Parsing을 이용한 다단계 언어 분석에 관한 논문(GPCE'09)을 마무리하고, 이를 이용한 PCC(Proof-Carrying Code) framework을 8월에 UCLA에서 열린 PCC 워크숍에 발표하였다. 발표를 마치고 토후쿠대학의 Naoki Kobayashi 교수로부터 질문을 받았다.

"프로그램이 만들어내는 스트링의 의미구조도 분석할 수 있느냐?"

깊이 생각해보지 않았던 부분을 정확하게 지적하는 질문이었고, 모르겠다고 답할 수밖에 없었다. 모르겠다고 대답한 것에 대한 부끄러움과 동시에 오기가 생겼다. 최원태 학생과 돌아오는 비행기 안에서 내내 해결방안을 토의하다가 괜찮은 방법을 찾았고 지금은 그것을 다듬고 있다.

문제 자체에 몰두하여 시야가 좁아졌을 때는 제삼자가 지나가듯 던져준 피드백이 큰 도움이 된다는 것을 배웠다.

키워드 : 요약 구문 분석(Abstract Parsing), 증명 전달 코드(Proof-Carrying Code), 다단계 언어(Multi-staged Language)

]

"Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation."
Hakjoo Oh.
Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'09). Seoul, Korea. December 2009. pp. 14-29.

[bibTex | pdf |

이 짧고 간단한 논문을 완성하기 위해서 거의 2년이 걸렸다.

2007년 가을, 우리 연구실에서 개발해오던 프로그램 분석기를 가지고 이리저리 뜯어보던 도중에, 분석을 잘 아는 사람들에게는 당연했지만 그 당시 아무것도 모르던 나에게는 도무지 상식적이지 않던 현상을 하나 발견하게 되었다. 내 나름대로의 방식으로 다시 구현하고 실험을 해보니 분석기의 성능이 몇 배 좋아지는 결과를 얻었다.

그 당시에는 이런 아이디어로 논문을 쓸 수 있는건지에 대한 감도 없던 시기였기에 별 생각없이 랩 세미나 시간에 발표를 했었는데, 교수님께서 논문으로 정리해보자고 하셨다. 아이디어 자체를 내 방식으로 정리하는것은 쉬웠지만, 이 아이디어가 기존의 관련연구들 속에서 어떤 위치에 있는지, 어떤 의미를 가지는지를 명확히 하며, 이 분야의 전문가들이 이해할수 있는 형식과 내용으로 표현하기에는 내공이 많이 모자랐다.

이 논문을 통해 교수님께 정말 많은 것을 배웠다. 커뮤니티의 사람들이 이해할수 있도록 내용을 구성하는 방법을 점차 알게되었고 영어 표현을 비롯한 논문의 마무리에도 감이 조금 잡히게 되었다.

]

"A Practical Memory Leak Detector Based on Parameterized Procedural Summaries."
Yungbum Jung and Kwangkeun Yi.
Proceedings of the 7th International Symposium on Memory Management (ISMM'08). ACM. 2008. pp. 131-140.

[bibTex | pdf |

우리 연구실에서 시간과 공을 들여 개발한 Sparrow의 한 엔진인 memory leak detector에 관한 논문이다. PLDI에 제출했었다가 성능은 좋은데 어떤 점이 새로운 것인지 잘 부각시키지 못해서 떨어졌었다. 이때 ISMM에 동시에 제출이 가능해서 새롭게 써서 제출하기로 했다. 처음으로 혼자 쓰는 논문은 교수님을 참으로 여러번 실망시켜 드렸었다. 이 논문은 교수님께 어떻게 논문을 써야 하는지 배우는 좋은 배움터였다. 논문 제출 마감 때는 교수님께서 안식년으로 미국에 계시고, 구정과 겹쳐서 처가가 있는 경주에서 얼마 없는 PC 방을 찾아 새벽에 돌아다니던 기억이 난다. CMU에 있는 박사과정 학생 Will Klieber의 자세한 교정을 생각하니 또 한번 고맙다.

PLDI에 떨어지고 나니 프로그램 버그를 찾는 도구들이 모두 모여서 겨루는 competition이 있으면 재밌겠다는 생각을 했었다. 프로그램에 memory leak이나 buffer overrun 같은 버그들을 심어놓고 프로그램을 공개하면 각자 다운받아 제한된 시간(일주일?) 안에 수단과 방법을 가리지 않고 누가 가장 많은 버그를 찾는 지를 겨루는 것이다. 성능이 뛰어난 분석기를 만드는 것이 논문에 새로운 아이디어를 제출하는 것보다 실제 현장에 있는 사람들에게는 더욱 절실하다고 본다.

]

"Efficient Embedded Code Generation with Multiple Load-Store Instructions."
Yunheung Paek, Minwook Ahn, Doosan Cho, and Taehwan Kim.
Software: Practice and Experience. 37 (11). 2007. pp. 1133-1159.

[bibTex | pdf |

소프트웨어는 프로세서 위에서 작동되어야 한다는 태생적 존재이기에 해당 하드웨어의 특성을 충분히 고려하지 않을 경우, 성능은 물론 코드의 정확성에까지 영향을 미칠 수 있다. 본 논문에서는 오늘날 프로세서들에서 종종 발견되는 Multiple Load/Store라는 하드웨어 명령어를 활용해서 보다 좋은 성능을 내는 코드를 효율적으로 생성하기 위한 컴파일러적 노력에 대해 이야기하고 있다.

]

"Goal-Directed Weakening of Abstract Interpretation Results."
Sunae Seo, Hongseok Yang, Kwangkeun Yi, and Taisook Han.
ACM Transactions on Programming Languages and Systems. 29 (6). 2007. pp. 39.

[bibTex | pdf]

"A Polymorphic Modal Type System for Lisp-Like Multi-Staged Languages."
Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno.
Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06). 2006. pp. 257-269.

[bibTex | pdf |

2년간의 긴 터널이었다. 2003년 여름부터 2005년 여름까지. 김익순 박사와 함께한 연구 결과였다.

김익순 박사가 어느 날 내게, "스스로 진화하는 프로그램에 대해서 연구해 보고 싶다"고 했다. 김박사는 LISP의 매크로 시스템에 매혹되 있었다. 내 답은, "그게 요즘 이야기되는 다단계 프로그래밍(multi-staged programming)이란 것이다. 우선 그러한 프로그래밍 언어의 좋은 static type system을 만들어 보자." LISP정도의 풀 다단계 언어를 위한 정교한 타입 시스템이 목표였다.

김박사는 곧 타입 룰을 가지고 왔다. 맞을 수 밖에 없다는 직감이 왔다. 그러곤 같은 연구를 앞서 한 대표 주자들을 접촉했다. Imperial의 Cristiano Calcagno을 2004년 1월 POPL에서 만나 이야기했다. 현재 다단계 언어의 타입시스템에서 제일 문제되는 것을 우리가 푼 것일 지 모른다는 확신을 얻었다. CMU의 Frank Pfenning을 2004년 APLAS에 초청강연 연사로 불러서, 김박사 일을 소개하고 김박사와 이야기 붙였다. Rice 의 Walid Taha와는 수시로 email하면서 우리 아이디어를 흘려보았다. 이러면서 좋은 결과를 우리가 만들어 냈다는 자신감이 쌓였다.

직관적인 타입 룰. 단순 타입 시스템의 안전성 증명은 수월했다. 다형타입시스템(polymorphic type system)으로 정교하게 확장했다. 그 안전성 증명은 지난했다. 이번엔 메모리 반응(imperative features)을 지원하도록 확장했다. 그 안전성 증명도 또 지난했다. "이렇게 계속 증명만 하고 시간이 가도 되는 건가요." "확인하지 않고는 굴 밖으로 나갈 수 없지 않겠냐." 거의 매주 토요일 오전에 만나서 증명을 확인해보고 수정했다. 토요일 점심을 참 많이 같이했다. 캠퍼스 솔밭식당으로 자주 같다.

김박사는 이렇게 논문없이 세월이 가도 되는지 초조해했다. 나는 소총 100발 보다는 미사일 1방이 더 가치있다고 했다.

POPL 2006을 위해 2005년 7월 논문을 제출했다. 2달여 후 억셉트 email이 왔다. 기뻤다. 박사논문을 POPL에 내고 두 번째였다. 특히, 연구동기부터 마무리까지 순수 국내 연구로 POPL에 낸 것이 자랑스러웠다. 이 소식을 받을 때 김익순 박사는 파리 Cousot그룹에서 1년간 방문연구를 막 시작한 중이었다.

논문 리뷰중:

"the article is a significant step towards a practical multi-stage extension of ML."

"I found this to be original and significant work, and paper is well written. Much effort has gone into presenting the exact relation of this work with related work, which helps view their contribution in a much clearer perspective."

"Overall, this looks like a clean design. It seems to have all of the components that one would want for multi-stage programming. I did not check the proofs carefully, but they seem plausible. I think that this paper should be published."

]

Team 2: Domain-specific analysis technology research & development

"TaintDroid: An Information-Flow Tracking System for Realtime Privacy Monitoring on Smartphones."
William Enck, Peter Gilbert, Seungyeop Han, Vasant Tendulkar, Byung-Gon Chun, Landon P. Cox, Jaeyeon Jung, Patrick McDaniel, and Anmol N. Sheth.
ACM Transactions on Computer Systems. 32 (2). June 2014. pp. 5:1-5:29.

[bibTex | pdf |

이 논문은 2010년에 게재한 TaintDroid OSDI 학회 논문을 확장한 저널 논문입니다. TaintDroid는 실시간으로 스마트폰 등의 기기에서 개인 정보의 흐름을 동적으로 추적하여 유출되는 것을 감지하는 시스템입니다. TaintDroid 연구는 모빌 보안 분야에서 중요한 연구로 인정되어 2014년 3월호 CACM Research Highlights에 선정되었습니다. 이 저널에서는 TaintDroid의 모든 것을 자세하게 설명하고, 새로운 Android 버전을 지원하기 위해 추가한 것들을 기술합니다. 그리고, 시간의 흐름에 따라 모빌 앱의 개인 정보 유출 정도를 분석한 결과도 추가로 제시합니다.

]

"Stability of the Max-Weight Protocol in Adversarial Wireless Networks."
Sungsu Lim, Kyomin Jung, and Matthew Andrews.
The 31st Annual IEEE International Conference on Computer Communications. 2012.

[bibTex | pdf |

본 연구는 2010년부터 정교민 교수님, Bell Labs, Murray Hill의 Matthew Andrews 연구원과 함께 진행하였습니다. 처음에는 SIGMETRICS 2011에 제출하였고 전체적인 평은 좋았으나 네 명의 reviewer중 한 명이 이 문제는 통신 네트워크보다 전산 이론에 더 가까운 문제로 보인다며 weak reject로 평가하여 최종 채택되지 않았습니다. Review를 감안하여 의미를 더 쉽게 설명하고 복잡한 증명은 technical report 등으로 넘겨서 증명 과정을 요약하는 등 수정을 거쳐서 통신•네트워크 분야 최고 학회인 INFOCOM 2012에 채택되었습니다. 관련 연구 결과를 제 6회 ROSAEC 워크샵에서 발표하기도 하였습니다.

]

"String Analysis as an Abstract Interpretation."
Se-Won Kim and Kwang-Moo Choe.
Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11). 2011.

[bibTex | pdf |

올해 3월, 예전의 아이디어를 다시 꺼내 쓴 논문입니다.

1. formalism의 일반화

원래는 제약된 형태의 pushdown automata를 이용했었습니다. 이들의 표현력에 관한 정리를 찾을 수 없었고, 이 automata에 대한 알고리즘이 이해하기 어려웠습니다. 오토마타 개론에서 배운 형태의 pushdown automata를 이용하여 알고리즘을 다시 썼는데, 프로그램 분석을 하는 사람에게 더 이해하기 쉬운 형태가 되었습니다.

2. 타입 기반 분석 대신 요약해석을 적용

요약해석에 대해 많이 들어서 알고 있다고 생각했었는데, 새로운 도메인을 만드는 과정에서 제가 요약해석을 제대로 알지 못함을 깨달았습니다. 요약해석에 정통하기 위해 Cousot의 논문을 보며 주요 명제 하나하나를 증명하며 공부했습니다. 분석 도메인 요소의 표현력이 문맥자유언어 또는 그 이상이어서 좋은 성질의 도메인을 기대하기 어려울꺼라 생각했었습니다.

하지만, 수차례 수정을 거듭하면서 complete lattice가 얻어졌고, 가장 classical한 경우인, complete lattice간의 Galois 연결을 만들수 있었습니다.

VMCAI 논문 제출을 앞두고 약 한달간은 증명에 집중했습니다. 막히는 곳이 많았고, 물어볼 곳도 없어 답답했습니다. 이 논문 본문에는 나오지 않지만 증명에서 가장 핵심적인 보조 정리가 하나 있는데, 이 명제를 찾는 것이 가장 힘들었습니다. 증명을 위아래에서 접근하며 그럴싸한 명제를 만들고, 증명하다 실패하는 과정을 반복하였습니다. 실패를 거듭하던 며칠간은 밥도 잘 넘어가지 않았고, 실제로 몸무게도 줄었었습니다.

논문을 쓰는 동안 지도 교수님께서 두 번의 큰 수술로 부재중이셔서 조언을 얻지 못했지만 그 만큼 제게는 많은 공부가 된 논문이었습니다.

]

"Program analysis for overlaid data structures."
Oukseh Lee, Hongseok Yang, and Rasmus Petersen.
Proceedings of the 23rd international conference on Computer Aided Verification (CAV'11). Princeton, NJ, USA. 2011.

[bibTex | pdf |

영국에 연구년을 가서 처음 맡은 연구이다. 양홍석 박사가 2년 정도 Rasmus Petersen과 작업하였는데도 분석하지 못하는 시스템 코드가 있다고 하였다. 문제는 겹쳐진 자료구조였다. 겹쳐진 자료구조를 분리해서 각각 분석하는 아이디어까지는 좋은데 각각 분석하면서 놓치는 정보가 있어 검증이 되지 않는다는 것이었다. 필요한 정보를 놓치지 않도록 지역 (region) 정보를 유지하고 이용하도록 하였더니 문제없이 검증이 되었다. 때에 맞추어 CAV에 제출하였고 문제없이 게재되었다. 연구 결과가 CAV에 "문제없이" 게재될 수 있었던 큰 이유 중 하나는, 양홍석 박사가 이 결과에 대한 세미나를 여기저기서 하여 내용을 미리 널리 알렸다는 것이다. 이 논문을 심사할 가능성이 높은 사람들은 양홍석 박사의 세미나를 통해 이미 내용을 알고 있었고, 그렇기 때문에 논문의 사소한 문제가 아닌 깊은 심사가 가능했고, 결과적으로 높은 점수를 획득할 수 있었다. 연구 결과의 소통이 중요함을 새삼 느꼈다.

]

"Nonlinear Estimation for Spacecraft Attitude using Decentralized Unscented Information Filter."
Jonghee Bae and Youdan Kim.
Proceedings of the International Conference on Control, Automation and Systems (ICCAS'10). 2010.

[bibTex | pdf |

“S/W는 오류검증기, H/W는 고장진단 알고리즘”

소프트웨어 오류 검증기는 말 그대로 S/W 개발자가 만든 코드의 오류를 찾아낸다. 그렇다면, 하드웨어에 오류(혹은 고장)가 있다면 어떻게 해야 할까? 현재, 이 이야기의 저자가 몸담고 있는 항공분야에서는 고장이 인명적, 비용적 측면에서 큰 손실을 가져올 수 있다.

물론 소프트웨어 검증기를 통해 S/W의 오류를 검증하게 되면 고장의 확률을 낮출수 있다. 하지만 하드웨어에 고장이 발생한다면, 이를 진단하고 분리하는 알고리즘이 추가로 필요하다.

이 논문은 틸트로터 스마트 무인항공기가 대상이며 항공기의 자세를 측정하는 센서에 고장이 발생할 경우, 센서고장을 검출하는 알고리즘에 대해 다룬다. 소프트웨어 검증기에 하드웨어 고장진단 알고리즘이 추가된다면, 정말로 ‘smart’한 틸트로터 스마트 무인항공기가 될 수 있을 것이다.

]

"Task Assignment of Multiple UAVs using MILP and GA."
Hyunjin Choi, Joongbo Seo, and Youdan Kim.
Journal of the Korean Society for Aeronautical & Space Sciences. 38 (5). 2010. pp. 427-436.

[bibTex | pdf |

본 논문은 2010년 5월 한국항공우주학회지에 개제된 논문입니다. 항공우주학회지는 항공우주분야에서 가장 많은 논문이 개제되는 국내 논문지입니다. 본 논문은 다수의 목표물과 다수의 임무가 존재하는 상황에서의 다수 무인항공기의 임무할당 문제를 다룹니다. 임무할당의 문제는 문제의 크기가 커질수록 계산시간이 급격히 증가하기 때문에 문제를 효율적으로 풀기 위해서 근사화 또는 발견적인 방법을 사용합니다. 본 논문에서는 임무할당 문제를 혼합정수 선형계획 문제로 정식화하고, 혼합정수 선형계획법과 유전 알고리듬으로 해를 구하였습니다.

]

"Malware Detection based on Dependency Graph using Hybrid Genetic Algorithm."
Keehyung Kim and Byung-Ro Moon.
Proceedings of the Genetic and Evolutionary Computation Conference (GECCO'10). 2010.

[bibTex | pdf |

본 연구실에서는 2009년 7월 GECCO 컨퍼런스에서 발표된 바이러스 자동 생성 유전알고리즘 논문을 접하고, 변형 바이러스에 대한 대응책이 시급히 필요하다는 판단에 작년 8월부터 본 연구에 착수하였다. 약 5~6개월 정도의 연구결과를 집약한 본 논문이 2010년 7월 GECCO 컨퍼런스에서 발표되었다.

기존의 바이러스 감지 알고리즘들은 피해가 보고된 후 바이러스를 수배하여 이에 대한 백신을 만드는 방식이다. 본 연구에서는 알려지지 않은 다형변이로 만들어지는 바이러스를 감지하기 위해, 바이러스 검출 문제를 Maximum Subgraph Isomorphism 문제로 표현하고, 혼합형 유전 알고리즘을 사용하여 경험하지 않은 바이러스에 대해서 제로데이에 감지할 수 있도록 하는 것이다.

직접 제작한 바이러스를 포함한 총 18개의 다형변이 바이러스 데이터에서 기존 백신 소프트웨어의 검출률과 연구실에서 제안한 방법의 검출률의 비교를 수행했다. 그 결과 예상대로 기존 백신 소프트웨어들은 새로운 변형 바이러스의 검출에 취약한 모습을 보여주었고, 어느 백신도 본 연구실에서 제안한 방법의 검출률에 미치는 결과를 보여주지 못했다.

비록 아직까지는 작은 크기의 초보 수준의 다형변이 바이러스를 이용한 감지를 성공적으로 수행한 것이지만, 이를 바탕으로 강력한 감지 알고리즘을 만들고, 실험을 위한 바이러스를 자동으로 생성하는 알고리즘을 개발하며, 유전 알고리즘의 속도 문제를 해결하기 위한 다양한 접근법을 개발 및 시도하고 있다.

언제가 될 지 확언할 수는 없지만 현재의 바이러스들과는 전혀 성격이 다른 다형변이 바이러스들이 대량으로 출현하는 시기가 올 것이다. 만일 바이러스 안에 다형변이를 생성하는 기능이 들어간다면 걷잡을 수 없을 정도의 속도로 출현할 가능성도 있다. 본 연구가 다형변이 바이러스들을 감지하는데 큰 기여를 하기를 기대해본다.

]

"Automatic Reproduction of a Genius Algorithm: Strassen's Algorithm Revisited by Genetic Search."
Seunghyun Oh and Byung-Ro Moon.
IEEE Transactions on Evolutionary Computation. accepted.

[bibTex | pdf |

알고리즘으로 천재에 맞서 보자

스트라센! 듣기만 해도 주눅이 드는 이름이다. 행렬의 곱셈 연산 시간은 무조건

이라는 고정관념을 깨버려 20세기의 명사중 한 사람이 된 천재수학자 스트라센. 사람들이 그의 알고리즘에 놀라는 것은 어떻게 그 방대한 문제 공간에서 그런 해를 찾아내었느냐 하는 것이다. 나에게 그를 옆자리에 앉혀놓고 경쟁을 하라고 한다면 찻집이나 하나 차려 여생을 편히 사는 길을 택하겠다.

10여년 전부터 유전 알고리즘을 이용하여 스트라센의 알고리즘을 재현하는 것을 목표로 작업을 시작했다. 학회에서 만난 외국인 동료들에게 그 작업을 하고 있다고 하니까... “... looks interesting...” 재미있어 보이지만 되겠냐? 이런 표정들이다. 그래 쉽지는 않겠지. 그렇지만 우리 전공이란 게 밑져봐야 재료비가 드는 것도 아니고... 지가 아무리 천재라도 사람인데... 우리에겐 컴퓨터와 공간탐색 기법이 있지 않은가? 결과는... 실패, 또 실패... 훌쩍 5~6년.

이러던 어느날, 오승현 학생으로부터 흥분이 담긴 이메일이 날아왔다. “교수님, 찾았어요.” 스트라센과 같은 성능의 알고리즘이 드디어 발견되다! 좀 더 나가니.. 스트라센의 알고리즘도 발견. 현재까지 대칭과 중복을 다 제외하고 적어도 608개의 서로 다른 스트라센급 (

) 알고리즘을 발견하였다. 공간탐색 알고리즘의 위력에 새삼 놀란다.

요즘은 스트라센의

행렬곱을 벗어나

행렬을 이용해서 더 좋은 알고리즘이 있는지 찾는 작업을 하고 있다. 10여년 전에 처음 시작하던 때보다 더 난감>하고, 벽이 높다. 그렇지만 시간의 문제지 나 죽기 전에는 될 것이다. 지금까지 해온 것들이 정도의 차이가 있을 뿐 주로 그랬으니까... 우리는 그만한 천재가 아니지만 천재를 누를 수 있는 문화적 도구를 갖고 있다. 이런 것이 리처드 도킨스가 말한 ‘확장된 유전형’이겠지.^^

]

"Decentralized Task Assignment for Multiple UAVs Using Genetic Algorithm with Egotiation Scheme Approach."
Hyunjin Choi, Joongbo Seo, and Youdan Kim.
Proceedings of the Asia-Pacific International Symposium on Aerospace Technology (APISAT'09). Gifu, Japan. November 2009.

[bibTex | pdf |

본 논문은 2009년 11월 일본 기후에서 개최된 APISAT(아시아 태평양 지역 항공우주 기술 심포지움)에서 발표된 논문입니다. 이 심포지움은 한국항공우주학회, 일본항공우주학회, 중국항공우주학회, 호주항공우주학회가 공동으로 항공우주 기술에 대한 기술교류의 장으로 개최되는 학회로 주로 4개국에서 항공우주 분야의 논문을 발표하는 학회입니다.

본 논문은 다수 무인기가 임무를 효율적으로 수행할 수 있도록 유전자 알고리듬을 이용하여 임무를 할당하도록 하는 내용을 다룬 논문으로, 발표 당시 관련 연구를 수행하고 있는 일본 연구자들로부터 다양한 질문을 받으며 주목을 받았습니다.

]

"Local Rules for Global MAP: When Do They Work."
Kyomin Jung, Pushmeet Kohli, and Devavrat Shah.
Advances in Neural Information Processing Systems. 2009. pp. 871-879.

[bibTex | pdf |

이논문의 내용은 정교민 교수의 박사과정 thesis의 중요한 아이디어 중 하나를 제시하고 있습니다. 즉, 주어진 그래프가 특정한 구조(polynomially growing)를 가지면 그곳에서의 optimization을 local하게 수행하여도 global한 optimal soltion의 approximation이 된다는 내용입니다.

]

"A Hybrid Genetic Algorithm for a Variant of Two-Dimensional Packing Problem."
Jin Kim and Byung-Ro Moon.
Proceedings of the 11th Annual Conference on Genetic and Evolutionary Computation. ACM. 2009. pp. 287-292.

[bibTex | pdf |

본 논문에서 다루는 문제는 2008년 GECCO 컨퍼런스(Evolutionary Computation 분야에서 대표적인 컨퍼런스)의 콘테스트 문제였다. 문제는 20×20 크기의 행렬을 채우는 것이었고, 이 때 가장 높은 점수를 얻는 것이 목적이다. 우리 연구실 학생 몇 명이 도전했고, 그 학기 대학원 유전 알고리즘 강좌 과제로 제시하여 약 80여명의 수강생도 참가하였다.

연구실 학생들과 수강생들간의 경쟁을 기대한 것이었는데, 초기부터 다양한 아이디어가 나오며 수강생들이 좋은 점수를 내었다. 그러나 후반부로 갈수록 연구실 학생들이 높은 수준의 아이디어를 제시하여 결과가 역전되었다. 콘테스트 홈페이지에 참가팀의 목록이 점수순으로 게시되었다. 우리 연구실에서는 다른 참가팀보다 압도적으로 높은 점수의 해를 찾아두고 마감 직전에 제출하였다. 다행이도 2위팀보다 근소하게 높은 점수로 우승을 차지할 수 있었다.

]

"Controller Design for UAV Formation Flight Using Consensus Based Decentralized Approach."
Joongbo Seo, Chaeik Ahn, and Youdan Kim.
Proceedings of the AIAA Infotech@Aerospace Conference. Seattle, WA, USA. April 2009.

[bibTex | pdf |

본 논문은 2009년 4월 미국 시에틀에서 개최된 AIAA Infotech@Aerospace Conference 에서 발표된 논문입니다. AIAA는 American Institute of Aeronautics and Astronautics( 미국항공우주학회)로서 항공우주 분야에서 매우 다양한 분야의 논문들이 많이 제출되는 학회입니다. 요즘 항공우주분야에서의 추세가 무인항공기의 자율비행에 대한 연구로 본 논문은 다수의 무인항공기의 군집비행에 관련된 연구입니다. 무인항공기의 자율비행은 비행제어 소프트웨어가 중요하므로 향후 소프트웨어 분야와의 접목이 더욱더 중요해 질 것으로 판단됩니다.

]

"Tightly-Coupled Spatial Database Features in the Odysseus/OpenGIS DBMS for High-Performance."
Kyu-Young Whang, Jae-Gil Lee, Min-Soo Kim, Min-Jae Lee, Ki-Hoon Lee, Wook-Shin Han, and Jun-Sung Kim.
GeoInformatica. 2009. pp. 1-22.

[bibTex | pdf |

본 논문은 Odysseus/OpenGIS의 공간 밀결합 기술에 관한 것이다. 본 연구실에서 19 년에 걸쳐 개발한 Odysseus/OpenGIS는 공간, 비공간 데이터를 유기적으로 통합 관리하는 객체관계형 공간 DBMS로, 공간 색인, 공간 연산자, 공간 질의 처리기를 DBMS 내에 밀결합시킴으로써 공간 데이터에 대한 높은 일관성과 빠른 공간 질의 처리 속도를 제공한다.

키워드: Tight-coupling, Object-relational DBMSs, Spatial DBMSs, Geographical information system (GIS)

]

"A Lagrangian Approach for Multiple Personalized Campaigns."
Yong-Hyuk Kim, Yourim Yoon, and Byung-Ro Moon.
IEEE Transactions on Knowledge and Data Engineering. 20 (3). 2008. pp. 383-396.

[bibTex | pdf]

"Scalable Shape Analysis for Systems Code."
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O'Hearn.
Proceedings of the International Conference on Computer Aided Verification (CAV'08). Princeton, NJ, USA. July 2008. pp. 385-398.

[bibTex | pdf |

방학동안 양홍석 박사가 있는 영국으로 가서 공동 연구한 것이다. 양홍석 박사의 고민이 모양 분석기(shape analysis)의 성능이였다. 잘 알려져 있는 기술들을 활용하여 매일 속도를 반으로 줄였고 결과적으로 몇 백배 빨라진 경우까지 생겼다. 결과는 좋았지만 새로운 기술이 없어 논문 쓰기가 어려웠다. PLDI에 한 번 떨어지고 나서, 마이크로소프트에 있는 Byron Cook을 영입했다. Byron Cook의 현란한 글솜씨와 필요한 것/필요없는 것 골라내는 기술, 감탄스러웠다. 바로 CAV에 게재 승인을 받았다. 글 쓰는 것, 얼마나 중요한 기술인지!

키워드: 모양 분석 (shape analysis), 프로그램 분석 (program analysis), 성능 (performance)

]

"A Hybrid Neuro-Genetic Approach for Stock Forecasting."
Yung-Keun Kwon and Byung-Ro Moon.
IEEE Transactions on Neural Networks. 18 (3). May 2007. pp. 851-864.

[bibTex | pdf]

"Trajectory Clustering: A Partition-and-Group Framework."
Jae-Gil Lee, Jiawei Han, and Kyu-Young Whang.
Proceedings of the 2007 ACM SIGMOD International Conference on Management of Data. ACM. 2007. pp. 604.

[bibTex | pdf]

"The Dynamic Predicate: Integrating Access Control with Query Processing in XML Databases."
Jae-Gil Lee, Kyu-Young Whang, Wook-Shin Han, and Il-Yeol Song.
The Very Large Data Base Journal. 16 (3). 2007. pp. 371-387.

[bibTex | pdf]

"Convex Optimization Algorithms for Active Balancing of Humanoid Robots."
Juyong Park, Jaeyoung Haan, and Frank C. Park.
IEEE Transactions on Robotics. 23 (4). 2007. pp. 817.

[bibTex | pdf |

로봇에게 균형감각을 심어주자

현대인들의 필수품이 된 컴퓨터처럼, 미래에는 인간을 닮은 휴머노이드 로봇이 우리의 삶에 아주 가까이 있을 것이다. 집안에서 집안일을 돕기도 하고, 같이 외출하여 무거운 짐을 들어주기도 하고 말이다. 그런데 이런 휴머노이드 로봇이 균형 감각이 없어 잘 넘어진다면 어떨까? 만약, 버스를 타고 가다가 급출발한 버스 때문에 이 비싼 로봇이 넘어져서 고장나거나 인명 피해라도 낸다면 그 누가 이 로봇과 함께 하겠는가?

이러한 휴머노이드 로봇에게 ‘균형감각을 심어주자.’라는 목표로 최적화 기반의 로봇 동작 안정화 알고리즘을 연구하기 시작했다. 주변 환경의 변화에도 스스로 넘어지지 않고 균형을 잘 잡아 넘어지지 않을 수 있는 그런 균형감각을 부여해주는 것이다. 일반적으로 이런 휴머노이드 로봇의 안정성에 관련한 제약조건들은 복잡한 비선형 형식으로 표현된다. 문제는 이러한 복잡한 비선형 제약조건들은 가진 최적화 문제는 실시간으로 풀어나가기 힘들뿐더러 전역 최적해를 구해준다는 보장이 없다. 다시 말해, 아무리 좋은 균형 잡기 알고리즘이라 하더라도 아주 고사양의 컴퓨터가 로봇에 탑재되어 있지 않으면 무용지물이라는 것이다.

그러던 어느 날, 이 복잡한 최적화 문제를 볼록 최적화(convex optimization) 문제로 정의 할 수 있다는 사실을 박주용 학생이 알아냈다. 어떤 최적화 문제를 볼록 최적화 문제로 정의 할 수만 있다면, 전역 최적해를 구할 수 있음이 보장될 뿐 아니라, 수치적 계산 효율도 상당히 좋아지게 된다. 이렇게 새로 정의한 균형잡기 볼록 최적화 문제를 시뮬레이션 해 본 결과, 25자유도를 갖는 휴머노이드 로봇에 대해 균형 잡기 알고리즘이 실시간으로 동작한다는 사실을 보였다.

논문을 마무리하면서, 이 균형잡기 알고리즘이 다양한 시나리오에서 성공적인 실시간 균형잡기 성능을 내는지 테스트해 보았다. 우리 태권도 동작의 앞 차기 동작과 마치 버스가 급출발할 때처럼 가속되는 바닥위에서의 균형잡기 동작을 테스트하였다. 그 결과 마치 사람이 넘어지려고 할 때 양팔 및 다른 발을 벌려서 균형잡는 것과 유사한 동작을 취하는 것을 볼 수 있었다. ‘역시 인간은 본능적으로 많은 것을 터득하고 있구나’라고 생각해본다.

]

"A Practical String Analyzer by the Widening Approach."
Tae-Hyoung Choi, Oukseh Lee, Hyunha Kim, and Kyung-Goo Doh.
Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS'08). Sydney, Austrailia. November 2006. pp. 374-388.

[bibTex | pdf |

한양대에 와서 도경구 교수님과 협업한 첫 사례. 최태형 학생이 새로운
형태의 문자열 분석기를 개발했는데 시간이 흘러도 논문으로 쓰질 못하고
있었다. publish or perish! 때마침 APLAS 학회가 있어 여기다 내야겠다 작정하고 며칠만에 논문을 생산했다. 최태형 학생과 계속 토론하여 작성하고, 김현하 학생이 실험 결과 만들고, 도경구 교수님이 작성된 논문의 표현을 교정하고. 연구는 천재가 아닌 경우 '협업 시스템'의 결과다.

키워드: 문자열 분석 (string analysis), 정규 표현식 (regular expression), 넓히기 (widening), 프로그램 분석 (program analysis)

]

"Multicampaign Assignment Problem."
Yong-Hyuk Kim and Byung-Ro Moon.
IEEE Transactions on Knowledge and Data Engineering. 18 (3). 2006. pp. 405-414.

[bibTex | pdf]

"Transform-Space View: Performing Spatial Join in the Transform Space Using Original-Space Indexes."
Min-Jae Lee, Kyu-Young Whang, Wook-Shin Han, and Il-Yeol Song.
IEEE Transactions on Knowledge and Data Engineering. 18 (2). 2006. pp. 245-260.

[bibTex | pdf]

"A Formal Framework for Prefetching Based on the Type-Level Access Pattern in Object-Relational DBMSs."
Wook-Shin Han, Kyu-Young Whang, and Yang-Sae Moon.
IEEE Transactions on Knowledge and Data Engineering. 2005. pp. 1436-1448.

[bibTex | pdf]

"Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis."
Oukseh Lee, Hongseok Yang, and Kwangkeun Yi.
Proceedings of the European Symposium on Programming. Edinburgh, UK. April 2005. pp. 124-120.

[bibTex | pdf |

박사과정을 졸업하고 서울대에서 박사후연구원을 하는 도중 양홍석 박사와
함께 작업한 논문이다. 이광근 교수님의 '문법(grammar)'을 활용하자고 하는 아이디어 제안, 양박사와의 분석기 설계, 나의 구현까지 3~4달만에 순식간에 연구가 이루어졌다. '함께 연구한다'는 것의 즐거움과 힘을 느끼게 해 주었다.

키워드: 모양 분석 (shape analysis), 문법 (grammar), 프로그램 분석 (program analysis)

]

Team 3: Theory and innovative analysis technology research & development

"A Proof System for Separation Logic with Magic Wand."
Wonyeol Lee and Sungwoo Park.
Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14). 2014. pp. 477-490.

[bibTex | pdf |

2008년 소프트웨어무결점연구센터의 탄생과 함께 분리논리를 이용한 소프트웨어 검증 도구에 관한 연구를 본격적으로 시작하였다. 당시 분리논리에 관한 연구는 대부분 곱하기 연산자 하나만을 이용하는 형태였다. 나는 곱하기 연산자 뿐 아니라 마술봉 연산자도 함께 지원하는 검증 도구를 개발하겠다는, 당시로서는 아무도 시도하지 않았던, 굉장히 모험적인 연구 주제를 장기적인 목표로 택하게 되었다.

연구 계획은 세 단계로 이루어졌다. 첫 번째 단계는 분리논리의 이웃이라고 할 수 있는 Boolean BI 논리의 증명체계를 완성하는 것이고, 두 번째 단계는 분리논리 자체의 증명체계를 완성하는 것이고, 마지막 단계는 완성한 증명체계를 이용하여 실제 검증 도구를 구현하는 것이었다. Boolean BI 논리는 분리논리의 모델이기 때문에 분리논리를 다루기 전에 시도해 볼 수 있는 연습문제라고 볼 수 있다. 그렇지만 당시 Boolean BI의 논리체계에 대한 해답이 없었고 오히려 멀쩡한 논리체계는 없을 것이라는 추측만이 있었기 때문에 첫 번째 단계마저 성공적으로 끝낼 수 있을지 확신은 없었다.

첫 번째 단계를 시작하며 우선 Boolean BI보다 더 쉬운 BI 논리에 대한 자동증명기를 개발해 보기로 했다. 어느 정도 결과가 나온 뒤 더 지체할 수 없어서 Boolean BI 문제로 바로 넘어갔는데 예상했던 것보다 훨씬 문제가 어려워서 난감했다. 결국 2010년 여름 나는 이 문제를 풀 수 없다는 우울한 결론과 Boolean BI에 멀쩡한 증명체계는 없을 것이라는 비관적인 결론을 내리고 PSPL 워크샵에 이러한 내용으로 논문을 발표한 뒤 연구를 접게 되었다. 당시 나만 믿고 몇 년간 따라와 준 종현이에게 연구를 포기하자는 말을 했을 때 지도교수로서 너무 참담했고 정말 미안했다.

그 뒤 나는 Boolean BI 문제에 대해서 생각하지 않았지만 종현이는 여전히 문제에 대해서 생각하고 있었다. 사실 이 문제에 몇 년을 투자했기 때문에 문제를 그만 버리기도 어려웠을 것이다. 그런데 2010년 겨울 우연한 기회에 다시 얘기를 하면서 그 때 종현이가 생각하던 아이디어가 문제의 답이라는 것을 직감했다. 당시 종현이는 자기가 생각하던 방법이 문제의 답이라는 것을 깨닫지 못하고 있었기 때문에 문제의 답을 찾았다고 칭찬하면서 흥분하던 나를 잘 이해하지 못했었다. 이후 Boolean BI 문제를 다시 풀기 시작했고 곧 증명체계를 완성했다. 2011년 제출한 POPL 논문은 떨어졌는데 구현이 없다는 것이 이유였다. 이후 정봉이가 연구에 합류했고 함께 Boolean BI 증명기를 완성한 뒤 2012년 다시 POPL에 논문을 제출해서 게재 승인을 받았다.

2013년부터 두 번째 단계 연구를 본격적으로 시작했다. 혼자서 문제를 풀고 있어서 진척이 별로 없던 중 3월 초에 원열이가 찾아와서 나와 연구를 하고 싶다고 말했다. 원열이는 나의 학부지도생으로서 2학년때 다른 교수의 지도를 받아서 이미 국제학회에 논문을 발표한 적이 있었다. 분리논리 증명체계 문제를 소개해 주면서 문제의 중요성 때문에 해결만 하면 확실하게 POPL 논문이 될 거라고 말해 주었다. 그러나 어려운 문제이기 때문에 나도 풀 수 있을지 확신이 없고 그래서 결과물이 아예 없을 수도 있지만 그래도 도전하고 싶으면 합류하라고 얘기했다. 원열이는 며칠 뒤 도전하겠다는 이메일을 나에게 보내왔다.

이후 원열이와 본격적으로 분리논리 증명체계 문제에 도전했다. 첫 한 달은 전산논리의 기초를 원열이에게 집중적으로 가르치면서 보냈다. 그 다음 달부터 문제를 함께 풀기 시작했는데 원열이는 내가 몇 달 동안 생각해 오던 방법과는 다른 접근 방법을 제시했다. 원열이의 접근 방법은 결국 문제가 있는 것으로 결론 났지만, 이후 두 방법을 절충하여 문제 해결의 틀이 서서히 갖추어졌다. 그러던 중 원열이가 문제 해결에 가장 중요한 발견을 했고 결과를 완성한 뒤 7월에 POPL에 논문을 제출하였다. 예상대로 논문은 무난하게 POPL에 게재되었다.

두 편의 POPL 논문을 쓰면서 함께 공부한 학생들로부터 논문 내용 이상의 많은 것을 배웠다. 종현이의 끈기가 없었더라면 PSPL 워크샵 논문을 끝으로 이 연구는 끝이 났을 것이며, 정봉이의 성실함이 없었더라면 아직도 첫 번째 단계에서 뒹굴고 있을지도 모르겠다. 원열이와 함께 공부한 다섯 달은 나에게도 벅찬 경험이었다. 비록 전산논리 기초도 없는 학부생이었지만 배움에 대해서 겸손하고 공부에 대해서 열의를 갖춘 학생과 함께라면 짧은 시간에라도 불가능할 것 같은 결과를 만들어 낼 수 있다는 것을 몸으로 체험했다.

2015년 소프트웨어무결점연구센터의 마지막 워크샵에서는 세 번째 단계 연구 결과를 보여주고 싶다.

]

"Ask the Mutants: Mutating Faulty Programs for Fault Localization."
Seokhyeon Moon, Yunho Kim, and Moonzoo Kim.
7th IEEE International Conference on Software Testing, Verification and Validation(ICST'14). 2014.

[bibTex | pdf |

“그래서 버그가 있는 건 개발하신 기술로 잘 찾을 수 있는 걸 알겠어요. 그런데 그 버그를 고치려면 대체 어딜 고쳐야 하는거죠?” 개발자 대상 강연에서 한 개발자가 던진 질문을 듣고 디버깅 문제에 대한 고민이 시작되었다. 지난 몇 년간 집중했던 테스트 연구에 어느 정도 성과를 보이고 나니 디버깅이라는 재미있는 문제가 눈에 보이기 시작했다.
첫 시도는 정확한 버그 위치를 찾기 위해 기존에 널리 사용하고 있는 통계 분석 방법의 공식을 최적화하는 것이었다. 기존 방법은 통계 분석 기법에만 집중하고 디버깅 대상이 되는 프로그램에 집중하지 않았던 점을 노려 통계 분석이 더 정확해지도록 프로그램을 변환하는 기법을 개발했다.
리뷰 결과는 처참했다. 한 리뷰어는 통계 분석을 사용한 버그 위치를 찾는 연구는 이제 끝(dead end)라고 했고 또 다른 리뷰어는 이런 기법이 정말 개발자에게 의미가 있으려면 실제 버그가 있는 구문이 TOP 10 안에 있어야 한다고 했다. 기존 기법에서 10~20% 성능을 높이는 것은 이제 더 이상 의미가 없다는 분위기가 이미 형성되어 있었다.
그 이후 한참을 고민하다 나온 게 변이 분석(mutation analysis)을 활용한 버그 위치 찾는 기술이다. 어떻게 할까 고민 중에 1저자인 석현군이 아이디어를 냈다. ‘그럼 프로그램 변이를 통해 버그를 더 심어보면 어떨까요?’ 버그가 없는 프로그램 구문을 수정하면 해당 구문에 버그를 만든 효과가 난다. 프로그램에 버그가 추가 되었기 때문에 기존에 성공한 테스트도 실패하게 될 것이다. 반면 버그가 이미 있는 프로그램 구문을 수정할 경우는 기존에 성공한 테스트는 큰 영향을 받지 않을 것이다. 운이 좋다면 변이로 수정을 한 게 버그를 고치는 효과를 내어 기존에 실패한 테스트들도 성공한 테스트가 될 수 있다.
실험 결과는 놀라웠다. 수 만 줄에 달하는 유닉스 유틸리티 flex, grep, gzip, sed 등에 적용하니 실제 버그 위치를 1~3등 안에 들어오도록 정확하게 찾아냈다. 새 논문에 대한 리뷰어 반응도 좋았고 특히 다음 리뷰 문장이 마음에 들었다. “The new fault localization technique is highly effective, novel, and based on sound and intuitive principles.”

]

"A Theorem Prover for Boolean BI."
Jonghyun Park, Jeongbong Seo, and Sungwoo Park.
Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13). 2013. pp. 219-232.

[bibTex | pdf |

]

"A New Approach for Processing Ranked Subsequence Matching Based on Ranked Union."
Wook-Shin Han, Jinsoo Lee, Yang-Sae Moon, Seung-won Hwang, and Hwanjo Yu.
Proceedings of the 37th ACM SIGMOD International Conference on Management of Data (SIGMOD'11). 2011.

[bibTex | pdf |

순위를 지원하는 서브시퀀스 매칭은 데이터 시퀀스로부터 주어진 질의 시퀀스와 가장 유사한 서브시퀀스 상위 k개를 찾는 것이다. 기존에 제안된 HLMJ방법은 최소 거리 매칭 윈도우 쌍(minimum distance matching window pair-MDMWP)라는 개념과 전역 우선순위 큐를 사용하여 이 문제를 풀었다. MDMWP의 개념을 사용함으로써 HLMJ방법은 하한 거리값을 사용하여데이터 시퀀스에 많은 불필요한 접근을 제거할 수 있다. 그러나 우리는 HMLJ방법이 중요한 유형의 질의에 대해서 심각한 성능의 오버헤드를 야기함을 알아냈다. 이 논문에서, 우리는 순위를 지원하는 서브시퀀스 매칭을 순위를 지원하는 합집합 질의로 봄으로써 이 문제를 풀기위한 새로운 체계적인 프레임워크를 제안한다. 특히, 우리는 matching subsequence equivalence class(MSEQ)의 개념과 MSEQ-distnace라고 불리는 새로운 lower-bound 를 제안한다. HLMJ방법의 성능 문제를 완전히 제거하기위해서, 우리는 또한 cost-aware density-based scheduling 기법을 제안하고, 밀도와 우선순위 큐의 비용을 둘다 고려하도록 한다. 많은 실제 데이터 셋을 가지고 한 광범위한 실험의 결과는 제안된 알고리즘이 HLMJ와 adapted PSM보다 뛰어난 성능을 나타냄을 보였고, 최신의 연구인 non-monotonic distnace 함수를 지원하는 색인 기반 병합 알고리즘보다 수백배에서 수천배까지 더 좋았다.

]

"iGraph in Action: Performance Analysis of Disk-Based Graph Indexing Techniques."
Wook-Shin Han, Minh-Duc Pham, Jinsoo Lee, Romans Kasperovics, and Jeffrey Xu Yu.
Proceedings of the 37th ACM SIGMOD International Conference on Management of Data (SIGMOD'11). 2011.

[bibTex | pdf |

그래프는 화학 구조식이나 단백질 상호작용, 그림, 그리고 프로그램 종속성 등과 같이 복잡한 구조를 모델링하는 강력한 방법을 제공한다. 그래프 색인 기술에서 실험하는 이전의 관행은 새로 제안된 기술의 저자가 자신의 것을 구현한 code를 기반으로 기존의 index를 구현하지 않고, 원 저자의 실행 파일을 사용하여 실험하고, 시간판을 보고해왔다. 우리는 이러한 관행이 몇몇 문제들을 낳는다는 거을 알았다. 이 문제를 해결하기 위해서 우리는 모든 대표적인 그래프 색인 기술을 iGraph라 불리는 하나의 공통 프레임 워크에 구현했다.이 데모에서 우리는 iGraph를 보이고, 몇몇 실제 데이터셋과 그들의 workload를 사용하여 그림으로 나타낸다. workload로부터 선택된 질의들에 우리는 철저한 성능 분석을 포함하여 몇몇 고유의 특성들을 보인다.

]

"A Syntactic Type System for Recursive Modules."
Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park.
The Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'11). 2011.

[bibTex | pdf |

ML 모듈 시스템은 강력합니다. 중첩 모듈을 이용하여 이름공간을 효과적으로 구성할 수 있으며 추상 데이터 타입 및 signature sealing을 이용하여 미려하고 오묘한 데이터 추상화, 정보 은닉을 지원합니다. Functors를 이용한 모듈 단위의 강력한 코드 재사용 또한 일품입니다. 그러나 재귀 모듈을 완벽하게 지원하지는 못합니다.

보다 완전한 재귀 모듈 시스템을 설계하고자 했습니다. 재귀 모듈 시스템에 관한 연구로 박사 논문을 쓰신 Keiko 박사님과 OCaml 모듈 시스템 개발자이신 Jacques 교수님께서 함께 하셨습니다.

천군만마였습니다. 재귀 모듈 시스템 설계에 있어서 양대 산맥인 double vision problem과 순환타입문제를 해결하고 논문을 작성했습니다. ICFP 2011에 제출하고자 했습니다. 초록을 등록하고 논문을 계속 수정하고 있었는데, 프로그램 위원장이었던 Olivier Danvy 교수님에게서 메일이 왔습니다. Jacques 교수님이 프로그램위원회 위원이기 때문에 논문을 제출할 수 없다는 것이었습니다. 청천벽력과 같은 소리였고 잠시 좌절했으나 OOPSLA에 논문을 제출하기로 했습니다. 다행히 OOPSLA가 타입이론까지 영역을 확장했기 때문에 논문을 제출할 수 있었고 또 논문이 게재 승인될 수 있었습니다.

]

"A modal logic internalizing normal proofs."
Hyeonseung Im and Sungwoo Park.
Information and Computation 2011. 2011.

[bibTex | pdf |

2005년에 지도교수님이신 Pfenning 교수님과 discussion 중에 찾은 문제로 문제를 풀고 논문으로 출판되기까지 6년이나 걸린 인고의 결과물이다. 양상논리를 이용하여 normal proof가 존재함을 judgment에 표현하는 방법에 대한 연구이다.

]

"Automated Analysis of Industrial Embedded Software."
Moonzoo Kim and Yunho Kim.
Proceedings of Automated Technology for Verification and Analysis (ATVA'11). 2011.

[bibTex | pdf |

이 논문은 ATVA 2011 에 영향력 있는 아시아 연구자로 선정되어 초대받은 논문이다. 처음 초대 메일을 받았을 때 '아 우리 연구가 이렇게 인정받고 있구나' 하는 생각과 함께 '아 우리가 옳바른 길을 걷고 있구나' 하는 생각이 들었다. 더 좋은 연구를 수행해서 더 많은 곳에서 초대받고 인정받는 연구자가 되고 싶다는 생각도 들었다.
논문 내용은 2006년부터 현재까지 진행해 온 사례 연구를 살펴보면서 각 검증 기법들이 어떤 장, 단점을 갖고 있는지 종합하는 것이었다. 특별히 새로운 내용을 더한 것은 아니지만 어떤 과정을 거쳐 우리가 현재 현구 방향을 설정하였는지가 명확하게 보였고, 그 과정이 사례 연구를 통해 탄탄하게 뒷받침 되고 있음을 다시 한 번 확인할 수 있었다. 우리가 발전시켜나가는 방향이 실제 현장에서 필요한 것이고, 우리 연구 결과가 실제 현장에서 유용하게 활용될 수 있음을 본 논문을 작성하면서 확신하게 되었다.

]

"A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study."
Moonzoo Kim, Yunho Kim, and Hotae Kim.
IEEE Transactions on Software Engineering. 37 (2). April 2011. pp. 146-160.

[bibTex | pdf |

이 논문은 ASE 2008 에 제출했던 모델 체킹 사례 연구를 확장한 논문이다. 기존 논문에서 SAT 문제 해결기에 기반한 모델 체킹 기법을 다루었는데 논문 발표 이후 다른 소프트웨어 모델 체킹 기법, 특히 Counterexample-guided abstraction refinement(CEGAR) with predicate abstraction 과 비교해서 어떤 게 더 쓸만하냐를 물어보는 질문을 종종 받았다. 서로 다른 두 소프트웨어 모델 체킹 기법이 어떤 차이점을 보여줄지 우리도 궁금해졌고, 내친 김에 이 둘을 상세하게 비교 분석해보는 연구를 수행하게 되었다.

처음 비교 연구를 시작하기 전에는 내심 CEGAR with predicate abstraction 기법에 대한 기대가 있었다. SAT 기반 모델 체킹 기법이 소스 코드가 커 질수록 SAT 문제 해결에 오랜 시간이 걸려 확장성에 한계를 보였는데 이런 한계를 abstraction 을 통해서 해결해 줄 수 있지 않을까 하는 기대였다. 하지만 막상 비교 연구를 수행하다 보니 CEGAR with predicate abstraction 기법이 C 언어의 포인터 구문을 정확하게 분석하지 못해 부정확한 결과를 내 주는 것을 확인할 수 있었다. 특히 임베디드 소프트웨어의 복잡한 포인터 활용을 생각해볼 때, 도저히 실제 활용 가능한 기법이라는 생각이 들지 않았다. 역시 SAT 기만 모델 체킹을 선택한 우리의 판단이 옳았다는 것을 다시 한 번 확인할 수 있었다.

2008년에 논문을 제출하고 심사평을 받았을 때도 느꼈지만 SE 커뮤니티가 실제 적용 사례 연구에 목말라 있다는 것을 이번 논문의 리뷰를 보면서 다시 한 번 느낄 수 있었다. 다음은 리뷰에서 발췌한 내용이다. SE 연구를 발전시켜 나가기 위해서 현재 기술 수준의 가능성과 한계를 평가하는 사례 연구에 목말라있음을 보여주는 리뷰였다.

"In general, I think this is a good TSE paper. It is a close case study, with important industrial software (components at least), using tools that many readers will be very interested to know more about -- including practical limitations and success."

"I enjoyed reading this paper. There is little "technical content" if by that term one means algorithms or theorems, but there is a severe shortage of papers that provide the service that this one does: detailed case studies that explore the possibilities and limitations of different software model checking technologies. Indeed it is difficult to make progress without these papers and so I definitely recommend acceptance."

]

"QSkycube: Efficient Skycube Computation Using Point-Based Space Partitioning."
Jongwuk Lee and Seung-won Hwang.
Proceedings of the 37th International Conference on Very Large Data Bases (VLDB'11). 2011.

[bibTex | pdf |

Skyline 계산에 dominance 개념이 주로 사용되었는데 incomparability를 활용하면 연산을 보다 최적화 할수 있음을 2009년에 발견하고 투고하였다. 슬프게도 같은 내용의 논문이 SIGMOD 2009년에 실려 소위 “scoop”을 당했다. Skyline은 마치 퍼즐처럼 누구나 듣고 쉽게 이해할 수 있는 문제다보니 도전자가 많아 scoop 당하는 일이 벌써 3번째이다. 하지만, 쌍생아 같아 보이는 두 논문도 언제나 다르고 내 자식만의 강점을 파고들다보면 오히려 더 튼튼한 논문이 되는 것 같다. 결국 scoop당한 자식은 EDBT 2010과 VLDB 2011에 각각 실리게 되었다. 리뷰는 아래와 같으며 이 두 논문에 대해서는 milestone 발표를 통해 이종욱학생이 소개할 것이다.

Overall, I positively evaluate the current work.
1) The problem statement is interesting, and
2) the proposed solution presents substantial improvements over the existing methods.
3) The paper is well-structured and well-written, and
4) the technical details easy to follow.
5) The experimental evaluation is adequate.

]

"COSTRIAGE: A Cost-Aware Triage Algorithm for Bug Reporting Systems."
Jin-woo Park, Mu-Woong Lee, Jinhan Kim, Seung-won Hwang, and Sunghun Kim.
Proceedings of the 25th AAAI Conference on Artificial Intelligence. 2011.

[bibTex | pdf |

이 논문은 새로 생성된 버그레포트들을 "빠르고 정확하게 해결할 수 있는 개발자"에게 알맞게 할당하기 위한 문제를 해결하기 위한 방법을 제시하여, AI 분야의 최고학회 중 하나인 AAAI 2011에 채택되었습니다. 이 논문을 적기 위해서 밤새 연구하던 모습들이 주마등처럼 지나가네요. 지금은 버그레포트 연구와는 다른 연구를 하고 있지만, 이 논문을 적으면서 했던 경험은 저의 연구에 많은 도움이 되고 있습니다. 지도교수님이신 황승원 교수님과 홍콩과기대의 김성훈 교수님의 지도와 공동저자인 무웅이형과 진한이의 도움에 감사드립니다.

]

"SocialSearch: Enhancing Entity Search with Social Network Matching."
Gaewon You, Seung-won Hwang, Zaiqing Nie, and Ji-rong Wen.
Proceedings of the 14th International Conference on Extending Database Technology. 2011.

[bibTex | pdf |

DB연구자로 센터에 기여하고자 하는 방향은, 아주 많은 데이터가 주어진다면 기존의 모델기반의 방법론을 보완할 수 있는 새로운 직관을 제시할 수 있다는 것이다. 이 논문의 novelty는 웹 문서의 정보를 하나의 그래프, 소셜네트워크를 다른 하나의 그래프로 보고 매핑하면 웹 문서에 등장하는 인명과 소셜네트워크 ID를 매핑할 수 있다는 아이디어에 있다. 같은 방법으로 영어 문서의 정보를 하나의 그래프, 중국어 문서의 정보를 또 하나의 그래프로 보고 매핑하면 번역도 가능하다는 논문을 EMNLP 2010에 발표한바 있다. 이러한 데이터기반 방법론에 대해 워크샵에서도 소개할 예정이며, 2 Accepts와 1 Strong Accept로 게재 확정되었다.

"This is a very interesting read, based on solid research, applied on real-world data. Matching graphs of social networks to identify individuals is not especially novel, but this is, as far as I know, the first time this is applied in conjunction with co-occurrence graphs extracted from the Web. Experiments are convincing. For all these reasons, I strongly support the acceptance of this paper."

]

"Design Verification in Model-Based Micro-Controller Development Using an Abstract Component."
Yunja Choi and Christian Bunse.
Software and Systems Modeling. accepted.

[bibTex | pdf |

정형과 비정형의 조화

이 논문은 독일 국제대학의 Bunse 교수와의 다년간의 공동작업의 첫 번째 결실이다. Bunse 교수는 소프트웨어 설계 방법론의 전문가이고 내장형시스템의 모델기반 개발방법론에 특별한 관심을 가지고 있는 사람이기도 하다. 공동작업의 목적은 원대했지만, 과정은 험난했다. 비정형성과 고질적인 습관과 생산 비용과 예외에 대한 고려가 주를 이루는 소프트웨어의 세계와, 논리적 무결성과 명확성이 생명이라고 할 수 있는 정형기법이라는 너무나도 판이해 보이는 두 세계의 실질적 교집합을 찾는 것이다. 이 논문에서는 그 첫 단추로 설계자의 입장에서 이해할 수 있는 정형검증기법의 적용방법론과 기법을 소개하였다.

키워드: 추상컴포넌트, 디자인 검증, 모델기반 개발 방법론

]

"On Supporting Effective Web Extraction."
Wook-Shin Han, Wooseong Kwak, and Hwanjo Yu.
26th IEEE International Conference on Data Engineering (ICDE). 2010.

[bibTex | pdf |

웹에서 정보를 추출하는 연구는 상당한 수준까지 이르렀으며, 많은 상용 시스템이 시장에 나와 있다. 이 시스템들은 추출하고자 하는 정보를 추출하기 위한 정규식과 같은 규칙을 저장하고, 이 규칙을 이용하여 이와 유사한 페이지들로부터 정보를 추출한다. 그런데, 웹페이지가 시간에 따라 변화하면 이 규칙들로는 추출이 더 이상 불가능해지게 된다. 이 문제를 근본적으로 해결할 수 없을까 고민한 끝에 웹페이지가 rendering되면 일종의 2차원 지도가 되고 추출하고자하는 정보는 일종의 공간 객체가 될 수 있다는 생각을 하게 되었다. 따라서, 추출하고자 하는 정보에 대한 위치 관계를 저장함으로써, 웹페이지에 새로운 표가 추가된다든지 열이 추가된다든지 다양한 변화가 발생해도 정보를 추출할 수 있는 기술을 개발하였다.

키워드: Web extraction, Robustness, Rectangle algebra

]

"iGraph: A Framework for Comparisons of Disk Based Graph Indexing Techniques."
Wook-Shin Han, Jinsoo Lee, Minh-Duc Pham, and Jeffrey Xu Yu.
Proceedings of the 36th International Conference on Very Large Data Bases (VLDB'10). 2010.

[bibTex | pdf |

그래프 데이타베이스는 최근에 db community에서 각광받고 있는 토픽중에 하나이다. 이 중 그래프 인덱싱은 주어진 입력 그래프를 포함하는 데이타 그래프를 빨리 찾는데 사용되는데, 경북대학교 데이타베이스 연구실에서는 iGraph라는 새로운 그래프 인덱싱 프레임워크를 제안하였고 이는 분야 Top 컨퍼런스인 VLDB 2010에 발표되었다.

그리고, 한국에서 발표한 논문으로는 최초로 VLDB 2010의 best로 선정되어 VLDB Journal에 초청받았다. iGraph에서는 대표적인 모든 그래프 인덱싱 방법을 하나의 프레임워크에 구현하고, 이 방법들의 성능에 대해서 정성적으로 분석한다. 이러한 프레임워크는 향후 그래프 데이타베이스 분야의 후속 논문들에서 많이 사용될 것으로 기대된다.

]

"Towards an Intelligent Code Search Engine."
Jinhan Kim, Sanghoon Lee, Seung-won Hwang, and Sunghun Kim.
Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI'10). 2010.

[bibTex | pdf |

ROSAEC센터에 참여하면서, 세계 모든 코드를 한곳에 모은다면 어떤 형태의 검색 엔진을 만들어야 개발도중 참조하기 좋은 정보가 될것인가라는 의문을 갖게 되었고, 그 한가지 대답으로, 긍정적인 리뷰를 받았다.

리뷰발췌:
To sum up, the authors present a tool which...integrates a sensible combination of techniques to ultimately give practical user support in a field where even small improvements in work effectiveness has a very significant impact at various levels.

]

"A Calculus for Hardware Description."
Sungwoo Park and Hyeonseung Im.
Journal of Functional Programming. 2010.

[bibTex | pdf |

몇년전 프로그래밍 언어 과목을 강의하면서 얻었던 아이디어를 발전시켜 진행한 연구의 최종 연구 결과물이다. 반도체 칩을 만들때 쓰는 프로그래밍 언어와 (반도체 칩 설계와는 전혀 무관해 보이는) 함수형 언어를 접목시키려는 노력에 대해서 공부를 하는 것도 흥미있었고, 아직까지 증명되지 않았던 근본적인 성질을 증명하는 것도 재미있었다. 반도체 산업에서 함수형 언어가 등장하고 있기 때문에 추후 관련된 연구도 진행할 수 있을 것이다.

]

"Directed Test Suite Augmentation: Techniques and Tradeoffs."
Zhihong Xu, Yunho Kim, Moonzoo Kim, Gregg Rothermel, and Myra B. Cohen.
Foundations of Software Engineering (FSE'10). 2010.

[bibTex | pdf |

작은 이야기: 대가의 면모

저널을 읽거나 학회를 참석하다 보면 자주 보이는 이름들이 있습니다. 아 직학위과정중에있지만놀라운연구실력을보여주는기대주들,막박사 를 받고 독립 연구자로서의 능력을 유감없이 발휘하는 젊은 스타들, 그리 고90년대혹은그이전부터좋은논문들을많이써오신대가들.같은연 구자로서 이런 사람들은 어떻게 연구를 하길레 이렇게 논문을 재밌게 잘 쓸 수 있나 궁금할 때가 많았습니다. 그런 중에 University of Nebraska- Lincoln에 계시는 Gregg Rothermel 교수님과 함께 진행한 공동 연구는 좋은 경험이 되었습니다.

Gregg 교수님과는 작년 가을부터 올 3월까지 regression testing 의 test-suite augmentation 의 성능과 효과에 영향을 미칠 수 있 는 요소들을 분석하는 연구를 연구를 진행하였고 그 결과를 ACM FSE 2010 에 발표하였습니다. 특히, regression testing 과 통 계적 분석, genetic algorithm 을 사용한 테스트 생성에 강점을 두고 있는 Gregg 교수님 연구실과 concolic testing과 formal analysis 에 강점을 두고 있는 우리 연구실 사이의 상승 효과가 돋보 이는 연구였습니다. 특히 같은 내용이라도 문제 정의를 어떻게 하고 어떻게 글을 풀어나가냐에 따라 논문의 내용이 크게 달라질 수 있다는 것을 Gregg 교수님과 같이 논문을 작성해 나가면서 느낄 수 있었습니다. 또한 우리의 강점을 발휘하여 체계적으로 실험설계를 하고 연구결과를 분석하여 헛점을 줄여 나갔습니다. 그 결과 FSE 리뷰어들로부터 "This is a very well done study...", "The paper covers an interesting problem related to test suite augmentation in regression testing..." 와 같이 재밌는 문제를 잘 찾아 분석을 잘 한 연구라고 평가받을 수 있었습니다.

Gregg 교수님은 올 여름부터 약 1년간 연구연가로 KAIST에 머물고 계십니다. FSE에 발표한 논문을 확장해서 더 일반화 시키는 연구와, 서로 다른 성질을 갖는 두 테스트생성기법이 어떻게 서로를 도와나가 상승효과를 극대화시킬 수 있는지 알아보는 연구를 같이 진행하고 있습니다. Gregg 교수님과 연구하는 것은 항상 즐겁습니다. 대가의 통찰력을 느낄 수 있고, 놀라운 논문 작성능력을 배울 수 있고, 또 같이 연구하는 사람들을 잘 이끌어가고 기분좋게 해 주는 모습을 볼 수 있습니다. 지금하고 있는 연구들도 좋은 결실을 맺고, 앞으로 이런 연구자가 되어야겠다고 다짐해봅니다.

]

"Dependency-Aware Reordering for Parallelizing Query Optimization in Multi-Core CPUs."
Wook-Shin Han and Jinsoo Lee.
Proceedings of the 35th SIGMOD International Conference on Management of Data (SIGMOD'09). 2009. pp. 45-58.

[bibTex | pdf |

VLDB 2008 논문의 확장 연구. 이 연구에서는 dependency-aware reordering이라는 새로운 개념을 사용하여 질의 최적화기를 병렬화하는 범용 병렬화 프레임워크를 처음으로 개발하였다. 개발된 프레임워크는 모든 bottom-up기반의 질의 최적화기를 지원하며, 질의 최적화를 위한 워크로드를 동적으로 분배하는 특징을 가지고 있다. 실험 결과, linear speedup을 보였으며, 기존 연구보다도 좋은 성능을 보였다.

리뷰평의 일부를 발췌하면 아래와 같다.

"The authors have looked at an important class of algorithms (bottom up dynamic programming) and have given a full accounting of how they can be parallelized on a modern multi-core computing system. They have looked not only at the theoretical aspects of scheduling these computations, but the actual software methodology and hardware tuning. (Really nice job!)"

키워드: Dependency-aware reordering, Multi-cores, Query optimization, Parallel databases

]

"Ensuring Sound Numerical Simulation of Hybrid Automata."
Yerang Hur, Jae-Hwan Sim, Jesung Kim, and Jin-Young Choi.
Computing Science and Engineering. 3 (2). Jun. 2009. pp. 73-87.

[bibTex | pdf |

올 초 한 훌륭하신 여성분이 내 인생 구제 해주신다고 나서셨습니다. 물론 저야 너무 감사했죠^^. 일사천리로 준비를 했는데. 어라... 결혼준비 기간이 논문 준비기간하고 딱 맞물려 버렸네요... 하여튼, 사력을 다해 둘 다 충실히 준비했는데.. 아뿔사 , 문제의 순간이 다가왔습니다. 내일까지 실험을 끝내야하고, 그러려면 밤새 테스트 프로그램을 준비해야 하는데, 내일은 그 중요하다던 앨범 촬영 날! 혼자 자문자답했습니다.. “논문이 중요해? 아님 장가가 중요해?“. 물론 대답은 ”둘 다“… 어느 한쪽도 포기할 수 없었습니다. 결국 밤 꼬박새고, 허겁지겁 스튜디오로 ... 물론, 포토샵의 위력으로 빨간 토끼눈은 보정되었지만, 예비 신랑이 찍는데 졸고 있다고, 혼나던 기억은 생생히 남아 있습니다.

]

"Adding Examples into Java Documents."
Jinhan Kim, Sanghoon Lee, Seung-won Hwang, and Sunghun Kim.
Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering. 2009.

[bibTex | pdf |

연구라는 이름의 소통

대표논문 [3], [4], [5]는 센터에 참가하게 된 뒤 센터 사사로 쓰게 된 논문들이다. [1], [2]와 다른 점이 있다면, 학문 후속세대인 연구실 학생들과 다른 연구 분야 연구자의 협동으로 이루어졌다는 점이다-- [3]은 마이크로소프트 아시아의 연구원들과 협력하였고 [4]는 포스텍의 계산기하 연구실과 협력하였고 [5]는 HKUST 소프트웨어 공학 연구실과 협력하였다. 후속세대의 초보 운전 연수를 겸하는 아찔하지만 신선한 연구, 다른 분야 연구자와 소통하면서 낯익은 문제 낯설게 보기, 혹은 낯선 문제 낯익게 보기. 이러한 새로운 도전을 통해, 후속세대와, 다른 분야와 연구로 소통하고 한 단계 성장하게 된 느낌이다. 경험하였다. 이러한 소통의 열매인 [3]은 KDD의 유일한 한국 기관 소속 발표 논문이고, [4]는 최우수 논문상을 수상하였고, [5]는 생애최초의 소프트웨어 공학 논문이다.

[1] Seung-won Hwang, Kevin Chen-Chuan Chang: Optimizing top-k queries for middleware access: A unified cost-based approach. ACM Trans. Database Syst. 32(1): 5 (2007)
[2] Seung-won Hwang, Kevin Chen-Chuan Chang: Probe Minimization by Schedule Optimization: Supporting Top-K Queries with Expensive Predicates. IEEE Trans. Knowl. Data Eng. 19(5): 646-662 (2007)
[3] Jongwuk Lee, Seung-won Hwang, Zaiqing Nie, Ji-Rong Wen: Query result clustering for object-level search. KDD 2009: 1205-1214
[4] Wanbin Son, Mu-Woong Lee, Hee-Kap Ahn, Seung-won Hwang: Spatial Skyline Queries: An Efficient Geometric Algorithm. SSTD 2009: 247-264
[5] Adding Examples into Java Documents, Jinhan Kim, Sanghoon Lee, Seung-won Hwang, Sunghun Kim. ASE 2009

]

"Query Result Clustering for Object-Level Search."
Jongwuk Lee, Seung-won Hwang, Zaiqing Nie, and Ji-Rong Wen.
Proceedings of the 15th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. ACM New York, NY, USA. 2009. pp. 1205-1214.

[bibTex | pdf |

연구라는 이름의 소통

]

"A Logical Account of Uncertain Databases Based on Linear Logic."
Sungwoo Park and Seung-won Hwang.
Proceedings of the 12th International Conference on Database Theory (ICDT'09). 2009. pp. 141-148.

[bibTex | pdf |

몇 년 전 Heinz Schweppe라는 독일분이 학과를 방문하셨다. 데이터베이스를 연구하시는 분으로 내 사무실과 가까운 곳에 계셔서 이런 저런 얘기를 나누었는데 “DB and PL are not that apart from each other."라는 인상깊은 말씀을 해 주셨다. 그 뒤 uncertain database에 대해서 설명을 해 주셨는데 linear logic에서와 비슷한 기호를 사용하는 것을 발견했다. 나는 linear logic을 이용하면 uncertain database의 의미를 매우 간결하게 설명할 수 있다고 직감했고 그 뒤 이 아이디어를 논문으로 완성했다. 이 논문의 내용은 깊지 않아서 linear logic의 기초적 지식만 있으면 누구나 이해할 수 있다. 그러나 다른 분야의 사람과 대화를 통해서 새로운 연구 주제를 찾아낸 아주 값진 경험을 나에게 선사한 논문이다.

]

"Model Checking of Real-Time Properties of Resource-Bound Process Algebra."
Junkil Park, Jungjae Lee, Jin-Young Choi, and Insup Lee.
IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences. E92-A (11). Nov. 2009. pp. 2781-2789.

[bibTex | pdf |

프로세스 대수는 동시적 시스템의 대수적 특성을 연구하는 컴퓨터학의 한 분야이다. ACSR은 프로세스 대수의 일종으로 미국 펜실베니아 대학의 이인섭교수님 연구팀이 개발했다. 이 논문은 ACSR에서 모델체킹을 활용할 수 있는 방법을 제안하고있다. 이는 ACSR이 정형명세언어로서 효과적으로 사용할 수 있도록 위함이다.

이 논문이 계기가 되어 저자 중 한명은 펜실베니아 대학의 그 연구팀에 초청받아 3개월간 공동연구를 다녀오기도 했다. 또한 이 논문을 작성하는 동안 물리학의 불확정성의 원리와 유사한 현상을 우선순위를 가지는 프로세스 대수에서 발견하기도 하였다. 이 연구가 실시간 시스템 모델링과 분석에 조금이나마 기여하게 되길 기대한다.

]

"Spatial Skyline Queries: An Efficient Geometric Algorithm."
Wanbin Son, Mu-Woong Lee, Hee-Kap Ahn, and Seung-won Hwang.
Proceedings of the 11th International Symposium on Advances in Spatial and Temporal Databases. Springer. 2009. pp. 264.

[bibTex | pdf |

연구라는 이름의 소통

]

"StreamTX: Extracting Tuples from Streaming XML Data."
Wook-Shin Han, Haifeng Jiang, Howard Ho, and Quanzhong Li.
Proceedings of the Very Large Data Base Endowment. 1 (1). 2008. pp. 289-300.

[bibTex | pdf]

"Parallelizing Query Optimization."
Wook-Shin Han, Wooseong Kwak, Jinsoo Lee, Guy M. Lohman, and Volker Markl.
Proceedings of the Very Large Data Base Endowment. 1 (1). 2008. pp. 188-200.

[bibTex | pdf]

"Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker."
Moonzoo Kim, Yunho Kim, and Hotae Kim.
Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08). Sept. 2008. pp. 198-207.

[bibTex | pdf |

연구를 하면서 항상 실용성에 대한 고민을 한다. 본 논문은 우리 연구가 실용적임을 보인 시금석이 되는 연구였다. 뿐만 아니라, 다른 연구자들도 산업체 사례 연구에 많이 목말라 하고 있었다는 걸 학회에서 느꼈다.

키워드: formal verification, embedded software, flash memory, SAT-based model checking

]

"Functional Netlists."
Sungwoo Park, Jinha Kim, and Hyeonseung Im.
Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08). 2008. pp. 353-366.

[bibTex | pdf |

2006년 포스텍에서 처음으로 학부 프로그래밍언어를 강의하는 동안 학생들로부터 과제가 많다는 불평을 줄곧 받았다. 총 8개의 과제가 지나치게 많은 것은 아니라고 생각했기 때문에 자세한 내막을 알아보았다. 학생들의 불만은 전년도까지 프로그래밍언어 과목은 과제가 거의 없는 (널널한) 과목이었는데 갑자기 과제가 많아져서 함께 수강하는 컴퓨터구조 과목의 과제를 할 시간이 없게 되었다는 것이고, 결국 엉뚱하게 애꿎은 나의 과목으로 화살을 돌리고 있었던 것이다.

당시 컴퓨터구조 과목의 과제는 Verilog 프로그래밍이었는데 나는 Verilog로 변환되는 함수형 하드웨어 기술 언어를 학생들에게 배포하면 컴퓨터구조 과목 과제를 빨리 끝낼 수 있을 것이고 그러면 나의 과목 과제를 더 열심히 하게 될 거라는 장난기 섞인 생각을 했다.

관련 연구를 살펴본 나는 이 주제가 사실 좋은 연구 주제임을 발견했고 이 후 본격적으로 문제를 풀기 시작했다. 결국 lambda-calculus를 Verilog로 변환하는 시스템을 설계해서 구현했고 2008년 ICFP에 발표하였다.

순수하게 학부생의 과제를 돕겠다는 연구 동기 때문에 논문의 깊이와는 무관하게 내가 가장 자랑스러워하는 논문이다.

]

"A Probabilistic Language Based on Sampling Functions."
Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
ACM Transactions on Programming Languages and Systems. 31 (1). 2008. pp. 1-46.

[bibTex | pdf |

2006년 초 POPL 2005 프로그램 위원장으로부터 TOPLAS POPL Special Issue에 논문을 제출해 달라는 부탁을 받았다. 초청 논문이어서 POPL 논문을 약간 확장만 하면 게제 승인될 줄 알았는데 4명의 reviewer들로부터 호된 비판을 받았다. 그 이후 3번의 revision을 거쳐서 최종적으로 46쪽의 긴 논문을 완성하게 되었다. Revision summary로 제출한 문서가 총 64쪽으로 논문보다 길었으며, 논문 수정 중에 좋은 박사 학위 연구 주제를 발견하기도 했다. 그런데 모든 reviewer들로부터 OK를 받았을 때는 이미 POPL Special Issue가 출판된 상태였다. 다시 제출 후 3개월 뒤 게제 승인이 났다.

]

"From NuSMV to SPIN: Experiences With Model Checking Flight Guidance Systems."
Yunja Choi.
Formal Methods in System Design. June 2007. pp. 199-216.

[bibTex | pdf]

"Ranked Subsequence Matching in Time-Series Databases."
Wook-Shin Han, Jinsoo Lee, Yang-Sae Moon, and Haifeng Jiang.
Proceedings of the 33rd International Conference on Very Large Data Bases (VLDB'07). 2007. pp. 423-434.

[bibTex | pdf]

"Progressive Optimization in a Shared-Nothing Parallel Database."
Wook-Shin Han, Jack Ng, Volker Markl, Holger Kache, and Mokhtar Kandil.
Proceedings of the 2007 ACM SIGMOD International Conference on Management of Data (SIGMOD'07). 2007. pp. 809-820.

[bibTex | pdf]

"Probe Minimization by Schedule Optimization: Supporting Top-k Queries with Expensive Predicates."
Seung-won Hwang and Kevin Chen-Chuan Chang.
IEEE Transactions on Knowledge and Data Engineering. 2007. pp. 646-662.

[bibTex | pdf |

셋방에서 1가구2주택까지

대표논문 [1]과 [2]는 박사과정 동안 관심을 가졌던 랭킹을 빨리 계산하는 알고리즘을 인덱스 유무 등의 임의의 다양한 환경을 다루도록 확장하여 정리한 저널 원고이다. 나의 연구 결과는 SIGMOD 2002년에 처음 출판되었는데 랭킹 문제가 정보 검색에서 흔히 사용되는 기법이다 보니 SIGMOD에 보내면 SIGIR로 보내라는 리뷰가 오고 SIGIR로 보내면 SIGMOD로 보내라는 리뷰가 오는 설움을 겪었다. 2002년 이런 연구는 데이터베이스 학회에서 “포푸리”나 “질의 처리” 세션에 세 들어 발표되었다. 2009년 현재에는 연구자가 많이 늘어 데이터베이스와 정보검색 학회에서 모두 Ranking I, Ranking II 등의 멀티세션으로 편성 될 만큼 규모가 커졌는데, 나의 연구 커리어와 시작을 같이 하는 이 토픽의 미래 모습에 궁금증과 애착이 크다.

[1] Seung-won Hwang, Kevin Chen-Chuan Chang: Optimizing top-k queries for middleware access: A unified cost-based approach. ACM Trans. Database Syst. 32(1): 5 (2007)
[2] Seung-won Hwang, Kevin Chen-Chuan Chang: Probe Minimization by Schedule Optimization: Supporting Top-K Queries with Expensive Predicates. IEEE Trans. Knowl. Data Eng. 19(5): 646-662 (2007)
[3] Jongwuk Lee, Seung-won Hwang, Zaiqing Nie, Ji-Rong Wen: Query result clustering for object-level search. KDD 2009: 1205-1214
[4] Wanbin Son, Mu-Woong Lee, Hee-Kap Ahn, Seung-won Hwang: Spatial Skyline Queries: An Efficient Geometric Algorithm. SSTD 2009: 247-264
[5] Adding Examples into Java Documents, Jinhan Kim, Sanghoon Lee, Seung-won Hwang, Sunghun Kim. ASE 2009

]

"Optimizing Top-k Queries for Middleware Access: A Unified Cost-Based Approach."
Seung-won Hwang and Kevin C. Chang.
ACM Transactions on Database Systems. 32 (1). 2007. pp. 5.

[bibTex | pdf |

셋방에서 1가구2주택까지

]

"Type-safe Higher-order Channels in ML-like Languages."
Sungwoo Park.
Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP'07). 2007. pp. 191-202.

[bibTex | pdf |

ML 계열 언어에서 타입시스템을 이용하여 병렬프로그래밍의 안전성을 보장하는 방법에 관한 연구 결과물이다. 확장 논문은 Journal of Functional Programming에 게제되었다.

]

"Deviation Analysis: A New Use of Model Checking."
Mats P.E. Heimdahl, Yunja Choi, and Michael W. Whalen.
Automated Software Engineering. January 2005. pp. 321-347.

[bibTex | pdf]

Individual research project leaders

"Structure Grid for Directional Stippling."
Minjung Son, Yunjin Lee, Henry Kang, and Seungyong Lee.
Journal of Graphical Models. 2010.

[bibTex | pdf |

컴퓨터 그래픽스 분야를 생각할 때 가장 먼저 생각나는 것은 역시 영화에서 자주 사용되는, 현실과 구별이 어려울 정도로 멋진 CG화면들이다. 실제로 컴퓨터 그래픽스 분야에서 많은 사람들이 집중적으로 연구해온 것은 보다 사실적인 영상을 만드는 방법이었다. 하지만 과연 사람들이 만들고 싶은 영상이 꼭 사실적인 영상들 뿐일까? 정말 그렇다면 사진과 인쇄술이 발달한 이 시대에도 예술가라는 직업이 존재하고, 사진 대신 풍경화나 초상화를 그려 걸어둘 이유가 없을 것이다. 이렇듯 사람들은 꼭 사실적인 사진이 아니더라도, 개성 있고 다양한 스타일의 그림들을 좋아한다. 하지만 예술가의 작품들은 만드는데 시간이 오래 걸리고 그 희소성으로 인해 누구나 쉽게 갖기가 어렵다.

다양한 스타일 중 신문이나 잡지에서 초상화를 위해 사용되는 헤드컷(headcut)의 경우, 점과 선만으로 이루어진 단순한 스타일임에도 불구하고도, 이들이 방향성 있게 나열되어 대상의 특징을 잘 표현해주는 인상적인 스타일이다. 그리고 그 특성으로 인해 인쇄술이 발달하여 굳이 사용할 필요가 없게 된 지금에도 계속해서 사용되고 있다. 하지만 이러한 헤드컷을 만들기 위해서는 숙련된 헤드컷 아티스트라 하더라도 3~4일이 소요되고, 따라서 신문이나 잡지에 나올 정도로 유명한 사람이 아닌 이상, 보통 자신의 모습을 이러한 헤드컷 스타일로 만들기는 거의 불가능하다.

우리가 개발한 기술은 이러한 헤드컷 영상을 사진 한 장만으로 누구나 쉽고 빠르게 만들어낼 수 있도록 한다. 이를 위하여 먼저 예술가가 그리는 헤드컷의 특징을 분석하고, 분석 결과에 따라 대상의 중요한 흐름을 정의하는 방법, 흐름에 따라 점이나 선의 위치를 정하는 방법, 그리고 실제 점이나 선으로 톤을 표현하는 방법을 정의하였다. 그리고 여기에 최신 GPU를 이용함으로써, 단 1~2초 이내에 멋진 헤드컷을 만들 수 있도록 하였다. 이 기술을 이용하여 유명한 사람이 아니라도 누구나 자신만의 특별한, 헤드컷 형태의 초상화를 가질 수 있게 되기를 기대한다.

]

"Fast Motion Deblurring."
Sunghyun Cho and Seungyong Lee.
ACM Transactions on Graphics. 28 (5). 2009.

[bibTex | pdf |

누구나 중요한 순간에 사진을 찍을 때 카메라가 흔들려서 사진을 망친 안타까운 경험들이 있을 것이다. 이럴 때 사진을 후 처리하여 선명하게 바꿀 수 있는 소프트웨어가 있다면 얼마나 좋을까? 영상 디블러링 기술은 이런 욕구를 만족시키기 위하여 영상처리 및 계산사진학 (computational photography) 분야에서 오랫동안 개발되어 왔다. 그러나, 지금까지의 기술들은 모두 블러가 제거된 영상의 화질이 만족스럽지 않거나 수행시간이 많이 걸리는 문제가 있었다.

영상화질과 수행시간이 모두 만족스러운 디블러링 소프트웨어를 만들기 위하여 알고리즘 개발과 실험을 반복한 후에 드디어 기존보다 수십 배가 빠른 기술을 개발할 수 있었다. 에지 추측 단계를 디블러링 과정에 추가하고 GPU 구현을 통하여 만족스러운 화질의 영상을 수초 만에 얻을 수 있게 된 것이다. 우리가 개발한 기술이 널리 활용되어 많은 사람들이 소중한 사진들을 보다 선명하게 복원할 수 있기를 기대해 본다.

]

"Robust Color-to-gray via Nonlinear Global Mapping."
Yongjin Kim, Cheolhun Jang, Julien Demouth, and Seungyong Lee.
ACM Transactions on Graphics. 28 (5). 2009.

[bibTex | pdf |

컬러 영상을 흑백 영상으로 변환하는 것에 대해 연구를 한다? 다양한 컬러 디스플레이가 넘쳐나는 이 시대에 컬러 영상을 흑백 영상으로 바꾼다는 것은 마치 세상을 역행하는 것과 같이 들리는 이야기이다. 그러나 서류, 슬라이드, 일간 신문 등 눈앞에 쌓여있는 흑백 출력물들을 보라. 실상 컬러 출력 기기들이 보편화된 지금에도 여전히 흑백출력이 사용되고 있지 않은가.

컬러의 밝기를 이용하는 것은 지금까지의 일반적이고 당연하게 여겨지는 방법이었지만, 컬러의 대비를 보존하지 못한다. 밝기가 똑같은 빨간색 물체와 파란색 물체가 서로 붙어있는 사진이 찍혔다고 하자. 이것을 밝기를 이용해 흑백 영상으로 바꾸게 되면 두 물체가 같은 흑백 값을 갖게 되어 구별되지 않을 것이다. 그렇게 되면, 기대한 품질의 흑백 출력물을 얻을 수 없음은 물론이다.

컬러 영상을 흑백으로 변환하는 것은 픽셀 정보가 3차원에서 1차원으로 줄어들기 때문에, 정보들을 완벽하게 보존하는 것은 불가능 하다. 밝기만을 이용하는 방법을 넘어 효과적인 변환을 위한 다양한 방법이 제시되었으나, 수십 분이 걸리거나, 컬러의 밝기나 일관성을 훼손하는 등 실용화하기 어려운 많은 한계점이 있었다. 우리는 이 문제에 대해서 컬러 영상의 밝기, 일관성, 컬러 대비 등 다양한 정보들을 빠른 시간 안에 효과적으로 보존하는 방법을 만들어 냈다.

그러한 방법을 찾아내기 위해 수많은 실패와 역경이 따랐음은 물론 말할 것도 없다. 그러나 어쩌면 연구의 출발점이었던, “황당하다고 생각될만한 것에도 관심을 갖고, 또한, 당연해 보이는 것에 의문점을 갖는다.” 라는 것이 어쩌면 가장 중요한 교훈일 것이라는 생각이 든다.

]

"A Policy Description Language for Context-based Access Control and Adaptation in Ubiquitous Environment."
Joonseon Ahn, Byeong-Mo Chang, and Kyung-Goo Doh.
Lecture Notes in Computer Science. vol. 4097. 2006. pp. 650-659.

[bibTex | pdf |

2005년도 연말, 연구과제 제안서를 준비하면서 우리도 일반인(?)의 관심을 받는 분야를 해보자라는 생각에 일단 유비쿼터스라는 주제를 정해놓고 무엇을 할 수 있을지 의견을 모으기 시작했다. 교수님들과의 많은 난상토론이 이루어졌고 그래서 나온 제목은 유비쿼터스 컴퓨팅을 위한 프로그래밍 환경이었다.

뭔가 미래지향적이고 새로운 언어가 나올 것만 같았지만, 겨울이 지나고 수많은 메신져 회의를 거쳐 나온 언어는 논리 언어의 형태가 되어 있었다. 사람들이 쉽게 작성하기 위해서는 선언적인 언어여야만 했고, 상황에 따른 서비스를 정의하려다 보니 논리 프로그래밍 언어의 형태를 닮아가게 된 것이다.

과거의 지나간 연구 결과로 생각했던 것들이 다시 유용하게 사용되고 주목받는 경우를 많이 본다. 시맨틱 웹과 논리 프로그래밍이 그렇고, 멀티코어의 등장과 함께 다시 주목을 받고 있는 병렬 프로그래밍과 병렬화 컴파일러가 그렇고, 자료 병렬 함수형 언어 구조가 사용되는 구글 맵리듀스(MapReduce)의 경우가 그렇다. 이번 경우도 비슷한 경우였다. 과거 논리언어 강의 노트와 자료를 다시 찾아보기 시작했다.

개발된 PDL(Policy Description Language)을 기반으로 실행환경이 구축되었고, 유비쿼터스 환경을 위한 프로그램 분석이나, 접근 제어를 위한 언어의 확장도 고안되었고, 실제적인 응용도 개발해 보았다. 이거 한번 해볼까 하고 바닥부터 시작하다 보니 장님 문고리 잡는 토론도 많이 했지만, 그런 만큼 재미있게 이것저것 많이 시도해 볼 수 있었던 연구의 시작이었다.

키워드 : Ubiquitous Computing, Policy Description Language, Context Awareness, Access Control

]

Research associates

"Sharp Thresholds for Hypergraph Regressive Ramsey Numbers."
Lorenzo Carlucci, Gyesik Lee, and Andreas Weiermann.
Journal of Combinatorial Theory, Series A. 2011.

[bibTex | pdf |

이론쪽 저널 논문 출판이 좀 오래걸린다. 원고 제출 후 6개월 내에 결졍이 나면 초스피드이고 보통 1년이내에 되면 빠른 편이다라고 하는데 이 논문은 그러한 과정을 3번 거쳤다. 그러다보니 만 3년이 되어서야 출판 결정이 되었다.

논문의 주 내용은 수리논리의 증명론과 조합론과의 연관성을 밝혀 낸 내 박사논문의 일부 결과를 일반화 시킨 연구다. 박사논문 지도교수와 이태리 출신 친구와 함께 공동으로 진행한 연구인데 결과가 아주 좋다고 판단을 해서 수학쪽 탑10 안에 들어가는 저널에 제출했다가 1년 반만에 흥미롭긴 한데 분야가 논리라서 좀 특수하다라는 평아닌 평으로 거절당했다. 논문을 제출했다가 거절을 당할 수도 있지만 무려 1년 반을 기다리게 하고선 단 몇 줄로 ‘흥미롭긴 한데 좀 특수하다’라는 말로 논문평가를 내리는 건 무슨 심보일까 궁금하기만 하다.

두 번째로 선택한 저널은 랭킹이 한 단계 더 높은 데를 선택했다. 랭킹이 하나 더 높긴 했지만 우리 논문과 관련된 논문이 이미 출판된 역사가 있기에 시도한 것이지 오기에 그런 건 아니었다.

내 입장에선 논문 출판이 하나라도 빨리 되기를 바랬기에 처음엔 반대했지만 다른 두 사람이 강력히 원했기에 ‘그래, 이미 시간은 한참 지나갔다. 그래도 되면 대박아니겠어’ 라며 동의 했다. 근데 1년여의 시간이 흘러 첫 시도와 비슷한 반응으로 거절 당했다. 이젠 좀 신경질이 났다. 도대체 몇 년을 이 논문 하나 때문에 시간을 보내야 하는지. 그래서 작년 초에 논문의 내용에 수정을 가하여 우리 논문에 가장 많은 관심을 보여줄 combinatorics 쪽 저널에 제출을 했다. 탑10은 아니지만 그래도 위에서 30 등 안에 드는 저널이다보니 경험상 이곳도 최소 1년은 기다리는 것으로 알고 있었기에 논문 제출 사실을 아예 잊고 지내기로 했다. 하지만 무슨 일인지 6개월 만에 긍정적인 결정이 났다.

그래도 좋은 저널에 출판이 되는 것으로 마무리 되어서 정말 다행이지 그렇지 않다라면 너무나도 아쉬운 논문이 될뻔 했다. 오는 2월 출판 예정이다.

]

"Kripke Models for Classical Logic."
Danko Ilik, Gyesik Lee, and Hugo Herbelin.
Annals of Pure and Applied Logic. 2010.

[bibTex | pdf |

공저자: Danko Ilik, Hugo Herbelin
키워드: Kripke model, classical logic

미국 태생의 철학자이자 논리학자인 Saul Kripke가 1950년대 후반에서 1960년대 초반 사이에 고안한 Kripke model은 non-classical 논리 시스템에 대한 semantics를 제공한다. 예를 들어 intuitionistic first-order logic과 modal logic에 대해서 sound하며 complete한 semantics를 제공하며 이는 classical first-order logic이 참, 거짓에 기저를 둔 집합론식 semantics를 갖는 것과 대비된다.

Kripke model은 참, 거짓이라는 이분법이 아닌 주어진 명제의 증명가능성을 기본 개념으로 한다. 즉, 어떤 주어진 명제의 참, 거짓 여부가 아니라 그것이 참인지 거짓인지에 대한 증명가능성을 이야기 한다. 예를 들어, 주어진 명제의 참, 거짓 여부가 증명 되었는가 또는 앞으로 증명이 될 것인가에 관심을 둔다.

이와 같이 Kripke model은 intuitionistic logic 또는 modal logic과 깊은 연관을 맺고 있으며 classical logic과는 무관하다고 알려져 왔다. 다만 double-negation을 통해 간접적으로만 정의해서 언급되어졌을 뿐 실질적인 활용성에 있어서는 별다른 연구가 진행되지 않아 왔다. (참고로 double-negation은, 간략하게 설명해서, A라는 명제가 classical logic에서 증명가능하면 ￢￢A는 intuitionistic logic에서 증명가능하다 라는 관계를 보이는 데에 이용된다. 따라서 A가 classical logic에서 forcible 하다는 것을 ￢￢A가 intuitionistic logic에서 forcible 하다라는 것으로 정의하면 classical logic에 대한 sound하며 complete한 Kripke semantics를 얻는다.)

반면에 위 논문은 classical logic에 대한 Kripke semantics를 어떠한 double-negation도 사용하지 않으면서 forcing relation을 정의하는 방식을 소개한다. 이와 같이 classical Kripke semantics를 직접적으로 정의할 경우에만 얻어질 수 있는 중요한 부산물이 있다. 대표적으로 기존의 어떤 증명보다도 쉬운 cut-elimination의 constructive한, 즉 배중율을 사용하지 않는 증명과 그 결과로 얻을 수 있는 classical logic의 무모순성(consistency)의 constructive한 증명이다. 배중율을 사용하지 않는다는 사실은 어떠한 증명으로부터도 cut-rule를 사용하지 않는 증명을 기계적으로 추출할 수 있음을 의미하며 이는 proofs-as-programs을 사용할 경우 주어진 proof term의 normal form을 자동으로 추출하는 프로그램을 작성할 수 있음을 의미한다.

결과적으로 위 논문은 classical logic에 대한 Kripke semantics를 직접적으로 정의하는 방식을 처음으로 제안한 의미 있는 논문이 되었으며 앞으로 새로운 연구방향을 제시하는 역할을 수행할 것이라 기대하고 있다.

지금까지 몇 번 공동연구를 진행했었지만 이 논문처럼 재밌게 한 적이 드물다. 프랑스 인리아에서 포닥을 하면서 알게된 두 친구와 함께 진행한 연구인데 세 명의 저자가 각자의 지식을 적절하게 조합해서 이뤄낸 성과를 논문이 담고 있을 뿐만 아니라, 함께 연구를 진행하면서 서로의 의견을 진지하면서도 비판적으로 주고받을 수 있는 분위기를 끝까지 유지하면서 완성시킨 논문이기도 하다.

논문의 내용은 직관주의 논리 또는 양상논리 modal logic에만 적용된다고 알려진 Kripke semantics를 고전논리에도 적용할 수 있음을 보이는 내용을 관련 분야 내에서 최초로 담고 있다. 논문의 후속타가 가능하다고 보는데 지난 시간동안 다른 일에 집중하느라 진행시킬 수가 없어서 많은 아쉬움을 갖고 있으며 조속한 시기에 새로운 시도를 해서 다시 한 번 즐거운 공동연구를 다시 한 번 경험할 수 있기를 바랄 뿐이다.

]

"Scala for Generic Programmers Comparing Haskell and Scala Support for Generic Programming."
Bruno C. d. S. Oliveira and Jeremy Gibbons.
Journal of Functional Programming. 2010.

[bibTex | pdf |

This paper is about doing datatype-generic programming in Scala and it was published last year at the Journal of Functional Programming.

Together with Jeremy Gibbons (my former PhD advisor), I have showed that Scala (like Haskell) already provides all the essential features required for the development of DGP libraries. Moreover, we have demonstrated that Scala has important advantages over Haskell when it comes to implementing DGP libraries. In particular, Scala supports a form of open datatypes, which can be used to support extensible generic functions in a more natural way.

We believe that this work will provide important foundations for future developments of DGP libraries in OO languages and, hopefully, help the mainstream adoption of DGP techniques.

]

"Type Classes as Objects and Implicits."
Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky.
The Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'10). 2010.

[bibTex | pdf |

This paper was published at last years Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) conference and it describes how the concept of type classes (originally from Haskell) inspires a useful programming technique in Object-Oriented (OO) Languages with generics (such as Java or C#).

Type classes were originally developed in Haskell as a disciplined alternative to ad-hoc polymorphism. Type classes have been shown to provide a type-safe solution to important challenges in software engineering and programming languages such as, for example, retroactive extension of programs. They are also recognized as a good mechanism for concept-based generic programming and, more recently, have evolved into a mechanism for type-level computation.

Together with Adriaan Moors and Martin Odersky, I have shown a lightweight approach to type classes in object-oriented (OO) languages with generics using the Concept pattern and implicits (a type-directed implicit parameter passing mechanism). Furthermore, I have also shown that Scala, a multi paradigm language that blends functional and object-oriented programming and supports implicits, supports many features that make the language ideally suited for expressing various types of generic programming.

I was motivated to write this article because I think the concept of type classes is not well-understood by a lot of people. On the one hand OO programmers are puzzled by type classes declarations in Haskell and they wonder how it relates to OO programming. On the other hand Haskell programmers tend to have a misconception that type-classes are fundamentally different from classes in OO languages and that it is not easy to encode similar behaviour in OO. I think this article clarifies those issues and it also shows how implicits can effectivelly support type class programming in OO languages.

]

"EffectiveAdvice: Disciplined Advice with Explicit Effects."
Bruno C. d. S. Oliveira, Tom Schrijvers, and William R. Cook.
Proceedings of the 9th International Conference on Aspect-Oriented Software Development. 2010.

[bibTex | pdf |

This paper, published at last year proceedings of the Aspect Oriented Software Development (AOSD) Conference, is about a difficult problem in reasoning about programs: how to reason modularly about inheritance in the presence of effects?

In the paper we focus on advice, which is a form of inheritance widely-used in aspect-oriented programming (AOP) languages and which allows one program component to augment or modify the behavior of other components. When advice and other components are composed together they become tightly coupled, sharing both control and data flows. However modular reasoning about a component becomes very difficult; and two tightly coupled components may interfere with each other’s control and data flows.

Together with Tom Schrijvers and William Cook, I proposed EffectiveAdvice: a disciplined model of advice that supports both modular reasoning and reasoning about interference. By modelling advice in a monadic purely functional language, we have shown that traditional reasoning techniques such as equational reasoning and parametricity can be used to prove properties about interference in a modular way.

Here’s what one of the reviewers said about this paper:

The problem tackled in that paper is probably the most important and difficult one AOP has to face. Even if the language considered is not full AOP (e.g. no pointcuts), it remains very expressive and allow modular reasoning. The approach and the use of interference combinators are very interesting and the results look impressive.

]

"Formal Identification of Right-Grained Services for Service-Oriented Modeling."
Yukyong Kim and Kyung-Goo Doh.
Proceedings of the Web Information Systems Engineering (WISE'09). 2009. pp. 261-273.

[bibTex | pdf |

에피소드: 논문리뷰중에

The motivation behind the transformation and its methodology is clearly presented. Moreover, the authors provide a new cost metric as a tool to solve the clustering problem over business activity diagrams. Since the granularity control is one of major concerns in SOA modeling, the significance of the presented work is unquestionable. The contribution is stated clearly. Limitations and further improvements are also fairly indicated. Briefly, the paper is of excellent quality and relevance to the conference.

** STRONG POINTS
The paper presents a completely new approach to the service granularity problem. As the problem concerns the system modeling, it greatly influences SOA application development. Presentation is of very good quality.

]

"Formally Verifiable Features in Embedded Vehicular Security Systems."
Gyesik Lee, Hisashi Oguma, Akira Yoshioka, Rie Shigetomi, Akira Otsuka, and Hideki Imai.
Proceedings of the 1st IEEE Vehicular Networking Conference. 2009.

[bibTex | pdf |

공저자: Hisashi Oguma, Akira Yoshioka, Rie Shigetomi, Akira Otsuka, Hideki Imai
키워드: 자동차 보안 프로토콜, 정형증명

논문은 자동차에 사용되는 electronic system이 점점 복잡해지면서 발생할 수 있는 사안들에 대한 이야기로 시작한다. 현재 자동차 생산비용의 23％ 정도가 전자시스템과 관련되어 있으며 앞으로 자동차 관련 연구의 80％ 수준까지 전자시스템에 대한 연구로 채워질 것으로 기대하고 있다. 이와 상응해서 vehicular networking의 중요성도 상응해서 올라갈 것이며 따라서 networking 보안 프로토콜의 중요성도 커질 것이다 등등.

사실 과학, 기술에 대한 기본 지식만 있으면 누구나 이해할 수 있는 말이다. 하지만 구체적인 문제로 파고들면 상황은 달라진다. 가격 경쟁력이 있으면서 원하는 실행능력을 갖춘 칩을 어떻게 만들 것이며, vehicular networking을 가능케 하는 environment를 어떻게 구현할 것이며, 자동차 내부에서의 칩과 칩 또는 자동차 칩과 신호등 칩 사이의 communication의 구현문제와 통신에 사용되는 보안 프로토콜의 검증 등등 구현 또는 해결해야 할 많은 문제들이 산적해 있다.

위 논문은 일본 AIST 연구소에서 지내면서 진행한 자동차 관련 보안 프로토콜의 정형증명 프로젝트의 결과물이다. 팀장이 보안 프로토콜 관련 정형증명에 관심을 갖게 되면서 진행된 프로젝트는 ProVerif, Scyther 등 논리에 기반으로 한 automatic verification tools에 대한 공부로 시작하여서 자동차 관련 보안 프로토콜의 검증에 응용하는 것을 주 내용으로 담고 있다.

Toyota InfoTechnology Center에서 개발한 보안프로토콜의 검증을 시도하면서 Embedded Vehicular Security Systems과 관련된 보안 프로토콜이 기본적으로 만족해야 하는 성질을 아래와 같이 규정하고 주어진 보안 프로토콜이 그것들을 만족시키는 가를 정형증명을 이용하여 어떻게 증명할 수 있는가에 중점을 두었다.

(1) 오직 유효한 권한을 가진 controller만이 교신할 수 있다.
(2) 검증되지 않은 메시지는 따로 관리되거나 폐기처분 된다.
(3) 모든 교신은 암호화 되어 있어야 하며 검증된 controller만 교신에 참여할 수 있다.
(4) 우연히 성공한 한 번의 공격이 전체 시스템을 해치지 않아야 한다.

논문이 이론적으로 아주 깊은 내용을 담고 있지는 않지만 Vehicular Security Systems 관련해서 처음으로 정형증명에 대한 논리적 접근을 담았다는 점에 의미가 있다.

]

"Modular Visitor Components: A Practical Solution to the Expression Families Problem."
Bruno C. d. S. Oliveira.
Proceedings of the 23rd European Conference on Object Oriented Programming (ECOOP'09). 2009.

[bibTex | pdf |

A major obstacle in the development of software components is the so-called expression problem. One way in which the expression problem is experienced in practice by developers is when a system has been developed with some initial requirements in mind, but suddenly there is the need to extend it in a way that involves modifying all parts of the system. Modular Visitor Components [1] provides an interesting solution to the expression problem and other related problems using inspiration from type-theoretical encodings of datatypes. I am particularly excited about this work, because I believe that is the starting step to the development of a new programming language mechanism that does not suffer from the expression problem.

[1] B. C. d. S. Oliveira. Modular visitor components: A practical solution to the expression families problem. In ECOOP ’09: Proceedings of the 23rd European Conference on Object Oriented Programming, 2009.

]

"Sharp Thresholds for the Phase Transition between Primitive Recursive and Ackermannian Ramsey Numbers."
Menachem Kojman, Gyesik Lee, Eran Omri, and Andreas Weiermann.
Journal of Combinatorial Theory, Series A. 115 (6). 2008. pp. 1036-1055.

[bibTex | pdf]

"The Visitor Pattern as a Reusable, Generic, Type-safe Component."
Bruno C. d. S. Oliveira, Meng Wang, and Jeremy Gibbons.
Proceedings of the 23rd ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'08). 2008.

[bibTex | pdf |

Another goal of the DGP project was the investigation of advanced parametrization techniques as a means of capturing some common object-oriented design patterns [2] as reusable library code. The main problem here is that design patterns, while valuable abstractions available for programmers, cannot be captured by anything other than informal paper descriptions. In this paper (which I wrote together with Wang and Gibbons) [1] I showed how to capture the VISITOR design pattern as a Scala software component by exploiting themathematical structure of encodings of datatypes as higherorder combinators in a type-theoretic setting.

[1] B. C. d. S. Oliveira, M. Wang, and J. Gibbons. The visitor pattern as a reusable, generic, type-safe component. In OOPSLA ’08: Proceedings of the 23rd ACM SIGPLAN conference on Object oriented programming systems languages and applications, 2008.
[2] E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.

]

"A Comparison of Well-known Ordinal Notation Systems for e0."
Gyesik Lee.
Annals of Pure and Applied Logic. 147 (1-2). 2007. pp. 48-70.

[bibTex | pdf]

"'Scrap Your Boilerplate' Reloaded."
Ralf Hinze, Andres Löh, and Bruno C. d. S. Oliveira.
Functional and Logic Programming. 2006.

[bibTex | pdf |

My early research focused on datatype-generic programming (DGP), which is aimed at the reuse of code patterns that show up over and over again for different data structures. During my visit to the University of Bonn in 2005, Hinze, Löh and myself [1] reconstructed an appropriate DGP view and used it to relate the Scrap your Boilerplate (SyB) approach to other DGP approaches, since the original work was extremely hard to understand from an implementers perspective due to some advanced features and tricks used in the implementation. In essence the goal of our work was to explain in lay man’s terms how the SyB approach worked. In fact our initial version of the paper was entitled “Scrap your Boilerplate Explained”.

[1] R. Hinze, A. Löh, and B. C. d. S. Oliveira. ‘Scrap your Boilerplate’ reloaded. In Functional and Logic Programming, 2006.

]

"Multiclass Sparse Logistic Regression for Classification of Multiple Cancer Types Using Gene Expression Data."
Yongdai Kim, Sunghoon Kwon, and Seuck Heun Song.
Computational Statistics and Data Analysis. 51 (3). 2006. pp. 1643-1655.

[bibTex | pdf |

소중한 경험

2005년 봄, 박사과정을 수료하지도 못한 채 덜컥 결혼을 하고 나서 취직을 심각하게 고민하고 있을 즈음이었다. 연구나 공부에 흥미를 잃어가던 나에게 어느 날 갑자기 긴 영어 제목이 달린 Tex 파일 하나와 함께 들려온 말은 아직도 기억이 생생하다. “이거 읽어보고 이해해라. 마지막 Section에 자료 분석 part를 네가 좀 해봐라. 이 정도는 할 수 있지? ” 막 새로 부임하신 김용대 교수님과의 첫 만남이었다. 조금 한심한 고백이지만, 당시 행해온 수많은 행적(?) 때문에 주어진 논문을 이해하는 것조차가 나에겐 엄청난 고난이었다. 더군다나 프로그램을 만들라니!

그때부터 경험한 나 스스로에 대한 황당함들, 하다못해 메일에 첨부된 aaaa.tex 파일을 열 수가 없어서 교수님께 직접 여쭤보러 들리기 까지 했다. 더욱 난감한 것은 논문에 실린 내용이었다. 전혀 이해 할 수가 없었다. 많이 알려진 모형을 수정한 모형이라고 적혀있지만 도움이 되지 않았다. 교수님 말씀처럼 이 정도는 할 수 있어야 하는 것 아닌가? 결국 온갖 방법을 다 동원해서 몇 편의 참고 논문을 읽어보고, 제안된 모형을 적합할 만 한 프로그램의 사용법을 공부한 후에야 겨우 늦은 시작을 할 수 있었다. 완전히 새로 시작한 셈이라고 볼 수 도 있겠다.

위 논문은 내가 저자로 등록된 첫 논문이다. 하지만 처음이라서 라기 보다는, 강렬한 경험을 남긴 논문으로 나에게 기억되고 있는 논문이다. 당시 제안된 모형을 적합하는 알고리즘을 완성하였지만 수렴속도가 너무 느리다는 문제가 발생했다. 김용대 교수님이 개발한 glasso 알고리즘을 직접 제안된 모형에 적용하기에는 약간의 문제가 있었던 것이다. 수렴속도에 대한 상황을 이해하신 김용대 교수님은 곧바로 당시 boosting을 전공하던 박사님 한분과 함께 몇 시간을 토론하면서 알고리즘을 수정하기 시작했다. 옆에서 조용히 듣고 있을 수밖에 없었지만, 거창한 수학이나 혹은 수치적 이론이 아닌, 직관에 대한 믿음과 현상에 대한 이해만으로도 알고리즘은 서서히 빨라지기 시작했다. 얼마 지나지 않아서, 당시 토론의 결과들은 다시 잘 정리된 몇 개의 수식으로 요약되어 새로운 논문의 밑거름이 되었다.

당시 고급 확률론을 공부하면서 무슨 말인지 이해도 되지 않던 어려운 정리들을 글자만 따라가며 증명하는 일에 익숙하던 나에게, 증명이전에 현상에 대한 직관적인 이해가 무엇보다 우선이라고 하는 커다란 진리를 깨닫게 해준 계기가 되었다.

사실 논문의 내용을 적는 것이 본 글의 취지에 더 맞을지도 모른다. 하지만 현재 어떤 주제의 공부를 새로 시작한다고 해도 난 이 논문을 통해 배운 아주 간단한 경험에 충실히 따르려고 노력한다. 이러한 점에서 이 이야기가 위 논문에 더 어울리고, 이 이야기 속에서 위 논문이 내게 고마운 논문이 된다.

]

"Extensible and Modular Generics for the Masses."
Bruno C. d. S. Oliveira, Ralf Hinze, and Andres Löh.
Proceedings of the Trends in Functional Programming. 2006.

[bibTex | pdf |

Today there is a wealth of robust DGP libraries available for use in Haskell platforms. However, this was not always like this due to severe limitations in terms of extensibility and modularity in early approaches. Together with Hinze and Löh [1], I made important advances in the area and presented an extensible and modular variation of the Generics for the Masses [2] technique (that we call EMGM) in Haskell. This approach, which is now widely used within the Haskell community, has been consider one of the most complete DGP libraries in a recent comparison among existing DGP libraries [3].

[1] B. C. d. S. Oliveira, R. Hinze, and A. Löh. Generics as a library. In Trends in Functional Programming, 2006.
[2] R. Hinze. Generics for the masses. In International Conference on Functional Programming, pages 236–243. ACM Press, 2004.
[3] A. Rodriguez, J. Jeuring, P. Jansson, A. Gerdes, O. Kiselyov, and B. C. d. S. Oliveira. Comparing libraries for generic programming in haskell. In Haskell Symposium, 2008.

]

Technical Memos

ROSAEC-2015-001	"Static Analysis with Set-closure in Secrecy." Woosuk Lee, Hyunsook Hong, Kwangkeun Yi, and Jung Hee Cheon. March 2015.
	[bibTex \| pdf]
ROSAEC-2014-003	"Towards Scalable Translation Validation of Static Analyzers." Jeehoon Kang, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi. November 2014.
	[bibTex \| pdf]
ROSAEC-2014-002	"An Extensible Verified Validator For Simple Optimizations in LLVM." Sungkeun Cho, Joonwon Choi, Jeehoon Kang, Chung-Kil Hur, and Kwangkeun Yi. September 2014.
	[bibTex \| pdf]
ROSAEC-2014-001	"Encrypted Execution." Daejun Park, Jeehoon Kang, Kihong Heo, Sungkeun Cho, Yongho Yoon, and Kwangkeun Yi. February 2014.
	[bibTex \| pdf]
ROSAEC-2013-014	"Global Sparse Analysis Framework." Hakjoo Oh, Kihong Heo, Daejun Park, Jeehoon Kang, and Kwangkeun Yi. March 2013.
	[bibTex \| pdf]
ROSAEC-2011-013	"Hoare logic for multistaged programs." Kwangkeun Yi and Cristian Gherghina. September 2011.
	[bibTex \| pdf]
ROSAEC-2011-012	"CPS Transformation of Lisp-Like Multi-Staged Languages." Ludovic Patey and Kwangkeun Yi. September 2011.
	[bibTex \| pdf]
ROSAEC-2011-011	"Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness." Jieung Kim and Sukyoung Ryu. May 2011.
	[bibTex \| pdf]
ROSAEC-2011-010	"GMeta: A Generic Formal Metatheory Framework for First-Order Representations." Bruno C. d. S. Oliveira, Gyesik Lee, Sungkeun Cho, and Kwangkeun Yi. April 2011.
	[bibTex \| pdf]
ROSAEC-2010-009	"Semantics Preservation Proof of an Unstaging Translation of Lisp-Like Multi-Staged Languages." Wontae Choi, Baris Aktemur and Kwangkeun Yi. September 2010.
	[bibTex \| pdf]
ROSAEC-2010-008	"Clone Detection by Comparing Abstract Memory States." Heejung Kim, Yungbum Jung, Sunghun Kim, and Kwangkeun Yi. March 2010.
	[bibTex \| pdf]
ROSAEC-2010-007	"Inferring Quantified Invariants via Algorithmic Learning, Decision Procedures, and Predicate Abstraction." Cristina David, Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwangkeun Yi. January 2010.
	[bibTex \| pdf]
ROSAEC-2009-006	"Improving Code Review by Predicting Reviewers and Acceptance of Patches." Gaeul Jeong, Sunghun Kim, Thomas Zimmermann, and Kwangkeun Yi. September 2009.
	[bibTex \| pdf]
ROSAEC-2009-005	"A Control Flow Analysis for 2-staged Programming Languages." Taeksu Kim, Chunwoo Lee, Kiljoo Lee, Soohyun Baik, and Kwangkeun Yi. September 2009.
	[bibTex \| pdf]
ROSAEC-2009-004	"Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction." Yungbum Jung, Soonho Kong, Bow-Yaw Wang, and Kwnagkeun Yi. August 2009.
	[bibTex \| pdf]
ROSAEC-2009-003	"Identifying Static Analysis Techniques for Finding Non-fix Hunks in Fix Revisions." Yungbum Jung, Hakjoo Oh, and Kwangkeun Yi. August 2009.
	[bibTex \| pdf]
ROSAEC-2009-002	"Large Spurious Cycles in Global Static Analyses and Their Algorithmic Mitigation." Hakjoo Oh and Kwangkeun Yi. August 2009.
	[bibTex \| pdf]
ROSAEC-2009-001	"Abstract Parsing for Two-staged Languages with Concatenation." Soonho Kong, Wontae Choi, and Kwangkeun Yi. June 2009.
	[bibTex \| pdf]