프로그래밍 연구실에서는 소프트웨어를 잘 만들게 해 주는 기술을 연구한다. “소프트웨어”는 일반 프로그래밍언어로 작성하는 프로그램뿐 아니라 모든 레벨의 언어로 짜여지는 프로그램을 모두 포함한다. 반면에 “잘 만들게 해 주는 기술”은 프로그래밍 도구들(검증기 property verifier/static analyzer, 변환기 transformer, 번역기 compiler, 실행기 interpreter, 분장술 interface)에 대한 기술들로 집중한다.
Programming Language Theory and Applications
프로그래밍언어의 이론은 연구실에서 진행하는 모든 프로그램분석기술과 도구들의 원천기술이다. 특히 타입시스템과 프로그램 논리에 대한 이론 연구와 함께 이 이론들을 소프트웨어 오류 검증과 소프트웨어 생산성 향상에 접목하는 실용화기술을 연구한다.
Static Program Analysis for Software Bug Detection
프로그램 분석(static program analysis)기술은 주어진 프로그램이 실행 중에 어떤 성질을 가지는 지를 실행하기 전에 미리 엄밀하게 확인하는 기술이다. 이 기술을 이용해서 무결점 소프트웨어를 싼 비용으로 개발할 수 있게 하는 것을 연구한다. 최근에 이 기술은 전통적인 소프트웨어 테스팅의 단점을 해결하면서 선진 산업체로 흘러드는 속도가 거세지고 있다.
Static Program Analysis for Staged Computation
다단계 프로그래밍(staged programs)은 프로그램 코드가 일반 데이타와 같이 프로그램 실행중에 만들어지고 조합되고 실행된다. 다단계 프로그래밍은 요즘 동적인 웹 프로그램 제작에 긴요하게 쓰이지만 이러한 프로그래밍 언어로 프로그램을 짠다는 것은 매우 혼돈스러운 일이다. 우리는 이러한 언어로 짜여진 프로그램을 분석해서 오류를 찾아주는 방법을 연구한다.
