1. 서론

주□제□논□문

요약 해석 및 응용

(Abstract Interpretation and its Applications)

창 병 모

숙명여자대학교 정보과학부

chang@cs.sookmyung.ac.kr

요  약

본 논문에서는 시맨틱스를 기반으로한 대표적인 프로그램 분석 틀로써 최근에 활발한 연구가 진행되고 있는 요약 해석의 기본 개념에 대해서 소개하고 명령형 혹은 객체-지향 언어에서 많이 사용되고 있는 동작 시맨틱스를 기초로 하는 요약 해석에 대해서 설명한다. 또한 최근까지 소개된 요약 해석을 이용한 다양한 응용 분야에 대해서 설명한다.

본 연구는 한국과학재단 목적기초연구(2000-1-30300-009-2) 지원에 의해 수행되었음

프로그램 분석의 목표는 프로그램을 실행하지 않고 프로그램의 실행-시간 동작에 대한 정보를 가능한 한 많이 얻는 것이다. 또한 프로그램 분석 과정은 반드시 유한 시간에 종료되어야 한다.

프로그램 분석을 위한 여러 기법 중에 대표적인 프로그램 분석 틀로써 최근에 활발한 연구가 진행되고 있는 분야가 요약 해석(abstract interpretation)으로 Cousot는 여러가지 프로그램 분석 기법들간의 근본적인 유사성을 인식하고, 통합된 하나의 틀로서  시맨틱스를 기반으로한 요약 해석이라는 수학적 모델을 제시하였다 [5,6].

이 분석 기법은 프로그램을 실제 값 대신에 여러 값들을 의미하는 요약 값(abstract value)를 사용하여 실행함으로써 프로그램의 동작에 대한 정보를 계산하는 것이다 [5,6,7]. 또한 분석 결과는 표준 시맨틱스에 포함되어야 한다는 안전성의 조건을 만족해야 한다.

Cousot가 제시한 요약 해석은 더 구체적인 응용 분야에 적용될 수 있도록 여러 분석 기법으로 구체화되었는데 최근에는 특히, 모델 검사를 통한 프로그램 검증 [10], 프로그램 테스팅 및 디버깅 [2,12],  병렬성 분석 [3], 컴파일러 최적화[16] 등에서의 유용성으로 인해 주목받고 있다.

본 논문에서는 요약 해석의 기본 개념에 대해서 설명하고 명령형 혹은 객체-지향 언어에서 많이 사용되고 있는 동작 시맨틱스를 기초로 한 요약 해석에 대해서 설명하고 요약 해석을 이용한 다양한 응용 분야에 대해서 설명한다.

본 논문의 구성은 다음과 같다. 먼저 2장에서는 요약 해석에 관한 기본 개념을 설명한다. 3장에서는 요약 해석을 기반으로 한 분석방법에  대해 기술한다. 4장에서는 요약 해석의 응용에 관하여 살펴본다. 끝으로 5장에서 결론을 맺는다.

2. 요약 해석의 기초

요약 해석의 기본 아이디어는 실제 무한할 수도 있는 실제 도메인(concrete domain) 대신 더 단순하고, 일반적으로 유한한 요약 도메인 상에서 프로그램을 수행시킴으로써, 프로그램의 실제 수행 시 동작에 대한 정적 정보를 알아내는 것이다.

이 계산 과정은 프로그램의 모든 가능한 실제 실행의 결과가 요약 해석 결과에 포함된다는 의미에서 안전성(safeness)을 보장하면서 근사(approximate) 정보를 제공한다.

요약 해석은 다음과 같은 3가지 중요한 성질을 갖는다 :

(1) 프로그램의 동작에 대한 안전한 근사 값을 제공한다.

(2) 프로그램에 대한 사용자의 주석없이 자동 실행될 수 있다.

(2) 선택된 언어의 모든 프로그램에 대해서 적용 가능하다.

요약 해석에서는 해당 프로그래밍 언어에 대해서 분석하고자 하는 성질만을 고려한 모음 시맨틱스(collecting semantics) 즉 실제 시맨틱스(concrete semantics)를 정의한다. 이 실제 시맨틱스는 프로그램 분석의 기준이 되며 래티스와 같은 순서 구조에 대해서 고정점(fixpoint) 계산으로 설계된다.

이 실제 시맨틱스는 관심이 되고 있는 성질에 대해서 가장 작고(minimal) 즉 정확하고, 안전하며(sound), 상대적으로 완전한(complete) 시맨틱스로 분석의 기준이 된다. 직관적으로 설명하면 이 모음 시맨틱스는 관심이 되고 있는 성질만을 기술하는데 가장 정확한 시맨틱스라고 할 수 있다.

프로그램 분석 즉 요약 해석을 위해서는 앞서 설명한 실제 시맨틱스를 기반으로 수행시 동작에 대한 안전한 근사 정보를 주는 요약 시맨틱스(abstract semantics)를 정의하고 이를 계산하게 된다.

요약 해석은  보통  요약 도메인에 대한 고정점(fixed point) 계산으로 이루어진다. 따라서, 요약 도메인은 유한한 래티스이거나, 그렇지 않은 경우에는 무한 상승 체인(infinite ascending chain)을 허용하지 않는 래티스인 것이 보통이다.

전체적인 요약 해석의 방법은 다음과 같이 요약될 수 있다.

(1) 알아내고자 하는 특성을 올바로 나타낼 수 있도록 구체적 시맨틱스를 정한다.

(2) 시맨틱 객체와 연산들의 요약(approximated description)을 통해 요약 시맨틱스를 정의한다.

요약 해석 설계 시 주요 고려 사항은  실제 값들과 요약 값들간의 대응 관계를 정하는 것이다. 이 대응관계는 Galois 연결(connection)로 기술되는데 이 연결은 실제 값에 대응하는 최선의 근사치인 요약 값이 존재한다는 것을 표현하고 있다.

실제 도메인(concrete domain)를 나타내는  래티스(lattice) [eqn: ( D, sqsubseteq )], 요약 도메인을 나타내는 래티스(lattice)[eqn: ( D^\#, sqsubseteq^\# )]가 있다고 가정하자. 요약 과정을 나타내는 요약 함수(abstraction function) [eqn: alpha : D~ rightarrow D^\#]의 목적은 실제 도메인 [eqn: D]내의 실제 값을 요약 도메인 [eqn: D^\#]내의 근사값에 순서를 존중하면서 대응시키는 것이다. [eqn: d^\#]가 [eqn: d]의 유효한 근사치라는 사실은[eqn: alpha(d) sqsubseteq^\# d^\#]로 표시될 수 있다.

그리고 요약된 값의 의미를 나타내는 실체화 함수(concretization function)[eqn: gamma : D^\#~ rightarrow D]는 [eqn: D^\#]내의 요약 값을 [eqn: D] 내의 값에 순서를 존중하면서 대응시킨다.[eqn: d^\#]가 [eqn: d]에 대한 유효한 근사치라는 사실은 [eqn: d sqsubseteq gamma(d^\#)]처럼 표시될 수 있다.

이러한 두 조건이 동등할 때 [eqn: <alpha, gamma>]는 두 래티스를 오가면서  순서를 잃지 않는 Galois 연결이 된다. 직관적으로 Galois 연결은 최선의 요약(best approximateion) 정보가 [eqn: alpha]에 의해서 정의된다는 것을 의미한다.

정형화해보면 [eqn: D]와 [eqn: D^\#] 사이의  Galois 연결은 다음 조건을 만족하는 두 함수[eqn: alpha : D~ rightarrow D^\#]와 [eqn: gamma : D^\#~ rightarrow D]의 쌍 [eqn: <alpha, gamma>]이다

[eqn: FORALL d in D : FORALL d^\# in D^\# : alpha(d) sqsubseteq^\# d^\#~<->~d sqsubseteq gamma(d^\#)]

예 1

정수 집합 [eqn: "Integer"]의 멱집합 [eqn: wp ( "Integer" )]를 부호를 중심으로 요약하는 요약 도메인 Sign를 살펴보자. 요약 도메인 Sign은 래티스로 구성되며 각 원소들 간의 관계는 그림1.과 같다.

그림 1. Sign 요약 도메인

이 요약 도메인을 위한 요약 함수는 예를 들어 다음과 같이 대응시킨다.

[eqn: alpha( \{ 2,3,7 \})= +]

[eqn: alpha( \{ 2,3,7,-5 \})= != 0]

[eqn: alpha( \{ 2,3,7,0,-5 \})= TOP]

또한 실체화 함수는 요약 값을 다음과 같이 대응시킨다.

[eqn: gamma( DSUM ) = \{ i | i >= 0 \}]

[eqn: gamma( - ) = \{ i | i < 0 \}]

[eqn: gamma( TOP ) = "Integer"]

[eqn: gamma( BOT ) = \{ \}]

[eqn: (D,sqsubseteq)]와[eqn: (D, sqsubseteq^\#)] 사이의 Galois 연결 [eqn: <alpha,gamma>]를 가정해 보자. 프로그램에 대한 실제 시맨틱스 즉 실제 해석(concrete interpretation)에서는 실제 도메인[eqn: D] 상의 단조 연산자(monotone operator)[eqn: T : D~ rightarrow D]를 이용할 수 있고, 요약 시맨틱스 즉 요약 해석에서는 요약 도메인 [eqn: D^\#] 상의 단조 연산자[eqn: T^\# : D^\#~ rightarrow D^\#]를 이용할 수 있다.

다음 조건을 만족하면[eqn: T^\#]는[eqn: T]에 대한 안전한 요약 연산이다 :

(1) 모든 [eqn: d^\# in D^\#]에 대해 [eqn: T (gamma(d)) sqsubseteq gamma(T^\# (d))] (또는 모든 [eqn: d in D] 에 대해 [eqn: alpha(T(d)) sqsubseteq^\#~T^\# (alpha(d)))]이다).

위 조건은 [eqn: T]가 [eqn: T^\#]를 충실히 수용함을 보장하기 위한 안전성(safeness)의 기준으로 고정점 계산을 통한 근사값 계산에서의 안전성을 뒷받침하기 위한 이론적 근거를 마련한다.

예 2.

Sign 도메인의 경우 요약 연산은 쉽게 정의할 수 있다. 예를 들어 실제 연산 +에 대한 요약 연산 [eqn: +^\#]의 일부만 나열하면  다음과 같다.

+ [eqn: +^\#] + = +

[eqn: DSUM][eqn: +^\#] - =[eqn: TOP]

- [eqn: +^\#] - = -

0 [eqn: +^\#][eqn: DSUM] = [eqn: DSUM]

프로그램 [eqn: P]의 실제 시맨틱스는 일반벅으로[eqn: P]에 대해 정의된 단조 함수[eqn: F_P : D ~rightarrow D]의 최소고정점 [eqn: lfp( F_P )]로 정의되며 일반적으로

[eqn: alpha(lfp(F_P )) sqsubseteq^\# ~lfp(alpha circ F_P circ gamma)]

이다. 이 결과를 고정점 요약 정리(fixpoint abstract theorem)라고 한다. 그러나 [eqn: lfp(alpha circ F_P circ gamma)]는 실제 도메인이 유한하지 않으면 유한시간 내에 계산할 수 없다.

따라서 요약 해석에서는 이 값의 근사치를 다음 안전성 조건을 만족하는 단조 연산자 [eqn: F_P^\#]를 정의하여  계산한다 :

[eqn: FORALL d^\# in D^\# : alpha(F_P (gamma(d^\#))) sqsubseteq^\# ~F_P^\#(d^\#)]

혹은

[eqn: FORALL d^\# in D^\# : F_P (gamma(d^\#)) sqsubseteq^\# ~gamma(F_P^\#(d^\#))]

프로그램 [eqn: P]의 요약 시맨틱스는 [eqn: lfp(F_P^\#)] 에 의해서 정의되며 [eqn: alpha(lfp(F_P )) sqsubseteq^\# ~lfp(F_P^\#)]

관계를 만족한다.

3. 동작 시맨틱스를 기초로 한 요약 해석

명령형 언어 혹은 객체-지향 언어의 시맨틱스는 보통 동작 시맨틱스(operational semantics)로 정의하는데 이 시맨틱스는 프로그램 [eqn: P]에 대해서 전이 시스템(transition system)[eqn: (S,rightarrow,I,F)]를 대응시키며 각각은 다음과 같다.

(1) [eqn: S]는 프로그램 상태들의 집합이다.

(2) [eqn: rightarrow_P subseteq S times S]는 전이 관계(transition relation)로 제어의 흐름을 묘사한다.

(3) [eqn: I]는  시작 상태들,[eqn: F]는 종료 상태들의 집합을 나타낸다.

저장(store) [eqn: sigma]는 변수에 대한 값 배정을 나타낸다. 가능한 저장들의 집합을 다음과 같이 정의한다.

[eqn: Store = Variable ~rightarrow ~Value]

배정 표시[eqn: sigma[x mapsto v]]는 [eqn: x]를 [eqn: v]에 대응시키고 다름 모든 변수 [eqn: x']은 [eqn: sigma(x')]에 대응시키는 저장을 나타낸다. 프로그램의 상태(state)[eqn: s]는 [eqn: <p, sigma>]로 정의되며 저장 [eqn: sigma]에서 실행될 프로그램 포인트(program point) [eqn: p in PP]를 나타낸다. 여기서 [eqn: PP]는 프로그램 포인트들의 집합이다.

프로그램의 실제 동작 시맨틱스는 프로그램실행의 한 스텝을 나타내는  전이 규칙(transition rules)에 의해서 정의된다. 유도 (derivation)는 전이들의 연속[eqn: s_0~ rightarrow_P ~s_1 rightarrow_P ~s_2 ~cdots] 이다. [eqn: s]로부터 [eqn: s']으로 유도가 있다는 것은 [eqn: s~rightarrow_P^* ~s']로 나타낸다.

이 시맨틱스를 이용하여 프로그램과 입력 데이터에 대해서 실행 과정을 실제 계산 트리(concrete computation tree) 형태로 설명할 수 있다. 이 트리의 경로는 □실행 궤적□를 형성하며 트리의 각 노드는 계산 과정의 변화를 나타낸다. 만약 계산 과정이 발산하게 되면 무한 트리가 생성되게 된다.

실제 모음 시맨틱스 (concrete collecting semantics)는 시작 상태로부터 도달 가능한 모든 상태들의 집합으로 정의된다.

이 상태들의 집합은 다음 변환 함수 [eqn: F_P in wp(S) rightarrow wp(S)]의 최소고정점 [eqn: lfp (F_P )]으로 정의될 수 있으며 [eqn: F_P]의 정의는 다음과 같다:

[eqn: F_P (X) = I union post[rightarrow_P ] X] where

[eqn: post[rightarrow_P ] X = \{ s | EXIST s' in X : s' rightarrow_P s \}].

요약 해석에서는 위에서 정의된 실제 모음 시맨틱스에 대한 근사값인 요약 시맨틱스를 구해야 한다. 요약 시맨틱스는 앞에서 정의한 [eqn: F_P]에 대한 안전한 함수 [eqn: F_P^\#]를 정의하고 이의 최소고정점 [eqn: lfp (F_P^\# )]로 정의할 수 있다. [eqn: F_P^\#]는 요약의 종류에 따라 여러 형태로 정의할 수 있으며 예를 들면 다음과 같은 형태로 정의할 수 있다.

[eqn: F_P^\# (X) = I^\# union post[rightarrow_P^\# ] X.]

이 정의를 위해서는 일단 요약 상태 도메인 [eqn: S^\#] 및 시작 상태 [eqn: I^\#] 선택 혹은 설계해야 되고 실제 연산자 및 전이 규칙를 안전하게 요약하는 요약 연산자 및 요약 전이 규칙을 정해야 한다. 직관적으로 살펴보면 실제 전이 규칙 내의 실제 연산자를 요약 연산자로 대치하여 요약 전이 규칙을 만들 수 있다.

실제 요약 해석에서는 요약 시맨틱스를 구하는데 있어서는 위에서 정의된 단순한 상태들의 집합보다는 각 프로그램 포인트에 대해서 가능한 상태들을 모두 모아서 관리하는 경우가 보다 일반적이다. 이를 정리하면 [eqn: AbsStore]를 [eqn: Store]에 대한 요약 도메인이라고 하면  요약 도메인[eqn: State^\#]는 다음과 같이 정의된다.

[eqn: State^\# = PP ~rightarrow ~AbsStore]

또한 함수 [eqn: F_P]는

[eqn: F_P^\#: State^\#~ rightarrow~State^\#]

형태로 요약되어야 한다.

다음 프로그램에 대해서 Sign 요약 도메인을 이용해서 각 프로그램 포인트에 대해서 상태 정보를 모으는 요약 해석은 그림 2.의 등식 시스템처럼 정의될 수 있으며 그 최소고정점 해를 구하는 반복 과정은 그림 2.와 같다.

1:

x := 0;

2:

while i<n do begin

3:

x := x +1

4:

end

5:

등식 시스템   1  2  3  4

[eqn: s_1 = TOP ~~~~~~~ BOT~TOP~TOP~TOP]

[eqn: s_2 = 0 ~~~~~~~~ BOT~~0~~0~~0]

[eqn: s_3 = s_2 BIGSQCUP s_4 ~~~ BOT~~0~DSUM~DSUM]

[eqn: s_4 = s_3 +^\# 1 ~~~~ BOT~+~DSUM ~DSUM]

[eqn: s_5 = s_2 BIGSQCUP s_4 ~~~ BOT~DSUM~DSUM ~DSUM]

그림 2. 프로그램과 요약 해석 과정

요약 해석과 관련된 중요한 이슈 중의 하나가 분석 과정의 유한성이다. 정적 분석에서는 유한한 분석만이 의미가 있으므로 반드시 유한 시간 내에 분석이 끝나야 한다. 이를 위해서 요약을 통해서 유한한 요약 도메인을  설계하든지 아니면 [5,6]에서 정의한 확장 연산자(widening operator)를 통해서 분석 과정 중에 빨리 고정점에 수렴하게 함으로써 분석 과정이 유한 시간에 끝나도록 해야 한다.

4. 응용

정적 분석(static analysis)

정적 분석은 요약 해석의 동기가 되었으며 전통적으로 가장 많이 적용된 분야이다. 명령형 언어, 논리 언어, 함수 언어, 최근에는 이동 코드 등과 같은 등의 다양한 언어들에 적용되어 왔다[1,7,13,14,17]. 또한 최근에는 타입 검사[8], 병렬화[3] 및 컴파일러 최적화[16], 질의 최적화[4], 통신 프로토콜 분석 [18]에도 적용되었다.

자동 생성기(automatic generator)

최근에는 파서 생성기처럼 요약 해석기에 대한 명세를 제공하면 자동적으로 요약 해석기를 구현하는 도구에 관한 연구가 활발히 진행되어 왔다. Prolog를 위한 이러한 도구로는 [16]을 들 수 있으며 [21]에서는 중간 언어를 기반으로 한  자동 생성 시스템 Z를 구현하엿다. 또한 Cousot는 실험적인 자동 생성 시스템을 구현하였다 [9].

모델 검사(model checking)

모델 검사는 하드웨어 명세를 검증하는데 많이 사용되어 왔으며 기본적으로 유한 오토마타 상에서 이루어져 왔다. 최근에는 프로그램을 검증하는데 이 기술을 사용하고자 하는 연구들이 많이 진행되고 있다. 그러나 기본적으로 프로그램 검증을 위해서는 프로그램의 실행 모델이 필요한데 프로그램 경우에는 이 실행 모델이 무한할 수 있다.

요약 해석을 이용하면 이 무한할 수 있는 실행 모델을 정확도를 희생하고 유한 모델로 요약할 수 있으며 이 유한 모델이 사용자가 제공하는 명세를 만족하는지 검사할 수 있으며 검사 결과의 안정성을 보장할 수 있다 [11,12,20].

요약 테스팅 및 디버깅 (abstract testing and debuggin)

요약 해석을 이용한 모델 검사의 아이디어를 일반화한 것으로 사용자가 제공한 명세를 요약 해석에 의해서 검증하는 기법으로 이 기법은 프로그램 디버깅을  값 대신에 프로그램 성질(혹은 그에 대한 명세)을 사용하도록 확장한 기법이라고 할 수 있다 [2,12]. 프랑스의 Bourdodoncle은 이 아이디어를 이용하여 Pascal 언어를 위한 디버거 시스템 Syntox를 개발하였다[2]. 또한 이 기법은 비행 소프트웨어 검증 및 Ariane 5 로켓의 핵심 소프트웨어 검증에 사용되었다 [19].

상업화(commercialization)

최근에는 그 동안 요약 해석 분야를 발전을  상업화한 두 회사가 설립되었다. AbsInt 사는 요약 해석을 이용하여 실시간 시스템의 최악 시간 분석을 하고 있으며 Polyspace 사는 소프트웨어 검증을 주로 하고 있다. 두 회사의 웹 주소는 다음과 같다.

- AbsInt GmbH (독일)

http://www.absint.de

- Polyspace Technologies (프랑스)

http://www.polyspace.com

5. 결론 및 향후 연구 방향

본 논문에서는 요약 해석의 기본 아이디어와 이 분야에서 이루어진 지금까지의 연구 결과를 개괄적으로 소개하였다.

요약 해석이 보다 효과적이고 실용적으로 사용되기 위해서는 앞으로 다음과 같은 문제 혹은 과제에 대한 연구가 필요할 것이다.

- 고차-함수, 병렬, 분산, 이동 프로그램의 복잡한 제어 구조의 분석

- 부동 소수점 수, 자료 구조의 동적 할당과같은 복잡한 데이터 구조의 분석

- 분석기의  모듈화 및 복합적인 설계

- 확률적 성질 등과 같은 복잡한 성질 분석.

- 다양한 응용 분야의 개발

참고문헌

[1] F. Bourdoncle, "Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity", Proceedings of PLILP, Lecture Notes in Computer Science 456, pp. 307-323, Springer-Verlag, 1990.

[2] F. Bourdoncle, "Abstract debugging of higher-order imperative languages," in Proceedings of ACM Symposium on PLDI, pp. 46-55, 1993.

[3] F. Bueno, M. Garcia de la Banda, M. Hermenegildo. "Effectiveness of Abstract Interpretation in Automatic Parallelization: A Case Study in Logic Programming". ACM Transactions on Programming Languages and Systems, Vol. 21, Num. 2, pages 189-238, ACM Press, March 1999.

[4] B.-M. Chang, R. Giacobazzi, and K.-M. Choe, "Abstract Filters:Improving Bottom-up Execution of Logic Programs," Proceedins of '94 ACM Symposium on Applied Computing, March 1994.

[5] P. Cousot and R. Cousot, "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints," in Proceedings of 4th ACM Symposium on POPL, pp. 238-252, ACM Press, 1977

[6] P. Cousot and R. Cousot, "Systematic design of program analysis frameworks," in Proceedings of 6th ACM Symposiumm on POPL, pp. 269-282, ACM Press, 1979.

[7] P. Cousot and R. Cousot, "Abstract interpretation and application to logic programs", Journal of Logic Programming, vol. 13, no. 2-3, pp. 103-179, 1992.

[8] P. Cousot and R. Cousot, "Types as abstract interpretations," in Proceedings of 24th ACM Symposium on POPL, pp. 316-331, ACM Press, 1997.

[9] P. Cousot, "The Calculational Design of a Generic Abstract Interpreter," Course notes for the NATO International Summer School 1998 on Calculational System Design. Marktoberdorf, Germany, 28 July ~ 9 August 1998,

[10] P. Cousot and R. Cousot, "Refining model checking by abstract interpretations," Automatic Software Engineering, vol. 6, pp. 69-95, 1999.

[11] P. Cousot and R. Cousot, "Temporal abstract interpretations," in Proceedings of 27th ACM Symposium on POPL, pp. 12-25, ACM Press, 2000.

[12] P. Cousot and R. Cousot, "Abstract interpretation based program testing", Proceedings of SSGRR Conference on Computers and e-business, July 2000

[13] S. Debray, "Formal bases for dataflow analysis of logic programs", Advances in Logic Programming Theory (G. Levi, ed.), pp. 115-182, Clarendon Press, 1994.

[14] M. Dwyer and L. Clark, "Data Flow Analysis for Verifying Properties of Concurrent Programs," Proceedings of 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 62-75, 1994.

[15] J. Feret, "Confidentiality analysis for mobile systems," in Proceedings 7th Static Analysis Symposium, Springer-Verlag, 2000.

[16] M. Hermenegildo, R. Warren, S. K. Debray. "Global Flow Analysis as a Practical Compilation Tool," Journal of Logic Programming, Vol. 13, No. 4, pp. 349-367, Elsevier, August 1992.

[17] A. Venet, "Abstract interpretation of pi-calculus," in Analysis and Verification of Multiple-Agent Languages, LOMAPS Workshop (M. Dam, ed.), June 1996, LNCS 1192, pp. 51-75, Springer-Verlang, 1996.

[18] A. Venet, "Automatic determination of communication topologies in mobile systems," in Proceedings of 5th Static Analysis Symposium, Sep. 1998, LNCS 1503, pp. 152-167, Springer-Verlag, 1998.

[19] P. Lacan, J. Monfort, L. V. Q. Ribal, A. Deutsch, and G. Gonthier, "The software reliability verfication process: The ARIANE 5 example," in Proceedings DASIA98-DAtaSystems IN Aerospace, ESA Publicatios, May 1998.

[20] D. Schmidt, "Data-flow analysis is model checking of abstract interpretations," in Proceedings of 25th ACM POPL, ACM Press, 1998.

[21] K. Yi and L. Harrison, Automatic Generation and Management of Interprocedural Program Analyses, in Proceedings of 20th ACM Symposium on Principles of Programming Languages, pp. 246-259, Jan. 1993

창 병모

1984년~1988년 서울대학교 컴퓨터공학(학사).

1988년~1990년 한국과학기술원 전산학(석사).

1990년~1994년 한국과학기술원 전산학(박사).

1994년~1995년 전자통신연구원 연구원.

1996년 Univ. of Pisa 방문 교수

2000년 Univ. of Verona 방문 교수.

1995년~1999년 숙명여대 전산학과 조교수

1999년~현재 숙명여대 정보과학부 부교수

관심분야: 프로그램 분석, 자바 및 객체-지향 프로그래밍 언어, Formal Method