- Probabilistic Programming
- Software Verification
- Static Program Analysis for Software Bug Detection
프로그램 분석(static program analysis)기술은 주어진 프로그램이 실행중에 어떤 성질을 가지는 지를 실행하기 전에 미리 엄밀하게 확인하는 기술이다. 이 기술을 이용해서 무결점 소프트웨어를 싼 비용으로 개발할 수 있게하는 것을 연구한다. 최근에 이 기술은 전통적인 소프트웨어 테스팅의 단점을 해결하면서 선진 산업체로 흘러드는 속도가 거세지고 있다.
그동안 제한적이었던 (항공, 우주, 국방, 교통, 통신, 에너지, 의료등에 사용되왔던) 프로그램 검증기술(formal property verification/checking)이 일반 모든 소프트웨어 개발에서도 필요하게 되었고, 때맞추어 학교 연구실에서 연구된 기술이 이제 실용적으로 쓰일만큼 무르익었기 때문이다.
예를 들어, 우리 연구를 기반으로 상용화 과정을 거쳐 전세계 시장에 내 놓은 Sparrow
같은 것이 한 예가 되겠다.
무결점 소프트웨어를 싼 비용으로 개발할 수 있게하는 기술은, ``mobile
computing'' 혹은 ``ubiquitous computing'' 세상을
안전하게 운영해 주는 소프트웨어
기술의 숨은 기둥이 된다. - 산업화, 실제세계로: Sparrow.
- 정점의 논문: 100만라인 C프로그램을 통째로 자세하고 안전하게
분석하는 이론과 실제
(PLDI'12)
- 비슷한 일을 하는 C코드들을 찾아내는 분석기, sw공학에 응용
(ICSE'11)
- Static Program Analysis for Staged Computation
다단계 프로그래밍:-) (staged programs)은 프로그램이 프로그램을 만들고 실행하는 것을 말한다. 메타 프로그래밍(meta programming)이라고도 불린다. 프로그램 코드가 일반 데이타와 같이 프로그램 실행중에 만들어지고 조합되고 실행된다.
다단계 프로그래밍은 요즘 동적인 웹 프로그램 제작에 긴요하게 쓰인다. 그러나 다단계 프로그래밍은 여러가지 것들을 포섭하는 일반 개념이다. Lisp/Scheme의 준인용(quasi-quatation), 부분계산(partial evaluation), 실행중에 실행코드 만들기(runtime code generation), 매크로(macro) 등. 또, ``진화하는 코드(evolutionary code)'' ``알아서 잘하는 코드(autonomous code)'' 등을 가능하게 하는 원천 기술이 다단계 프로그래밍 기술이다.
하지만 이러한 프로그래밍 언어로 프로그램을 짠 다는 것은 매우 혼돈 스러운 일이다. 어떻게 해야 오류없는 다단계 프로그램을 쉽게 짤 수 있도록 도울 수 있을까? 프로그램 분석 기술이 도울 수 있다. 우리는 이러한 언어로 짜여진 프로그램을 분석해서 오류를 찾아주는 방법에 대한 연구를 진행중이다.
- 첫 결과로서, 지금까지의 문제를 모두 해결한, 안전하고 편리한 타입 시스템을 고안( POPL'06 논문)
- 두번째 결과로서, 타입 이상의 성질들을 분석하는 일반적인 정적분석 방법을
고안(
POPL'11
논문)
- Higher-Order & Typed (HOT) Programming Language System
연구실에서 연구되는 모든 프로그램 분석기술과 제반 도구들을 실제 프로그래밍 언어 시스템으로 구현한다. 이때 구축하는 프로그래밍 시스템은 ML 이라는 프로그래밍 언어의 새로운 컴파일러 시스템및 제반 프로그래밍 도구들이 된다. 이미 nML 이라는 우리 고유의 ML 프로그래밍 시스템을 개발해 놓은 상태인데, 이 nML을 이용해서(혹은 nML 안에) 우리의 다양한 연구성과들이 구체적으로 실현되고 있다.
- Your dream programming system
꿈꾸는 프로그래밍 시스템, 그 꿈을 실현하는 것이 된다.
- quantum programming system: language, type system, static checker, compiler, etc.
- bio programming system: bio simulation programming language system, bio synthesis modeling language system, bio property verifier system, etc.
- whatever you imagine.