Art

J-GLOBAL ID：200902200572897541   Reference number：08A0087197

DbC in Model-Checking of C Programs

Cプログラム・モデル検査におけるDbC

Author (5)： NAKAJIMA SHIN (国立情報学研) ,  NAKAJIMA SHIN (総合研究大学院大) ,  IKEDA KENJIRO (NEC) ,  HASHIMOTO YUSUKE (NEC) ,  IWASAKI SHIN'ICHI (NEC)
Material： 情報処理学会研究報告  (IPSJ SIG Technical Reports)
Volume： 2007  Issue： 121(EMB-6)  Page： 33-38  Publication year： Dec. 04, 2007 
JST Material Number： Z0031B  ISSN： 0919-6072  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *model checking ,  C language ,  *computer program ,  support program ,  scalability ,  computer programming ,  program analysis ,  data type ,  accuracy ,  automatic inspection
Semi thesaurus term： *Cプログラム ,  software tool

JST classification (2)： Theory of computation  (JB02000A) ,  Computer system development  (JD02010R)

Reference (14)：

• CHEON, Y. Model variables : cleanly supporting abstraction in design by contract. Softw. Pract. Exper. 2005, 583-599
• CLARKE, E. Model Checking. 1999
• CLARKE, E. A Tool for Checking ANSI-C Programs. Proc. TACAS'04. 2004, 168-176
• FAHNDRICH, M. A Re-Entrancy Analysis for Object Orietend Programs. 9th FTfJP at ECOOP 2007. 2007
• FILLIATRE, J.-C. Multi-prover Verification of C Programs. Proc. ICFEM'04. 2004, 15-29

Terms in the title (1)： モデル検査