프로그래밍 관련 연구실 석사 진학 예정 학생입니다..
- 글쓴이
- 꿈꾸는남자
- 등록일
- 2011-12-22 19:38
- 조회
- 5,620회
- 추천
- 0건
- 댓글
- 7건
관련링크
논문은 주로 정형기법을 바탕으로 한 설계를 하는 걸 석사 때 해볼려고 하는데
읽을만한 책이나 대가인 교수님이 있나요 ? Requirement engineering 의 한 부분인지..
아님 제가 나무만 보고 숲은 못 보는건지 모르겠습니다.
에이스님들의 조언을 부탁드립니다.
다른 사람들 의견
-
지각생
()
같은 분야라서 반갑네요. 제가 검색해 본 바로는 국내에서는 이광근교수님(<a href=http://ropas.snu.ac.kr/~kwang/)과 target=_blank>http://ropas.snu.ac.kr/~kwang/)과</a> 최진영 교수님(<a href=http://formal.korea.ac.kr/wiki/)이 target=_blank>http://formal.korea.ac.kr/wiki/)이</a> 눈에 띄는 듯 합니다. (개인적으로 뵌 적은 없습니다.) 정형기법을 하기도 하는 교수님들은 더 많이 계신데, 예를들어 프로그래밍 언어를 하시는 분들이 logic과 formalization을 병형하는 경우입니다.
formal methods를 좁게 해석하면 주로 하드웨어나 항공기등의 임베디드 소프트웨어 검증의 경우인데요. 전자의 경우 verilog/HDL로 제작된 디자인의 검증을 들 수 있구요. 후자는 lustre에 기반한 model checking을 예로 들 수 있겠네요. 하지만, 결국 전통적인 propositional logic이나 first order logic으로 환원한 뒤에 SAT/SMT solver를 적용하는 경우가 많기 때문에, 결국 러셀의 논리학과도 연관이 됩니다. 항공기 분야에서는 Rockwell Collins의 Steven Miller가 유명하신 것 같고요. 세부전공이 좀 달라서 자세히는 모르겠네요. (VMCAI, CAV, IJCAR conference 참조)
프로그래밍 언어 이론 쪽으로 넘어가면, 요즘 유럽에서는 type theory를 기반으로 하여, 수학 명제 증명을 많이 하는 것 같습니다. The Types mailing list 참조(<a href=http://lists.seas.upenn.edu/mailman/listinfo/types-list). target=_blank>http://lists.seas.upenn.edu/mailman/listinfo/types-list).</a> PLPV workshop 참조.
그리고, SAT/SMT/TPTP solver등 아주 일반적인 로직을 위한 automated theorem proving 분야도 있습니다. 이런 분야는 다양한 응용 분야에서 사용할 수 있는 고성능의 범용 도구를 개발하거나 사용방법을 연구하죠. (SAT conference, SMT workshop 참조)
기존 프로그래밍 언어 (Java, C) 기반의 formal verification도 있는데요. Microsoft Research에서 많은 진전이 있었습니다. (<a href=http://research.microsoft.com/en-us/projects/vcc/ target=_blank>http://research.microsoft.com/en-us/projects/vcc/</a> 등) 조만간에 여러 프로젝트들을 통합해서 상용화 할 예정이라고 들었는데. 시장에서 올킬이 예상됩니다. UIUC의 Rosu 교수가 C semantics에 기반한 검증 시스템을 만들었더군요. 그런게 아니면, abstract interpretation을 사용하여 특정한 속성을 효율적(+자동적)으로 증명하는 기법도 많이 사용되구요.
비슷한 연구를 하는 사람들도 많고, 다양한 적용분야가 있어서 나열하기는 힘들지만. 모두 logic이라는 고리로 연결되어있다고 할 수 있지요. 기업체에서 적용하기에는 logic과 theorem prover의 사용 방법을 익히는 것으로 충분하겠구요. 연구를 하려 한다면, 고전 logic의 metatheory(괴델)가 도움이 되는 것 같습니다.
-
지각생
()
그리고, requirement engineering이라고 보는 것도 합당합니다만, software engineering의 프로세스 관리에서 말하는 그 것과는 다르지요. 사실 requirement를 formal하게 논리적으로 기술하는 것이 상당히 어렵니다. (어떤 경우는 불가능에 가까움) 그리고 결과물이 그 requirement를 만족시킬 수 있는지를 증명하거나, 혹은 증명 가능성이 있는 requirement인지 예상하는 것은 더욱 어렵구요.
아무리 개발자들이 쉬운 증명 툴을 가진다고 해도, logic을 제대로 공부한 사람이 아니라면 질문 자체를 제대로 하기가 어렵습니다. 그래서 logic을 공부한 사람들이 시스템 개발자들을 그 부분에서 관여할 수 밖에 없습니다.
-
지각생
()
음냐 FM conference(<a href=http://fm2012.cnam.fr/), target=_blank>http://fm2012.cnam.fr/),</a> NASA Formal Methods conference도 있네요. 가본적은 없지만...
-
지각생
()
아, 그리고 작년에 제가 Summer School on Formal Techniques에 갔었는데, 홈페이지(<a href=http://fm.csl.sri.com/SSFT11/)에 target=_blank>http://fm.csl.sri.com/SSFT11/)에</a> 강의자료가 그대로 있습니다. 2012년에도 하는데 가실 수 있으면 좋겠네요. 박사과정이면 교수님께 보내달라고 하면 좋은데, 석사는 어렵겠죠.
-
꿈꾸는남자
()
감사합니다 ㅠㅠ ~..이렇게 친절하게 답변을 해주시니 ..
각골난망합니다. 따꺼 ~~ ABSENT STUDENT 님 ..
담에 좋은 정보 교환하고 싶네요 ~쪽지로 제 이멜 보내드릴게요 ..정보교환하며 담에 한번 만나요 ~ -
지각생
()
한 가지 아쉬운 점은, 박사 유학을 생각하신다면 바로 박사로 유학을 지원하시는 것이 좋습니다. 한국은 석사를 거쳐 박사를 많이들 하시던데, 미국을 포함하여 여러 나라에서는 석사는 졸업추 취직을 위한 것이고, 연구를 위해서는 바로 박사로 진학합니다. 그리고 석사를 국내에서 한다고 해도 졸업을 꼭 하실 필요는 없을 것 같습니다. 박사과정 중에 석사학위를 받을 수도 있으니까요.
그리고 formal 분야의 일자리가 그리 많지 않습니다. 얼마전에 저도 왜 취직하기 어려운 분야를 했냐는 이야기를 들었지요. 졸업 후에 어떤 자리를 희망하시는 지는 모르겠지만, "알고리즘을 공부하고 구글(등)에 가겠다"면 저도 기분좋게 좋은 생각이라고 말할 수 있지만, 이 분야는 그러기 어려운 것 같습니다. 물론 앞으로 이 분야도 더 커져야 한다고는 생각하지만, 현실은 그렇지 않으니까요. -
꿈꾸는남자
()
네 감사합니다. ^^;; 이멜로 제 상황을 써드릴게요 ^^
