DBPIA-NURIMEDIA
|
|
- 인권 도
- 7 years ago
- Views:
Transcription
1 424 정보과학회논문지 : 컴퓨팅의실제및레터제 19 권제 8 호 (2013.8) 사례연구를통한정적프로그램분석기법을사용하는도구의비교 (A Comparative Case Study on Static Program Analysis Tools) 김윤호 박용배 (Yunho Kim) 김문주 (Moonzoo Kim) (Yongbae Park) 요약프로그램신뢰성향상을위해서정적프로그램분석도구가많이사용되고있다. 하지만, 정적분석결과에서거짓경보를걸러내기위한추가적인분석이필요하고실제오류를찾지못할수있는문제점이있다. 본논문에서는상용정적프로그램분석도구인 Coverity 와 Sparrow 및오픈소스도구인 Clang analyzer 를 buffer overflow 벤치마크와 libexif 소스코드에적용하여실험대상도구가오류를찾아내는데얼마나효과적인지사례연구를수행하였다. 실험결과 buffer overflow 벤치마크에서는 Coverity, Sparrow, Clang analyzer 각각 6.02%, 3.61%, 0% 의버그탐지율과 2.41%, 1.20%, 0% 의오탐율을보였다. libexif 적용에서 Coverity, Sparrow, Clang analyzer 는총 745 개의오류를찾아내었으나알려진 7 개의오류중 6 개를 본연구는미래부가지원한 2013년정보통신 방송 (ICT) 연구개발사업, 지식경제부 / 한국산업기술평가관리원 IT R&D 프로그램 [ , 초소형 고신뢰 OS와고성능멀티코어 OS를동시실행하는듀얼운영체제원천기술개발 ], 그리고미래부 / 한국연구재단의중견연구자지원사업-핵심연구 ( ) 의연구비지원으로수행되었음 이논문은제39회추계학술발표회에서 정적프로그램분석기법을사용하는도구의비교 :Coverity 와 Sparrow 를사용한 libexif 사례연구 의제목으로발표된논문을확장한것임 학생회원 : KAIST 전산학과 kimyunho@kaist.ac.kr yongbae2@gmail.com 종신회원 : KAIST 전산학과교수 moonzoo@cs.kaist.ac.kr (Corresponding author임 ) 논문접수 : 2013년 1월 21일심사완료 : 2013년 5월 10일 CopyrightC2013 한국정보과학회 ː개인목적이나교육목적인경우, 이저작물의전체또는일부에대한복사본혹은디지털사본의제작을허가합니다. 이때, 사본은상업적수단으로사용할수없으며첫페이지에본문구와출처를반드시명시해야합니다. 이외의목적으로복제, 배포, 출판, 전송등모든유형의사용행위를하는경우에대하여는사전에허가를얻고비용을지불해야합니다. 정보과학회논문지 : 컴퓨팅의실제및레터제19권제8호 (2013.8) 찾아내지못하였다. 이와같이정적분석도구가놓칠수있는오류가많으므로높은소프트웨어신뢰성보장을위해다른기법과병행하여적용하는것이필요하다. 키워드 : 정적분석, 사례연구, Coverity, Sparrow, Clang analyzer Abstract Static analysis tools have been widely used to improve software reliability. However, static analysis tools have limitations that can generate false alarms and can miss real bugs. This paper presents a comparative study of three static analysis tools, Coverity, Sparrow, and Clang analyzer, through a case study on a set of buffer overflow benchmark programs and libexif to evaluate the effectiveness of the three static analysis tools in terms of a bug finding capability. Experiment results on buffer overflow benchmark show that bug detection capabilities of Coverity, Sparrow, and Clang analyzer are 6.02%, 3.61%, and 0%, respectively and false alarm ratios of Coverity, Sparrow, and Clang analyzer are 2.41%, 1.20% and 0%, respectively. Experiment results on libexif show that Coverity, Sparrow, and Clang analyzer detect 745 bugs and miss 6 out of 7 real bugs. Thus, it is necessary to use other bug finding techniques with static analysis techniques for achieving high software reliability, because static analysis tools can miss real bugs in target programs. Keywords: static analysis, case study, coverity, sparrow, clang analyzer 1. 서론 소프트웨어의활용범위가넓어짐에따라소프트웨어의신뢰성이더욱중요해지고있다. 특히의료장비, 우주탐사장비등의다양한종류의기기가소프트웨어로구동되면서소프트웨어의오류로심각한사회, 경제적피해및인명피해가발생한다. 예를들어아리안 5호로켓은 64bit 부동소수점을 16bit 정수형으로변환하던중발생한오류로폭발하여 5억달러의피해를남겼다 [1]. 또다른예로 Therac-25라는방사선의료기기의소프트웨어오류로인해환자가필요이상의많은방사선에노출되어사망하는사고가있었다 [2]. 이러한피해를막기위해서소프트웨어의신뢰성을높이기위한노력이필요하다. 소프트웨어신뢰성을효율적으로높이기위한방법으로정적프로그램분석기법이주목받고있다. 기존에소프트웨어의신뢰성향상을위해표준적으로사용되는소프트웨어테스트는개발자가테스트케이스를수동으로생성하고그결과를분석해야하기때문에비효율적이다. 정적프로그램분석기법은자동화된방식으로프로그램을분석하여프로그램이비정상적으로종료되는오류와 overflow오류등을찾을수있다.
2 사례연구를통한정적프로그램분석기법을사용하는도구의비교 425 본논문에서는상용정적분석도구 Coverity[3] 와 Sparrow[4] 및오픈소스도구 Clang analyzer[5] 를사용하여사례연구를통해버그찾는능력및오탐율을비교하였다. 사례연구는크게두가지로진행하였다. 먼저기존프로그램의 buffer overflow 버그를기반으로생성된소규모 (100~1000LOC) 벤치마크프로그램을대상으로버그찾는능력과오탐율을비교하고규모있는 (9KLOC) 오픈소스라이브러리인 libexif 을대상으로적용하여발생한경보및발견한오류를비교하였다. 실험결과 buffer overflow 벤치마크에서는 Coverity, Sparrow, Clang analyzer 각각 6.02%, 3.61%, 0% 의버그탐지율과 2.41%, 1.20%, 0% 의오탐율을보였다. libexif 적용에서 Coverity, Sparrow, Clang analyzer는총 745개의오류를찾아내었으나알려진 7개의오류중 6개를찾아내지못했다. 2. 정적프로그램분석정적프로그램분석 [6,7] 은프로그램을실제로실행시키지않고분석하여프로그램소스코드를실행하였을때나타나는오류를찾아내는방법이다. 분석방법은프로그램이실행가능한경로, 프로그램의변수가가질수있는값의범위등을추상화하여분석하고가능한실행경로나값의범위가프로그램오류가발생하는조건을만족하는지검사하여오류가발생하는부분을찾아내는것이다. 정적프로그램분석방법을사용하여동적으로할당한메모리자원, 0으로나누는연산, 잘못된메모리접근과같은오류를효과적으로찾아낼수있다. 정적프로그램분석은프로그램을실행시키지않고분석하기때문에실제프로그램이수행될만큼개발이진행되지않아도개발도중에적용할수있고, 프로그램을실제실행하여분석하는방법인동적프로그램분석에비해서짧은시간에넓은범위를분석할수있는장점이있다. 또한분석과정이자동화되어있어서개발자가큰노력없이적용할수있다. 이와같은장점에힘입어 Coverity, Sparrow, Clang analyzer와같은다양한도구들이개발되어사용되고있다. 하지만, 정적프로그램분석기법은프로그램이가질수있는무한한크기의실행경로와프로그램상태를추상화하여유한한크기내에서분석하기때문에이과정에서정확도가떨어져거짓경보를발생할수있다. 거짓경보가발생할경우개발자가직접경보를분석하여실제버그인지아닌지판별해야하기때문에거짓경보가많이발생할경우정적분석을통한개발비용절감보다거짓경보분석에따르는개발비용증가가더커질수있다. 따라서거짓경보를줄이기위한다양한관련연구가진행되고있다 [8]. 또한, 여러정적프로그램분석도구가효율적으로 buffer overflow 오류를찾아내는지를비교하는연구도있다 [9]. 본논문에서는 buffer overflow 오류외에도두도구가찾아낼수있는모든오류를분석하여분류하였다. 3. 실험환경 3.1 도구설정 Coverity 5.4와 Sparrow 4.7 도구는경보가발생하는수준을조절할수있으며 Coverity의경우 3단계가, Sparrow에는 5단계가있다. 낮은단계에서는거짓경보를줄이기위해최소의경보를발생시키고, 높은단계에서는오류를놓치지않기위해최대한많은경보를발생한다. 하지만두도구에서검사할수있는오류의종류와분석강도가서로다르기때문에완전히동일한설정에서의비교는어렵다. 따라서본논문에서는경보분석을위한시간을고려하여두도구가수백개수준의경보를발생할수있는경보발생단계를적용하여비교하였다. Clang analyzer 3.3 도구는경보발생수준을조절하는옵션이없어기본설정으로수행하였다. 각도구는 Intel Core i7 3.4GHz 프로세서와 8GB의메모리가장착된 Debian 서버에서실행하였으며모든분석은 5분내에종료되었다. 1) 3.2 Buffer overflow 벤치마크실험설정각도구의오류찾는능력과오탐율을비교하기위해 buffer overflow 벤치마크 [9] 를대상으로적용하여결과를비교하였다. buffer overflow는 C 프로그램에서자주발생하는버그로발생시프로그램비정상종료및심각한보안버그를야기할수있는치명적인버그이다. 벤치마크프로그램은오픈소스프로그램 BIND, Sendmail, wuftpd에서기존에발견된버그를재현하기위한코드로작성되어있으며크기는 90~800LOC이다. 총 14쌍의테스트케이스로구성되어있으며각테스트케이스는 buffer overflow 버그가있는 BAD 버전과해당버그를수정한 OK 버전한쌍으로구성되어있다. 각 BAD 버전은최소 1개에서최대 28개, 평균 5.9개의 buffer overflow 버그를발생시킬수있는소스코드라인을포함하고있다. Buffer overflow 벤치마크실험에서는미리지정된테스트케이스의오류와관련되지않은경보는무시하였다. 3.3 libexif 실험설정분석대상인 libexif는 Exchangeable Image File Format(EXIF)[10] 형식의이미지파일에포함된정보를읽고쓰기위해사용한다. libexif 은 C 언어소스코드파일 24개와 30개의헤더파일로구성되어있 1) 본논문은 2012 한국컴퓨터종합학술대회추계학술발표회에발표된 정적프로그램분석기법을사용하는도구의비교 : Coverity와 Sparrow 를사용한 libexif 사례연구 논문을확장한것으로기존논문에서적용한 Sparrow의성능을개선한새버전의 Sparrow 를사용하여실험을수행하고결과를분석하였다.
3 426 정보과학회논문지 : 컴퓨팅의실제및레터제 19 권제 8 호 (2013.8) 표 1 Buffer overflow 벤치마크실험결과 Table 1 Experiment results of buffer overflow benchmark Bug detection capability False alarm ratio Coverity 6.02% 2.41% Sparrow 3.61% 1.20% Clang analyzer 0.00% 0.00% 표 2 libexif 에서발생한경보 Table 2 The number of generated alarms for libexif Coverity Sparrow Clang -analyzer Real bugs 147 (84%) 599 (95%) 3 (100%) False alarms 28 (16%) 33 (5%) 0 (0%) Total alarms 175 (100%) 632 (100%) 3 (100%) 으며, 8,922줄이들어있으며함수의개수는 229개이다. libexif를사용한이유는실제널리사용되고있는규모있는오픈소스라이브러리이며알려진오류와찾지못한오류가모두있어서각정적분석도구가얼마나효과적으로오류를찾아내는지확인할수있기때문이다. 공개된버그리포트를확인하고 libexif의최신버전인 버전에서오류를고친부분과비교하면 에서오류가발생하는부분을찾을수있다. 4. 실험결과 4.1 Buffer overflow 벤치마크실험결과표 1은 buffer overflow 벤치마크실험결과를보여준다. Bug detection capability는 BAD 버전의전체 83개의 buffer overflow를야기할수있는소스코드라인중에서각도구가실제오류로찾아낸비율을나타내고 false alarm ratio는 OK 버전에서수정된 83개의소스코드라인중에서오류가있다고경보가발생한수의비율을나타낸다. Coverity의경우 6.02% (=5/83) 의 bug detection capability와 2.41% 의 false alarm ratio(=2/83) 을보였으며 Sparrow의경우 bug detection capability는 3.61%(=3/83) 로 Coverity보다낮았으나 false alarm ratio가 1.20%(=1/83) 로 Coverity보다낮아오탐이적게발생하였다. Clang analyer의경우모든테스트케이스에서경보를발생시키지않았다. Buffer overflow 벤치마크실험결과 Coverity와 Sparrow 의 buffer overflow bug detection capability 는 7% 미만으로낮은것으로나타났다. 상용정적분석도구들은수십만~수백만줄규모의프로그램을분석하면서유용한결과를주기위해오탐율을낮추는다양한휴리스틱알고리즘을적용한다. 이과정에서실제오류인지확실하지않은것으로보일경우오류가아닌것으로간주하여 bug detection capability를낮추더라 도오탐을줄이기위해최대한노력한다. 따라서정적분석도구는프로그램이올바르게작성된것을증명하는도구가아니기때문에정적분석도구가경보를발생시키지않더라도숨어있는버그가있을수있으며높은신뢰성을달성하기위해정적분석도구에만의존하지말고 concolic testing과같은동적분석기법과상호보완하여적용해야한다. 4.2 libexif 실험결과표 2는 Coverity, Sparrow, Clang analyzer로 libexif를분석하여발생한경보의수를나타낸다. Coverity, Sparrow, Clang analyzer는각각 175, 632, 3개의경보를발생시켰고세도구가모두공통적으로발견한경보가 1개있었다. Coverity와 Sparrow는세도구가모두찾은경보외에도 2개의동일한경보를발생시켰으며 Coverity와 Clang analyzer 역시모두찾은경보외에 2개의동일한경보를발생시켰다. Sparrow와 Clang analyzer는모두찾은경보외에동일한경보를발생시키지않았다. 그림 1은경보의종류별로각도구별각각발생시킨경보및공통적으로발생시킨경보를나누어비교한결과이다. 경보는원인에따라서 8가지분류의 17종류로구분하였다. 그림 2, 3, 4는각각 Coverity, Sparrow, Clang analyzer 가찾은실제오류와거짓경보를비교한것이다. 각도구가찾아낸오류와찾지못한오류가있고경보의종류에따른실제오류와거짓경보비율을알수있다 찾아낸실제오류세도구는총 745개의실제오류를찾아내었으며, 그중세도구가공통적으로찾은오류는 1개이다. 찾아낸오류중 에서고친오류도존재하며고쳐지지않은오류도존재한다. 그림 5는 Coverity, Sparrow, Clang analyzer가공통으로발견한 null pointer dereference 오류이다. exif-loader.c 파일의 exif_loader_get_buf() 함수 413 번째줄에서포인터 loader가 NULL일경우조건이참이되어 414 번째줄을실행한다. 하지만 414번째줄에서 exif_log() 함수의첫번째인자에서 loader를참조하므로 null pointer dereference 오류가발생한다. 해당오류는 버전에서아직수정되지않았다. 이처럼정적프로그램분석기법을사용하면개발자가찾기힘든오류까지찾을수있으므로정적프로그램분석으로소프트웨어의신뢰성을향상시킬수있다 발견한경보종류의비교그림 1을봤을때 Coverity의경우 null pointer dereference를포함하여총 12종류의경보를발생시켰으며그중 null pointer dereference를제외한 11종류의경보는 Sparrow가발생시키지않은경보이다. 반면 Sparrow 의경우 null pointer dereference, bad integer constant
4 사례연구를통한정적프로그램분석기법을사용하는도구의비교 427 그림 1 각도구가생성한경보비교 Fig. 1 Alarms generated by Coverity, Sparrow, and Clang analyzer 그림 2 Coverity 가찾은실제오류와발생된거짓경보 Fig. 2 Real bugs and false alarms generated by Coverity 그림 3 Sparrow 가찾은실제오류와발생된거짓경보 Fig. 3 Real bugs and false alarms generated by Sparrow 그림 4 Clang analyzer 가찾은실제오류와발생된거짓경보 Fig. 4 Real bugs and false alarms generated by Clang analyzer
5 428 정보과학회논문지 : 컴퓨팅의실제및레터제 19 권제 8 호 (2013.8) 그림 5 exif-loader.c 에서발생하는 null pointer dereference 오류 Fig. 5 Null pointer dereference error in exif-data.c definition 등총 6종류의경보를발생시켰으며그중 null pointer dereference를제외한 5종류의경보는 Coverity 가발견하지못한경보이다. Clang analyzer는 null pointer dereference와 unused local variable 두종류의경보를발생시켰다. 이와같이각도구는오류를찾기위한경보를발생시키는방식이달라서한도구가찾아낸오류를다른도구에서찾아내지못할수있으며, 최대한많은오류를찾아야한다면여러가지도구를함께사용하는것이효과적이다 찾아내지못한오류 에서수정된 7개오류중 1개를찾아내었으나나머지 6개는찾지못하였다. 그중하나는 libexif 내부의동작과관련된오류로, 정적프로그램분석으로찾을수없으며, 나머지오류는배열범위를벗어난접근오류 3개, buffer overflow 오류 1개, 0으로나누는오류 1개이다. Coverity와 Sparrow는 0으로나누는오류를찾아내는기능이있지만 libexif에있는오류는찾아내지못하였다. 그림 6은 0으로나누는오류가존재하는 과그오류가수정된 을비교한것이다. vr.denominator라는변수는 exif_get_rational에서파일의특정부분의값이대입되며 0이대입될가능성이존재한다. 따라서변수가 0인지확인해야하며, 버전의 80 번줄에 vr.denominator가 0인지확인한후에 vr.denominator로나누는매크로가추가되어 378번줄에서이를사용하도록소스코드가변경되었다. 이오류는 concolic execution 기법을사용하는도구인 CREST-BV는찾아내는오류이며 에서수정된 7개오류가운데 2개오류를 CREST-BV를사용해서발견하였다 [11]. 이처럼정적프로그램분석기법만으로는모든오류를찾아낼수없으므로, concolic execution과같은다른기법을함께사용하는것이필요하다. 5. 결론및향후연구사례연구를통해정적프로그램분석도구를비교하였다. 각도구모두 libexif 의실제오류를발견하 그림 6 mnote-olympus-entry.c에서 ( 위 ) 과 ( 아래 ) 의차이점 Fig. 6 Difference of mnote-olympus-entry.c between (above) and (below) 였으며따라서정적프로그램분석도구는소프트웨어신뢰성을향상시키는데유용하다. 하지만 buffer overflow 벤치마크결과가보여주듯이오탐율을줄이기위해낮은버그탐지율을보일수있고각도구가찾을수있는오류종류가서로다를수있기때문에소프트웨어신뢰성을높이기위해서는여러정적분석도구를같이활용하고 concolic execution과같은다른분석기법을사용하여오류를찾아내는것도필요하다. References [1] J. Jézéquel, B. Meyer, "Design by contract: The lessons of ariane," IEEE Computer, vol.30, no.1, pp , [2] N. Leveson, C. Turner, "An investigation of the therac-25 accidents," IEEE Computer, vol.26, no.7, pp.18-41, [3] Coverity [Online]. Available: (downloaded 2013, Jul. 28) [4] Sparrow [Online]. Available: product/sparrow_overview.asp (downloaded 2013, Jul. 28) [5] Clang analyzer [Online]. Available: (downloaded 2013, Jul. 28) [6] P. Emanuelsson, U. Nilsson, "A comparative study of industrial static analysis tools," Proc. of the 3rd International Workshop on Systems Software Verification (SSV 2008), [7] A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, D. Engler, "A few billion lines of code later: Using static analysis to find bugs in the real world," CACM, vol.53, no.2, pp.66-75, [8] K. Yi, J. Kim, Y. Jung, "Design and Implementation of Static Program Analyzer Finding All Buffer Overrun Errors in C Programs," Journal of KIISE : Software and Applications, vol.33, no.5, pp , [9] M. Zitser, R. Lippmann, T. Leek, "Testing static analysis tools using exploitable buffer overflows from open source code," Proc. of the SIGSOFT '04/FSE-12, [10] JEITA. Exif.org [Online]. Available: exif.org/ (downloaded 2013, Jul. 28) [11] Y. Kim, M. Kim, Y. Kim, Y. Jang, "Industrial application of concolic testing approach: A case study on libexif by using CREST-BV and KLEE," Proc. of the Software Engineering (ICSE), th International Conference, SEIP track, 2012.
2017 년 6 월한국소프트웨어감정평가학회논문지제 13 권제 1 호 Abstract
2017 년 6 월한국소프트웨어감정평가학회논문지제 13 권제 1 호 Abstract - 31 - 소스코드유사도측정도구의성능에관한비교연구 1. 서론 1) Revulytics, Top 20 Countries for Software Piracy and Licence Misuse (2017), March 21, 2017. www.revulytics.com/blog/top-20-countries-software
More informationexample code are examined in this stage The low pressure pressurizer reactor trip module of the Plant Protection System was programmed as subject for
2003 Development of the Software Generation Method using Model Driven Software Engineering Tool,,,,, Hoon-Seon Chang, Jae-Cheon Jung, Jae-Hack Kim Hee-Hwan Han, Do-Yeon Kim, Young-Woo Chang Wang Sik, Moon
More information인문사회과학기술융합학회
Vol.5, No.5, October (2015), pp.471-479 http://dx.doi.org/10.14257/ajmahs.2015.10.50 스마트온실을 위한 가상 외부기상측정시스템 개발 한새론 1), 이재수 2), 홍영기 3), 김국환 4), 김성기 5), 김상철 6) Development of Virtual Ambient Weather Measurement
More information09권오설_ok.hwp
(JBE Vol. 19, No. 5, September 2014) (Regular Paper) 19 5, 2014 9 (JBE Vol. 19, No. 5, September 2014) http://dx.doi.org/10.5909/jbe.2014.19.5.656 ISSN 2287-9137 (Online) ISSN 1226-7953 (Print) a) Reduction
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. vol. 29, no. 6, Jun Rate). STAP(Space-Time Adaptive Processing)., -
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2018 Jun.; 29(6), 457463. http://dx.doi.org/10.5515/kjkiees.2018.29.6.457 ISSN 1226-3133 (Print)ISSN 2288-226X (Online) Sigma-Delta
More informationDBPIA-NURIMEDIA
e- 비즈니스연구 (The e-business Studies) Volume 17, Number 1, February, 28, 2016:pp. 293~316 ISSN 1229-9936 (Print), ISSN 2466-1716 (Online) 원고접수일심사 ( 수정 ) 게재확정일 2015. 12. 04 2015. 12. 24 2016. 02. 25 ABSTRACT
More information<31325FB1E8B0E6BCBA2E687770>
88 / 한국전산유체공학회지 제15권, 제1호, pp.88-94, 2010. 3 관내 유동 해석을 위한 웹기반 자바 프로그램 개발 김 경 성, 1 박 종 천 *2 DEVELOPMENT OF WEB-BASED JAVA PROGRAM FOR NUMERICAL ANALYSIS OF PIPE FLOW K.S. Kim 1 and J.C. Park *2 In general,
More informationÀ±½Â¿í Ãâ·Â
Representation, Encoding and Intermediate View Interpolation Methods for Multi-view Video Using Layered Depth Images The multi-view video is a collection of multiple videos, capturing the same scene at
More information지능정보연구제 16 권제 1 호 2010 년 3 월 (pp.71~92),.,.,., Support Vector Machines,,., KOSPI200.,. * 지능정보연구제 16 권제 1 호 2010 년 3 월
지능정보연구제 16 권제 1 호 2010 년 3 월 (pp.71~92),.,.,., Support Vector Machines,,., 2004 5 2009 12 KOSPI200.,. * 2009. 지능정보연구제 16 권제 1 호 2010 년 3 월 김선웅 안현철 社 1), 28 1, 2009, 4. 1. 지능정보연구제 16 권제 1 호 2010 년 3 월 Support
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. vol. 29, no. 10, Oct ,,. 0.5 %.., cm mm FR4 (ε r =4.4)
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2018 Oct.; 29(10), 799 804. http://dx.doi.org/10.5515/kjkiees.2018.29.10.799 ISSN 1226-3133 (Print) ISSN 2288-226X (Online) Method
More informationDE1-SoC Board
실습 1 개발환경 DE1-SoC Board Design Tools - Installation Download & Install Quartus Prime Lite Edition http://www.altera.com/ Quartus Prime (includes Nios II EDS) Nios II Embedded Design Suite (EDS) is automatically
More information°í¼®ÁÖ Ãâ·Â
Performance Optimization of SCTP in Wireless Internet Environments The existing works on Stream Control Transmission Protocol (SCTP) was focused on the fixed network environment. However, the number of
More informationContents Contents 2 1 Abstract 3 2 Infer Checkers Eradicate Infer....
SV2016 정적분석보고서 201214262 라가영 201313250 서지혁 June 9, 2016 1 Contents Contents 2 1 Abstract 3 2 Infer 3 2.1 Checkers................................ 3 2.2 Eradicate............................... 3 2.3 Infer..................................
More informationHigh Resolution Disparity Map Generation Using TOF Depth Camera In this paper, we propose a high-resolution disparity map generation method using a lo
High Resolution Disparity Map Generation Using TOF Depth Camera In this paper, we propose a high-resolution disparity map generation method using a low-resolution Time-Of- Flight (TOF) depth camera and
More informationMicrosoft Word - KSR2016S168
2016 년도 한국철도학회 춘계학술대회 논문집 KSR2016S168 GPR 을 이용한 자갈궤도 파울링층 파악을 위한 실내실험적 접근 Evaluation of Applicability of GPR to Detect Fouled Layer in Ballast Using Laboratory Tests 신지훈 *, 최영태 **, 장승엽 *** Ji-hoon. Shin
More informationMicrosoft PowerPoint - chap02-C프로그램시작하기.pptx
#include int main(void) { int num; printf( Please enter an integer "); scanf("%d", &num); if ( num < 0 ) printf("is negative.\n"); printf("num = %d\n", num); return 0; } 1 학습목표 을 작성하면서 C 프로그램의
More informationuntitled
PMIS 발전전략 수립사례 A Case Study on the Development Strategy of Project Management Information System 류 원 희 * 이 현 수 ** 김 우 영 *** 유 정 호 **** Yoo, Won-Hee Lee, Hyun-Soo Kim, Wooyoung Yu, Jung-Ho 요 약 건설업무의 효율성
More informationDBPIA-NURIMEDIA
무선 센서 네트워크 환경에서 링크 품질에 기반한 라우팅에 대한 효과적인 싱크홀 공격 탐지 기법 901 무선 센서 네트워크 환경에서 링크 품질에 기반한 라우팅에 대한 효과적인 싱크홀 공격 탐지 기법 (A Effective Sinkhole Attack Detection Mechanism for LQI based Routing in WSN) 최병구 조응준 (Byung
More informationBMP 파일 처리
BMP 파일처리 김성영교수 금오공과대학교 컴퓨터공학과 학습내용 영상반전프로그램제작 2 Inverting images out = 255 - in 3 /* 이프로그램은 8bit gray-scale 영상을입력으로사용하여반전한후동일포맷의영상으로저장한다. */ #include #include #define WIDTHBYTES(bytes)
More informationFigure 1: 현존하는 정적 분석 기술의 한계와 본 연구의 목표. 이러한 허위경보(false alarm)를 가질 수 밖에 없는데, 오탐율(전체 경보중 허위경보의 비율)이 정확도의 척도가 된다. 유용한 정적 분석기는 충분히 낮은 허위경보율을 가져야 한다. 대형 프로그
고성능 정적 프로그램 분석 기법 오학주 고려대학교 컴퓨터학과 서론 1 1.1 소프트웨어 오류 문제 소프트웨어가 모든 산업의 기반 기술이 되면서 소프트웨어의 오류로 인해 발생하는 사회경제적 비 용이 천문학적으로 증가하고 있다. 한 예로 미국의 투자금융회사인 KCG(Knight Capital Group)은 2012년 8월 1일 하루동안 2년치의 매출액에 해당하는
More information<353420B1C7B9CCB6F52DC1F5B0ADC7F6BDC7C0BB20C0CCBFEBC7D120BEC6B5BFB1B3C0B0C7C1B7CEB1D7B7A52E687770>
Journal of the Korea Academia-Industrial cooperation Society Vol. 13, No. 2 pp. 866-871, 2012 http://dx.doi.org/10.5762/kais.2012.13.2.866 증강현실을 이용한 아동교육프로그램 모델제안 권미란 1*, 김정일 2 1 나사렛대학교 아동학과, 2 한세대학교 e-비즈니스학과
More information45-51 ¹Ú¼ø¸¸
A Study on the Automation of Classification of Volume Reconstruction for CT Images S.M. Park 1, I.S. Hong 2, D.S. Kim 1, D.Y. Kim 1 1 Dept. of Biomedical Engineering, Yonsei University, 2 Dept. of Radiology,
More informationOutput file
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 An Application for Calculation and Visualization of Narrative Relevance of Films Using Keyword Tags Choi Jin-Won (KAIST) Film making
More information(JBE Vol. 21, No. 1, January 2016) (Regular Paper) 21 1, (JBE Vol. 21, No. 1, January 2016) ISSN 228
(JBE Vol. 1, No. 1, January 016) (Regular Paper) 1 1, 016 1 (JBE Vol. 1, No. 1, January 016) http://dx.doi.org/10.5909/jbe.016.1.1.60 ISSN 87-9137 (Online) ISSN 16-7953 (Print) a), a) An Efficient Method
More information05(533-537) CPLV12-04.hwp
모바일 OS 환경의 사용자 반응성 향상 기법 533 모바일 OS 환경의 사용자 반응성 향상 기법 (Enhancing Interactivity in Mobile Operating Systems) 배선욱 김정한 (Sunwook Bae) 엄영익 (Young Ik Eom) (Junghan Kim) 요 약 사용자 반응성은 컴퓨팅 시스템에서 가장 중요 한 요소 중에 하나이고,
More information<333820B1E8C8AFBFEB2D5A6967626565B8A620C0CCBFEBC7D120BDC7BFDC20C0A7C4A1C3DFC1A42E687770>
Journal of the Korea Academia-Industrial cooperation Society Vol. 13, No. 1 pp. 306-310, 2012 http://dx.doi.org/10.5762/kais.2012.13.1.306 Zigbee를 이용한 실외 위치추정 시스템 구현 김환용 1*, 임순자 1 1 원광대학교 전자공학과 Implementation
More informationMicrosoft Word - KSR2012A021.doc
YWXY G ºG ºG t G G GGGGGGGGGrzyYWXYhWYXG Ÿƒ Ÿ ± k ¹Ÿˆ Review about the pantograph field test result adapted for HEMU-430X (1) ÕÕÛ äñ ã G Ki-Nam Kim, Tae-Hwan Ko * Abstract In this paper, explain differences
More information3. 클라우드 컴퓨팅 상호 운용성 기반의 서비스 평가 방법론 개발.hwp
보안공학연구논문지 Journal of Security Engineering Vol.11, No.4 (2014), pp.299-312 http://dx.doi.org/10.14257/jse.2014.08.03 클라우드 컴퓨팅 상호 운용성 기반의 서비스 평가 방법론 개발 이강찬 1), 이승윤 2), 양희동 3), 박철우 4) Development of Service
More informationDBPIA-NURIMEDIA
The e-business Studies Volume 17, Number 4, August, 30, 2016:319~332 Received: 2016/07/28, Accepted: 2016/08/28 Revised: 2016/08/27, Published: 2016/08/30 [ABSTRACT] This paper examined what determina
More information<35335FBCDBC7D1C1A42DB8E2B8AEBDBAC5CDC0C720C0FCB1E2C0FB20C6AFBCBA20BAD0BCAE2E687770>
Journal of the Korea Academia-Industrial cooperation Society Vol. 15, No. 2 pp. 1051-1058, 2014 http://dx.doi.org/10.5762/kais.2014.15.2.1051 멤리스터의 전기적 특성 분석을 위한 PSPICE 회로 해석 김부강 1, 박호종 2, 박용수 3, 송한정 1*
More information13 Who am I? R&D, Product Development Manager / Smart Worker Visualization SW SW KAIST Software Engineering Computer Engineering 3
13 Lightweight BPM Engine SW 13 Who am I? R&D, Product Development Manager / Smart Worker Visualization SW SW KAIST Software Engineering Computer Engineering 3 BPM? 13 13 Vendor BPM?? EA??? http://en.wikipedia.org/wiki/business_process_management,
More informationJournal of Educational Innovation Research 2019, Vol. 29, No. 1, pp DOI: (LiD) - - * Way to
Journal of Educational Innovation Research 2019, Vol. 29, No. 1, pp.353-376 DOI: http://dx.doi.org/10.21024/pnuedi.29.1.201903.353 (LiD) -- * Way to Integrate Curriculum-Lesson-Evaluation using Learning-in-Depth
More information09김정식.PDF
00-09 2000. 12 ,,,,.,.,.,,,,,,.,,..... . 1 1 7 2 9 1. 9 2. 13 3. 14 3 16 1. 16 2. 21 3. 39 4 43 1. 43 2. 52 3. 56 4. 66 5. 74 5 78 1. 78 2. 80 3. 86 6 88 90 Ex e cu t iv e Su m m a r y 92 < 3-1> 22 < 3-2>
More informationObservational Determinism for Concurrent Program Security
웹응용프로그램보안취약성 분석기구현 소프트웨어무결점센터 Workshop 2010. 8. 25 한국항공대학교, 안준선 1 소개 관련연구 Outline Input Validation Vulnerability 연구내용 Abstract Domain for Input Validation Implementation of Vulnerability Analyzer 기존연구
More information6.24-9년 6월
리눅스 환경에서Solid-State Disk 성능 최적화를 위한 디스크 입출력요구 변환 계층 김태웅 류준길 박찬익 Taewoong Kim Junkil Ryu Chanik Park 포항공과대학교 컴퓨터공학과 {ehoto, lancer, cipark}@postech.ac.kr 요약 SSD(Solid-State Disk)는 여러 개의 낸드 플래시 메모리들로 구성된
More information02(243-249) CSTV11-22.hwp
함수호출규약에 기반한 새로운 소프트웨어 워터마킹 기법 243 함수호출규약에 기반한 새로운 소프트웨어 워터마킹 기법 (A Novel Software Watermarking Scheme Based on Calling Convention) 전 철 정진만 김봉재 (Cheol Jeon) (Jinman Jung) (Bongjae Kim) 장준혁 조유근 홍지만 (Joonhyouk
More information저작자표시 - 비영리 - 변경금지 2.0 대한민국 이용자는아래의조건을따르는경우에한하여자유롭게 이저작물을복제, 배포, 전송, 전시, 공연및방송할수있습니다. 다음과같은조건을따라야합니다 : 저작자표시. 귀하는원저작자를표시하여야합니다. 비영리. 귀하는이저작물을영리목적으로이용할
저작자표시 - 비영리 - 변경금지 2.0 대한민국 이용자는아래의조건을따르는경우에한하여자유롭게 이저작물을복제, 배포, 전송, 전시, 공연및방송할수있습니다. 다음과같은조건을따라야합니다 : 저작자표시. 귀하는원저작자를표시하여야합니다. 비영리. 귀하는이저작물을영리목적으로이용할수없습니다. 변경금지. 귀하는이저작물을개작, 변형또는가공할수없습니다. 귀하는, 이저작물의재이용이나배포의경우,
More information03-서연옥.hwp
농업생명과학연구 49(4) pp.31-37 Journal of Agriculture & Life Science 49(4) pp.31-37 Print ISSN 1598-5504 Online ISSN 2383-8272 http://dx.doi.org/10.14397/jals.2015.49.4.31 국가산림자원조사 자료를 적용한 충남지역 사유림경영율 추정 서연옥
More information878 Yu Kim, Dongjae Kim 지막 용량수준까지도 멈춤 규칙이 만족되지 않아 시행이 종료되지 않는 경우에는 MTD의 추정이 불가 능하다는 단점이 있다. 최근 이 SM방법의 단점을 보완하기 위해 O Quigley 등 (1990)이 제안한 CRM(Continu
한 국 통 계 학 회 논 문 집 2012, 19권, 6호, 877 884 DOI: http://dx.doi.org/10.5351/ckss.2012.19.6.877 Maximum Tolerated Dose Estimation Applied Biased Coin Design in a Phase Ⅰ Clinical Trial Yu Kim a, Dongjae Kim
More information=10100 =minusby by1000 ÇÁto0.03exÇÁto0.03exÇÁ=10100 =minusby by1000 ·Îto0.03ex·Îto0.03ex·Î=10100 =minusby by1000 ±×to0.03ex±×to0.03ex±×=10100 =minusby by1000 ·¥to0.03ex·¥to0.03ex·¥=10100 =minusby by1000 ºÐto0.03exºÐto0.03exºÐ=10100 =minusby by1000 ¼®to0.03ex¼®to0.03ex¼®. SW=10100 =minusby by1000 ¿Àto0.03ex¿Àto0.03ex¿À=10100 =minusby by1000 ·ùto0.03ex·ùto0.03ex·ù=10100 =minusby by1000 °Ëto0.03ex°Ëto0.03ex°Ë=10100 =minusby by1000 Áõto0.03exÁõto0.03exÁõ. =10100 =minusby by1000 »êto0.03ex»êto0.03ex»ê=10100 =minusby by1000 °úto0.03ex°úto0.03ex°ú=10100 =minusby by1000 °ñto0.03ex°ñto0.03ex°ñ. =10100 =minusby by1000 ¹Ìto0.03ex¹Ìto0.03ex¹Ì=10100 =minusby by1000 °³to0.03ex°³to0.03ex°³=10100 =minusby by1000 ÇÑto0.03exÇÑto0.03exÇÑ.
프로그램분석. SW오류검증. 산과골. 미개한. 08/29/2011 @ 학부교수점심발표 문제 작성한 SW 의오류를자동으로미리모두찾아주거나, 없으면없다고확인해주는기술들은있는가? 그래서, SW 의오류때문에발생하는 개인 / 기업 / 국가 / 사회적비용을 절감시켜주는기술들은있는가? 목표 소프트웨어 MRI 소프트웨어 fmri 소프트웨어 PET 기반기술 정적프로그램분석
More informationMicrosoft PowerPoint - ch07 - 포인터 pm0415
2015-1 프로그래밍언어 7. 포인터 (Pointer), 동적메모리할당 2015 년 4 월 4 일 교수김영탁 영남대학교공과대학정보통신공학과 (Tel : +82-53-810-2497; Fax : +82-53-810-4742 http://antl.yu.ac.kr/; E-mail : ytkim@yu.ac.kr) Outline 포인터 (pointer) 란? 간접참조연산자
More informationDBPIA-NURIMEDIA
박건수 *, 서태영 **, 김종욱 *** ". 요약 Abstract The induction melting furnace using electric generator has been introduced since 1920s, and it began to be widely applied to industrial applications due to increasing
More information<31362DB1E8C7FDBFF82DC0FABFB9BBEA20B5B6B8B3BFB5C8ADC0C720B1B8C0FC20B8B6C4C9C6C32E687770>
Journal of the Korea Academia-Industrial cooperation Society Vol. 13, No. 4 pp. 1525-1531, 2012 http://dx.doi.org/10.5762/kais.2012.13.4.1525 저예산 독립영화의 구전 마케팅을 위한 스마트폰 모바일 애플리케이션 모델 개발 연구 김혜원 1* 1 청운대학교
More information에너지경제연구제 16 권제 1 호 Korean Energy Economic Review Volume 16, Number 1, March 2017 : pp. 95~118 학술 탄소은행제의가정용전력수요절감효과 분석 1) 2) 3) * ** *** 95
에너지경제연구제 16 권제 1 호 Korean Energy Economic Review Volume 16, Number 1, March 2017 : pp. 95~118 학술 탄소은행제의가정용전력수요절감효과 분석 1) 2) 3) * ** *** 95 Intended Nationally Determined Contributions 96 97 98 99 100 101
More information<5B313132385D32303039B3E220C1A634B1C720C1A632C8A320B3EDB9AEC1F628C3D6C1BE292E687770>
디지털 영상에서의 자막추출을 이용한 자막 특성 분석에 관한 연구 이세열 * 요약 본 연구는 방송 프로그램 제작에 있어서 중요한 역할을 담당하고 있는 영상 자막의 특성과 영상 커 뮤니케이션 기능적인 관점에서 나타나고 있는 현상을 살펴본다. 다양한 방송 프로그램에서 활용되고 있는 디지털 영상 자막의 기능은 단순하게 간략한 정보를 전달하는 기능적인 역할을 수행하였다.
More information사단법인 커뮤니케이션디자인협회 시각디자인학회
소도시 공공디자인 기본계획의 실효성 및 지속성 제고에 관한 연구 - 고성군을 중심으로 - Study on Public Design Master Plan to enhance the effectiveness and sustainability - Focusing on Goseong-Gun - 주저자 김정범 Kim, Jungbum 경동대학교 디자인학과 교수 Professor
More informationEndNote X2 초급 분당차병원도서실사서최근영 ( )
EndNote X2 초급 2008. 9. 25. 사서최근영 (031-780-5040) EndNote Thomson ISI Research Soft의 bibliographic management Software 2008년 9월현재 X2 Version 사용 참고문헌 (Reference), Image, Fulltext File 등 DB 구축 참고문헌 (Reference),
More information09È«¼®¿µ5~152s
Korean Journal of Remote Sensing, Vol.23, No.2, 2007, pp.45~52 Measurement of Backscattering Coefficients of Rice Canopy Using a Ground Polarimetric Scatterometer System Suk-Young Hong*, Jin-Young Hong**,
More informationU.Tu System Application DW Service AGENDA 1. 개요 4. 솔루션 모음 1.1. 제안의 배경 및 목적 4.1. 고객정의 DW구축에 필요한 메타정보 생성 1.2. 제품 개요 4.2. 사전 변경 관리 1.3. 제품 특장점 4.3. 부품화형
AGENDA 1. 개요 4. 솔루션 모음 1.1. 제안의 배경 및 목적 4.1. 고객정의 DW구축에 필요한 메타정보 생성 1.2. 제품 개요 4.2. 사전 변경 관리 1.3. 제품 특장점 4.3. 부품화형 언어 변환 1.4. 기대 효과 4.4. 프로그램 Restructuring 4.5. 소스 모듈 관리 2. SeeMAGMA 적용 전략 2.1. SeeMAGMA
More informationPowerPoint 프레젠테이션
System Software Experiment 1 Lecture 5 - Array Spring 2019 Hwansoo Han (hhan@skku.edu) Advanced Research on Compilers and Systems, ARCS LAB Sungkyunkwan University http://arcs.skku.edu/ 1 배열 (Array) 동일한타입의데이터가여러개저장되어있는저장장소
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Sep.; 30(9),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2019 Sep.; 30(9), 712 717. http://dx.doi.org/10.5515/kjkiees.2019.30.9.712 ISSN 1226-3133 (Print) ISSN 2288-226X (Online) MOS
More information06_ÀÌÀçÈÆ¿Ü0926
182 183 184 / 1) IT 2) 3) IT Video Cassette Recorder VCR Personal Video Recorder PVR VCR 4) 185 5) 6) 7) Cloud Computing 8) 186 VCR P P Torrent 9) avi wmv 10) VCR 187 VCR 11) 12) VCR 13) 14) 188 VTR %
More information- iii - - i - - ii - - iii - 국문요약 종합병원남자간호사가지각하는조직공정성 사회정체성과 조직시민행동과의관계 - iv - - v - - 1 - - 2 - - 3 - - 4 - - 5 - - 6 - - 7 - - 8 - - 9 - - 10 - - 11 - - 12 - - 13 - - 14 - α α α α - 15 - α α α α α α
More information디지털포렌식학회 논문양식
ISSN : 1976-5304 http://www.kdfs.or.kr Virtual Online Game(VOG) 환경에서의 디지털 증거수집 방법 연구 이 흥 복, 정 관 모, 김 선 영 * 대전지방경찰청 Evidence Collection Process According to the Way VOG Configuration Heung-Bok Lee, Kwan-Mo
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Jul.; 27(7),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 16 Jul.; 27(7), 64662. http://dx.doi.org/./kjkiees.16.27.7.646 ISSN 1226-3133 (Print)ISSN 2288-226 (Online) 2D Microwave Image
More information슬라이드 1
-Part3- 제 4 장동적메모리할당과가변인 자 학습목차 4.1 동적메모리할당 4.1 동적메모리할당 4.1 동적메모리할당 배울내용 1 프로세스의메모리공간 2 동적메모리할당의필요성 4.1 동적메모리할당 (1/6) 프로세스의메모리구조 코드영역 : 프로그램실행코드, 함수들이저장되는영역 스택영역 : 매개변수, 지역변수, 중괄호 ( 블록 ) 내부에정의된변수들이저장되는영역
More informationDBPIA-NURIMEDIA
The e-business Studies Volume 17, Number 6, December, 30, 2016:275~289 Received: 2016/12/02, Accepted: 2016/12/22 Revised: 2016/12/20, Published: 2016/12/30 [ABSTRACT] SNS is used in various fields. Although
More informationÆ÷Àå½Ã¼³94š
Cho, Mun Jin (E-mail: mjcho@ex.co.kr) ABSTRACT PURPOSES : The performance of tack coat, commonly used for layer interface bonding, is affected by application rate and curing time. In this study, bonding
More information목차 BUG 문법에맞지않는질의문수행시, 에러메시지에질의문의일부만보여주는문제를수정합니다... 3 BUG ROUND, TRUNC 함수에서 DATE 포맷 IW 를추가지원합니다... 5 BUG ROLLUP/CUBE 절을포함하는질의는 SUBQUE
ALTIBASE HDB 6.3.1.10.1 Patch Notes 목차 BUG-45710 문법에맞지않는질의문수행시, 에러메시지에질의문의일부만보여주는문제를수정합니다... 3 BUG-45730 ROUND, TRUNC 함수에서 DATE 포맷 IW 를추가지원합니다... 5 BUG-45760 ROLLUP/CUBE 절을포함하는질의는 SUBQUERY REMOVAL 변환을수행하지않도록수정합니다....
More information저작자표시 - 비영리 - 변경금지 2.0 대한민국 이용자는아래의조건을따르는경우에한하여자유롭게 이저작물을복제, 배포, 전송, 전시, 공연및방송할수있습니다. 다음과같은조건을따라야합니다 : 저작자표시. 귀하는원저작자를표시하여야합니다. 비영리. 귀하는이저작물을영리목적으로이용할
저작자표시 - 비영리 - 변경금지 2.0 대한민국 이용자는아래의조건을따르는경우에한하여자유롭게 이저작물을복제, 배포, 전송, 전시, 공연및방송할수있습니다. 다음과같은조건을따라야합니다 : 저작자표시. 귀하는원저작자를표시하여야합니다. 비영리. 귀하는이저작물을영리목적으로이용할수없습니다. 변경금지. 귀하는이저작물을개작, 변형또는가공할수없습니다. 귀하는, 이저작물의재이용이나배포의경우,
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Jan.; 26(1),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2015 Jan.; 26(1), 113118. http://dx.doi.org/10.5515/kjkiees.2015.26.1.113 ISSN 1226-3133 (Print)ISSN 2288-226X (Online) A Retro-Directive
More information???? 1
The Korean Journal of Applied Statistics (2014) 27(1), 13 20 DOI: http://dx.doi.org/10.5351/kjas.2014.27.1.013 Maximum Tolerated Dose Estimation by Stopping Rule and SM3 Design in a Phase I Clinical Trial
More informationFrama-C/JESSIS 사용법 소개
Frama-C 프로그램검증시스템소개 박종현 @ POSTECH PL Frama-C? C 프로그램대상정적분석도구 플러그인구조 JESSIE Wp Aorai Frama-C 커널 2 ROSAEC 2011 동계워크샵 @ 통영 JESSIE? Frama-C 연역검증플러그인 프로그램분석 검증조건추출 증명 Hoare 논리에기초한프로그램검증도구 사용법 $ frama-c jessie
More informationISP and CodeVisionAVR C Compiler.hwp
USBISP V3.0 & P-AVRISP V1.0 with CodeVisionAVR C Compiler http://www.avrmall.com/ November 12, 2007 Copyright (c) 2003-2008 All Rights Reserved. USBISP V3.0 & P-AVRISP V1.0 with CodeVisionAVR C Compiler
More informationuntitled
전방향카메라와자율이동로봇 2006. 12. 7. 특허청전기전자심사본부유비쿼터스심사팀 장기정 전방향카메라와자율이동로봇 1 Omnidirectional Cameras 전방향카메라와자율이동로봇 2 With Fisheye Lens 전방향카메라와자율이동로봇 3 With Multiple Cameras 전방향카메라와자율이동로봇 4 With Mirrors 전방향카메라와자율이동로봇
More information국립국어원 2011-01-28 발간 등록 번호 11-1371028-000350-01 신문과 방송의 언어 사용 실태 조사 연구 책임자: 남영신 국립국어원 2011-01-28 발간 등록 번호 11-1371028-000350-01 신문과 방송의 언어 사용 실태 조사 연구 책임자: 남영신 2011. 11. 16. 제 출 문 국립국어원장 귀하 2011년 신문과 방송의
More informationDBPIA-NURIMEDIA
e- 비즈니스연구 (The e-business Studies) Volume 17, Number 3, June, 30, 2016:pp. 93~116 ISSN 1229-9936 (Print), ISSN 2466-1716 (Online) 원고접수일심사 ( 수정 ) 게재확정일 2016. 06. 12 2016. 06. 20 2016. 06. 26 ABSTRACT e-
More informationMicrosoft PowerPoint - chap01-C언어개요.pptx
#include int main(void) { int num; printf( Please enter an integer: "); scanf("%d", &num); if ( num < 0 ) printf("is negative.\n"); printf("num = %d\n", num); return 0; } 1 학습목표 프로그래밍의 기본 개념을
More informationDBPIA-NURIMEDIA
한국소음진동공학회 2015추계학술대회논문집년 Study of Noise Pattern and Psycho-acoustics Characteristic of Household Refrigerator * * ** ** Kyung-Soo Kong, Dae-Sik Shin, Weui-Bong Jeong, Tae-Hoon Kim and Se-Jin Ahn Key Words
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Feb.; 29(2), IS
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2018 Feb.; 29(2), 93 98. http://dx.doi.org/10.5515/kjkiees.2018.29.2.93 ISSN 1226-3133 (Print) ISSN 2288-226X (Online) UHF-HF
More information슬라이드 1
Pairwise Tool & Pairwise Test NuSRS 200511305 김성규 200511306 김성훈 200614164 김효석 200611124 유성배 200518036 곡진화 2 PICT Pairwise Tool - PICT Microsoft 의 Command-line 기반의 Free Software www.pairwise.org 에서다운로드후설치
More informationuntitled
시스템소프트웨어 : 운영체제, 컴파일러, 어셈블러, 링커, 로더, 프로그래밍도구등 소프트웨어 응용소프트웨어 : 워드프로세서, 스프레드쉬트, 그래픽프로그램, 미디어재생기등 1 n ( x + x +... + ) 1 2 x n 00001111 10111111 01000101 11111000 00001111 10111111 01001101 11111000
More information서론 34 2
34 2 Journal of the Korean Society of Health Information and Health Statistics Volume 34, Number 2, 2009, pp. 165 176 165 진은희 A Study on Health related Action Rates of Dietary Guidelines and Pattern of
More information우리들이 일반적으로 기호
일본지방자치체( 都 道 府 縣 )의 웹사이트상에서 심벌마크와 캐릭터의 활용에 관한 연구 A Study on the Application of Japanese Local Self-Government's Symbol Mark and Character on Web. 나가오카조형대학( 長 岡 造 形 大 學 ) 대학원 조형연구과 김 봉 수 (Kim Bong Su) 193
More information에너지경제연구 Korean Energy Economic Review Volume 17, Number 2, September 2018 : pp. 1~29 정책 용도별특성을고려한도시가스수요함수의 추정 :, ARDL,,, C4, Q4-1 -
에너지경제연구 Korean Energy Economic Review Volume 17, Number 2, September 2018 : pp. 1~29 정책 용도별특성을고려한도시가스수요함수의 추정 :, ARDL,,, C4, Q4-1 - . - 2 - . 1. - 3 - [ 그림 1] 도시가스수요와실질 GDP 추이 - 4 - - 5 - - 6 - < 표 1>
More information11장 포인터
Dynamic Memory and Linked List 1 동적할당메모리의개념 프로그램이메모리를할당받는방법 정적 (static) 동적 (dynamic) 정적메모리할당 프로그램이시작되기전에미리정해진크기의메모리를할당받는것 메모리의크기는프로그램이시작하기전에결정 int i, j; int buffer[80]; char name[] = data structure"; 처음에결정된크기보다더큰입력이들어온다면처리하지못함
More informationJournal of Educational Innovation Research 2019, Vol. 29, No. 1, pp DOI: * Suggestions of Ways
Journal of Educational Innovation Research 2019, Vol. 29, No. 1, pp.65-89 DOI: http://dx.doi.org/10.21024/pnuedi.29.1.201903.65 * Suggestions of Ways to Improve Teaching Practicum Based on the Experiences
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Mar.; 25(3),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2014 Mar.; 25(3), 304310. http://dx.doi.org/10.5515/kjkiees.2014.25.3.304 ISSN 1226-3133 (Print)ISSN 2288-226X (Online) Analysis
More informationuntitled
MDEP I&C 2009. 4.6 ~ 4.7 14 I. MDEP II. DICWG III. DICWG SW IV. Nuclear Safety Information Conference 2009 Slide -2- I. MDEP MDEP? Multinational Design Evaluation Program MDEP Nuclear Safety Information
More informationHW5 Exercise 1 (60pts) M interpreter with a simple type system M. M. M.., M (simple type system). M, M. M., M.
오늘할것 5 6 HW5 Exercise 1 (60pts) M interpreter with a simple type system M. M. M.., M (simple type system). M, M. M., M. Review: 5-2 7 7 17 5 4 3 4 OR 0 2 1 2 ~20 ~40 ~60 ~80 ~100 M 언어 e ::= const constant
More information정보기술응용학회 발표
, hsh@bhknuackr, trademark21@koreacom 1370, +82-53-950-5440 - 476 - :,, VOC,, CBML - Abstract -,, VOC VOC VOC - 477 - - 478 - Cost- Center [2] VOC VOC, ( ) VOC - 479 - IT [7] Knowledge / Information Management
More information<33312D312D313220C0CCC7D1C1F820BFB0C3A2BCB12E687770>
Journal of the Society of Korea Industrial and Systems Engineering Vol No pp March 8 Scatter Search를 이용한 신뢰성 있는 네트워크의 경제적 설계 * ** * ** Economic Design of Reliable Networks Using Scatter Search HanJin Lee*
More informationJournal of Educational Innovation Research 2018, Vol. 28, No. 3, pp DOI: NCS : * A Study on
Journal of Educational Innovation Research 2018, Vol. 28, No. 3, pp.157-176 DOI: http://dx.doi.org/10.21024/pnuedi.28.3.201809.157 NCS : * A Study on the NCS Learning Module Problem Analysis and Effective
More informationMicrosoft Word - PLC제어응용-2차시.doc
과정명 PLC 제어응용차시명 2 차시. 접점명령 학습목표 1. 연산개시명령 (LOAD, LOAD NOT) 에대하여설명할수있다. 2. 직렬접속명령 (AND, AND NOT) 에대하여설명할수있다. 3. 병렬접속명령 (OR, OR NOT) 에대하여설명할수있다. 4.PLC의접점명령을가지고간단한프로그램을작성할수있다. 학습내용 1. 연산개시명령 1) 연산개시명령 (LOAD,
More information10( ) CPLV11-90.hwp
Concolic Testing 도구 KLEE 의다양한탐색방법비교 321 Concolic Testing 도구 KLEE 의다양한탐색방법비교 (Comparison of Search Strategies of KLEE Concolic Testing Tool) 김영주 김문주 (YoungJoo Kim) (Moonzoo Kim) 김윤호 정의준 (Yunho Kim) (Uijune
More information에너지경제연구 제13권 제1호
에너지경제연구 Korean Energy Economic Review Volume 13, Number 1, March 2014 : pp. 83~119 거시계량모형을이용한유가변동및 유류세변화의파급효과분석 * 83 84 85 86 [ 그림 1] 모형의해결정과정 87 [ 그림 2] 거시계량모형의흐름도 (flow chart) 88 89 < 표 1> 유류세현황 (2013
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Nov.; 26(11),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2015 Nov.; 26(11), 985991. http://dx.doi.org/10.5515/kjkiees.2015.26.11.985 ISSN 1226-3133 (Print)ISSN 2288-226X (Online) Analysis
More informationPowerPoint 프레젠테이션
Reasons for Poor Performance Programs 60% Design 20% System 2.5% Database 17.5% Source: ORACLE Performance Tuning 1 SMS TOOL DBA Monitoring TOOL Administration TOOL Performance Insight Backup SQL TUNING
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Jul.; 27(7),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2016 Jul.; 27(7), 625634. http://dx.doi.org/10.5515/kjkiees.2016.27.7.625 ISSN 1226-3133 (Print)ISSN 2288-226X (Online) Near-Field
More informationDBPIA-NURIMEDIA
The e-business Studies Volume 17, Number 6, December, 30, 2016:3~20 Received: 2016/12/04, Accepted: 2016/12/27 Revised: 2016/12/27, Published: 2016/12/30 [ABSTRACT] This study aims to comprehensively analyze
More information목차 BUG DEQUEUE 의 WAIT TIME 이 1 초미만인경우, 설정한시간만큼대기하지않는문제가있습니다... 3 BUG [qp-select-pvo] group by 표현식에있는컬럼을참조하는집합연산이존재하지않으면결괏값오류가발생할수있습니다... 4
ALTIBASE HDB 6.5.1.5.10 Patch Notes 목차 BUG-46183 DEQUEUE 의 WAIT TIME 이 1 초미만인경우, 설정한시간만큼대기하지않는문제가있습니다... 3 BUG-46249 [qp-select-pvo] group by 표현식에있는컬럼을참조하는집합연산이존재하지않으면결괏값오류가발생할수있습니다... 4 BUG-46266 [sm]
More information<4D F736F F F696E74202D203137C0E55FBFACBDC0B9AEC1A6BCD6B7E7BCC72E707074>
SIMATIC S7 Siemens AG 2004. All rights reserved. Date: 22.03.2006 File: PRO1_17E.1 차례... 2 심벌리스트... 3 Ch3 Ex2: 프로젝트생성...... 4 Ch3 Ex3: S7 프로그램삽입... 5 Ch3 Ex4: 표준라이브러리에서블록복사... 6 Ch4 Ex1: 실제구성을 PG 로업로드하고이름변경......
More informationTHE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE Mar.; 28(3),
THE JOURNAL OF KOREAN INSTITUTE OF ELECTROMAGNETIC ENGINEERING AND SCIENCE. 2017 Mar.; 28(3), 163 169. http://dx.doi.org/10.5515/kjkiees.2017.28.3.163 ISSN 1226-3133 (Print) ISSN 2288-226X (Online) PCB
More informationDBPIA-NURIMEDIA
e- 비즈니스연구 (The e-business Studies) Volume 17, Number 1, February, 28, 2016:pp. 3~30 ISSN 1229-9936 (Print), ISSN 2466-1716 (Online) 원고접수일심사 ( 수정 ) 게재확정일 2016. 01. 08 2016. 01. 09 2016. 02. 25 ABSTRACT
More information<313920C0CCB1E2BFF82E687770>
韓 國 電 磁 波 學 會 論 文 誌 第 19 卷 第 8 號 2008 年 8 月 論 文 2008-19-8-19 K 대역 브릭형 능동 송수신 모듈의 설계 및 제작 A Design and Fabrication of the Brick Transmit/Receive Module for K Band 이 기 원 문 주 영 윤 상 원 Ki-Won Lee Ju-Young Moon
More information슬라이드 제목 없음
2006-09-27 경북대학교컴퓨터공학과 1 제 5 장서브넷팅과슈퍼넷팅 서브넷팅 (subnetting) 슈퍼넷팅 (Supernetting) 2006-09-27 경북대학교컴퓨터공학과 2 서브넷팅과슈퍼넷팅 서브넷팅 (subnetting) 하나의네트워크를여러개의서브넷 (subnet) 으로분할 슈퍼넷팅 (supernetting) 여러개의서브넷주소를결합 The idea
More informationProblem New Case RETRIEVE Learned Case Retrieved Cases New Case RETAIN Tested/ Repaired Case Case-Base REVISE Solved Case REUSE Aamodt, A. and Plaza, E. (1994). Case-based reasoning; Foundational
More information강의10
Computer Programming gdb and awk 12 th Lecture 김현철컴퓨터공학부서울대학교 순서 C Compiler and Linker 보충 Static vs Shared Libraries ( 계속 ) gdb awk Q&A Shared vs Static Libraries ( 계속 ) Advantage of Using Libraries Reduced
More information00내지1번2번
www.keit.re.kr 2011. 11 Technology Level Evaluation ABSTRACT The Technology Level Evaluation assesses the current level of industrial technological development in Korea and identifies areas that are underdeveloped
More information커알못의 커널 탐방기 이 세상의 모든 커알못을 위해서
커알못의 커널 탐방기 2015.12 이 세상의 모든 커알못을 위해서 개정 이력 버전/릴리스 0.1 작성일자 2015년 11월 30일 개요 최초 작성 0.2 2015년 12월 1일 보고서 구성 순서 변경 0.3 2015년 12월 3일 오탈자 수정 및 글자 교정 1.0 2015년 12월 7일 내용 추가 1.1 2015년 12월 10일 POC 코드 삽입 및 코드
More information