“무결점 프로그래밍 환경 가능한 정적분석 기술 개발 매진”
연구논문 다수 발표로 주목…스패로우에 성과물 적용 방침
파수닷컴(대표 조규곤)에 지난해 11월 합류한
입사 전 정 연구원은 서울대학 박사과정에서 프로그램 분석 기술을 전공했다. 이 기술은 말 그대로 코딩한 프로그램을 분석해 오류를 찾아 내는 기술로 수학적인 기법이 많이 사용된다.
[파수닷컴 정영범 연구원]
국내선 아직 생소한 분야인 이 기술은, 진입 장벽이 매우 높은 것으로 알려져 있다. 그러나 이 기술이 적용된 제품이 시장에 출시된다면 성장 가능성은 매우 높다고 한다.
정 연구원은 학교에 있으면서 분석기 관련 연구를 했고, 학회서 해당분야 연구자들과 긴밀히 교류했다. 이런 일들은 적성에 맞아 학교생활은 즐거웠다. 그러나 언제부턴가 한켠엔 아쉬움이 쌓여갔다.
“연구를 진행할수록 내가 만든 성과물을 현장의 프로그래머들이 실제로 사용했으면 좋겠다라는 생각이 들었습니다.”
열심히 연구해 나온 결과물을 현장에서 적용하지 못할 때 느끼는 괴리감. 이런 감정은 자꾸 쌓여 어느 순간 그에게 스트레스로 다가왔다. 이로 인해 기업에 입사해 지금까지 연구한 결과를 실제 개발 과정에다 적용하고 싶은 욕구는 하루하루 커졌다.
그런던중 그의 고민을 복잡하게 만들 일들이 연거푸 생겼다. 영국 옥스퍼드 대학에서 박사 후 연구원으로 일할 기회가 그에게 찾아온 것. 대기업으로부터 입사해달라는 제안도 받았다.
“유학 길에 오를 것인가? 기업에 입사해 현장에서 새 꿈을 펼칠 것인가?” 2011년은 그의 인생에서 가장 큰 고민과 결단의 시기였다. 아침에 눈을 뜰 때부터 학교에서 돌아와 잠들 때까지 진로를 줄기차게 고민했다. 그런 끝에 기업행을 결정했다.
“장학금을 받고 유학길에 오를 수 있었지만 포기했습니다. 대기업이 주는 이점이 있었지만, 이 또한 나의 길은 아니었죠. 이 길을 선택하면 지금까지 공부한 정적 분석 분야의 연구를 계속할 수 없었으니까요.”
국립대서 귀중한 국민 세금으로 오랬동안 공부했는데, 전공 분야와 상관없는 일에 종사한다면 이 또한 도리에 맞지 않는 일이라고 판단했다. 그래서 그는 전문성을 가장 잘 살릴 수 있는 정적분석 툴 전문기업인 파수닷컴 입사를 최종 선택했다.
"파수닷컴에 입사해서 내가 진정 좋아하는 분야의 연구와 솔루션 개발을 할 수 있게 됐죠. 그리고 미래를 내다보며 연구자로서 인생의 계획을 바로 세울 수 있게 됐습니다."
파수닷컴에 입사한지 불과 몇 달 밖에 지나지 않았지만, 그의 연구활동은 관련 학계나 업계의 조명을 받고 있다.
그는 최근 “Automatically Inferring Loop Invariants via Algorithmic Learning”이란 제목의 논문을 공개했다.
공저(共著)인 이 논문엔 정 연구원을 포함해, 카네기 멜론 대학(Carnegie Melon University)의
이 논문은 VMCAI10과 APLAS10 학회에서 발표됐고 해당 저널의 초청을 받아 출판까지 하게 됐다. 캠브리지 저널 중 하나인 “Mathematical Structures in Computer Science(http://journals.cambridge.org/action/displayJournal?jid=MSC)”에 논문이 실릴 예정이다.
논문의 주요 내용은, 프로그램 검증의 난제인 루프의 변하지 않는 성질(loop invariant)을 알고리즘적인 학습 (Algorithmic Learning)이라는 새로운 방법으로 유추하는 기술이다.
“모든 프로그래머는 암시적으로 프로그램이 만족해야 하는 성질을 고려하면서 프로그램을 작성합니다. 그리고, 그런 성질들이 실제 만족되는지 확인하고 싶어하죠.”
“C 프로그램에선 assert() 구문을 이용해서 실행 중에 그러한 성질들이 만족되는지 확인할 수 있습니다. 만약 그런 assert() 구문이 루프 이후에 있다면 자동으로 검증되기 위해선 루프의 불변성을 알아내야 합니다.”
프로그램 검증을 연구하는 사람들은, 프로그래머가 가정한 이런 성질들이 항상 만족하는지 실행 전에 자동으로 검증하고 싶어한다.
이런 욕구 충족을 위해 이 논문은 기존에 없던 새로운 프로그램 검증 방법을 제시했다. 논문은 리뷰어에게 후속 연구가 기대된다는 좋은 평가를 받기도 했다.
“일차 논리(firtst-order logic)으로 표현할 수 있는 루프의 불변성을 찾는 후속 연구를 진행했습니다. 이어 루프의 불변성을 표현하는 오토믹 프레딕케이트(atomic predicate)를 프로그램으로 자동 생성하는 연구물을 내놨습니다.” 이 또한 학계의 호평을 받았다.
정 연구원은 또 지난해 프로그래밍 언어와 소프트웨어 공학 분야에서 세계 최고 수준으로 인정 받고 있는 TACAS라는 학회에서 해당 연구논문을 발표했다. 이후 이 논문은 “Logical Method in Computer Science”라는 저널에서도 초청받을 정도로 관심을 모았다.
정 연구원은 입사한 파수닷컴에서 앞으로 프로그램 검증 연구를 계속 할 계획이다. 지금까지 논문에서 제시하고 있는 프로그램 검증 방법은 아직까지는 상용화하기엔 다소 이른 단계라고 한다.
정 연구원은 최신 연구 동향을 주시하고 연구에 더욱 박차를 가해, 상용화가 가능한 단계까지 기술력을 끌어올릴 생각이다. 포부도 당차다.
“만약 프로그램 자동 검증이 상용화 가능하면 프로그램이 프로그래머의 의도대로 작성됐는지 자동으로 그리고 완벽하게 확인할 수 있어, 프로그램의 오류가 없는 프로그래밍 환경의 구축이 가능합니다.”
정 연구원이 연구한 프로그램 검증 기술은, 향후 이 회사의 정적 의미 분석기인 스패로우(Sparrow)에 적용될 예정이다. 이를 통해 파수닷컴이 세계서 인정받는 소프트웨어 기업이 되는데 일조하고 싶다고 그는 말했다.
우리나라의 정적분석 기술은 먼저 기술을 선보인 북미에 비해 다소 뒤떨어져 있다. 파수닷컴에서 새로 터전을 잡은 정 연구원의 꿈이 속히 이루어져, 그러한 결과로 한국의 정적 분석 기술이 세계 최고라는 평가를 받는 날이 오길 기대해본다.
<데일리그리드>