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

"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 ]

"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. Proceedings of the 16th International Symposium on Static Analysis (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. Software: Practice and Experience. accepted.

[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

"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개국에서 항공우주 분야의 논문을 발표하는 학회입니다. 본 논문은 다수 무인기가 임무를 효율적으로 수행할 수 있도록 유전자 알고리듬을 이용하여 임무를 할당하도록 하는 내용을 다룬 논문으로, 발표 당시 관련 연구를 수행하고 있는 일본 연구자들로부터 다양한 질문을 받으며 주목을 받았습니다. ]

"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

"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). accepted.

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

"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 | 연구라는 이름의 소통 대표논문 [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 ]

"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 | 연구라는 이름의 소통 대표논문 [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 ]

"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주택까지 대표논문 [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 ]

"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

"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

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

[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를 직접적으로 정의하는 방식을 처음으로 제안한 의미 있는 논문이 되었으며 앞으로 새로운 연구방향을 제시하는 역할을 수행할 것이라 기대하고 있다. ]

"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