National Institute of Advanced Industrial Science and Technology (AIST)
Research Center for Information Security
|
|
National Institute of Advanced Industrial Science and Technology (AIST)
|
 |
Contact:National Institute of Advanced Industrial Science and Technology (AIST) Research Center for Information Security (RCIS) Akihabara Daibiru, Room 1003 Sotokanda 1 - 18 - 13, Chiyoda-ku Tokyo 101 - 0021 Japan Phone: +81 (0)3 5298 4722 Fax: +81 (0)3 5298 4522 E-mail: c (dot) artho (at) aist (dot) go (dot) jp |
My main interests are software verification and software engineering. In my master's thesis, I compared different approaches for finding faults in multi-threaded programs. In my Ph.D. thesis, I have continued my search for such errors, which our tool JNuke can detect efficiently. My most recent works focused on analyzing networked programs - see publications below.
After graduating at ETH Zurich, I decided to pursue research there and obtained m Ph.D. in May 2005. During research, I spent two summers at the Computational Sciences Division of the NASA Ames Research Center.
After obtaining my Ph.D., I moved to Tokyo, where I have worked for two years at the National Institute of Informatics as a Postdoctoral Researcher. From April 2007 onwards, I work at the National Institute of Advanced Industrial Science and Technology (AIST).
Click on the number for the bibtex entry.
| [38] | C. Artho, Y. Oiwa, K. Suzaki, M. Hagiya. Extraction of properties in C implementations of security APIs for verification of Java applications. Analysis of Security APIs, July 2009, Port Jefferson, USA. | PDF | Postscript (gzipped) |
| [37] | W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto. Verifying Networked Programs Using a Model Checker Extension. ICSE 2009 tool/demo paper, May 2009, Vancouver, Canada. | PDF | Postscript (gzipped) |
| [36] | W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto. Introduction of Virtualization Technology to Networked Model Checking. NASA Formal Methods Symposium, April 2009, Moffett Field, USA. | PDF | Postscript (gzipped) |
| [35] | C. Artho. Separation of Transitions, Actions, and Exceptions in Model-based Testing. Eurocast 2009, Las Palmas de Gran Canaria, Spain, February 2009. | PDF | Postscript (gzipped) |
| [34] | C. Artho. Iterative Delta Debugging. HVC 2008, Haifa, Israel, October 2008. | PDF | Postscript (gzipped) |
| [33] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe. Architecture-aware Partial Order Reduction to Accelerate Model Checking of Networked Programs. SNPD 2008, August 2008, Phuket, Thailand. | PDF | Postscript (gzipped) |
| [32] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe. Tools and Techniques for Model Checking Networked Programs. SNPD 2008, August 2008, Phuket, Thailand. | PDF | Postscript (gzipped) |
| [31] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe. Efficient Model Checking of Networked Applications. TOOLS 2008, July 2008, Zurich, Switzerland. Errata: The published version has a typo in Table 2 regarding the time of the alphabet client, case 3/3. | PDF | Postscript (gzipped) |
| [30] | C. Artho, K. Taguchi, Y. Tahara, S. Honiden, Y. Tanabe. Teaching Software Model Checking. FORMED 2008, March 2008, Budapest, Hungary. | PDF | Postscript (gzipped) |
| [29] | C. Artho, B. Zweimüller, A. Biere, E. Shibayama, S. Honiden. Efficient Model Checking of Applications with Input/Output. Eurocast 2007 post-proceedings, LNCS 4739. | PDF | Postscript (gzipped) |
| [28] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, E. Shibayama. Architecture-aware Partial-order Reduction to Accelerate Model Checking of Networked Programs. Third DIKU-IST workshop, Roskilde, Denmark. | PDF | Postscript (gzipped) |
| [27] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, E. Shibayama. Hiding Backtracking Operations in Software Model Checking from the Environment. Third DIKU-IST workshop, Roskilde, Denmark. | PDF | Postscript (gzipped) |
| [26] | C. Artho, A. Biere, S. Honiden. Exhaustive Testing of Exception Handlers with Enforcer. FMCO 2006 post-proceedings, LNCS 4709. | PDF | Postscript (gzipped) |
| [25] | C. Artho, K. Havelund, S. Honiden. Visualization of Concurrent Program Executions. NII technical report #NII-2007-006E. Extended version of SACT paper. | PDF | Postscript (gzipped) |
| [24] | C. Artho, K. Havelund, S. Honiden. Visualization of Concurrent Program Executions. SACT 2007, Beijing, China, July 2007. | PDF | Postscript (gzipped) |
| [23] | C. Artho, Z. Chen, S. Honiden. AOP-based automated unit test classification of large benchmarks. AoAsia 2007, Beijing, China, July 2007. | PDF | Postscript (gzipped) |
| [22] | C. Artho, E. Shibayama, S. Honiden. Iterative Delta Debugging. TESTCOM 2007, Tallinn, Estonia, June 2007 (Poster session). | PDF | Postscript (gzipped) |
| [21] | C. Artho, C. Sommer, S. Honiden. Model Checking Networked Programs in the Presence of Transmission Failures. TASE 2007, Shanghai, China, June 2007. | PDF | Postscript (gzipped) |
| [20] | C. Artho, B. Zweimüller, A. Biere, S. Honiden. Efficient Model Checking of Applications with I/O. Eurocast 2007, Las Palmas de Gran Canaria, Spain, February 2007. | PDF | Postscript (gzipped) |
| [19] | C. Artho, P. Garoche. Accurate Centralization for Applying Model Checking on Networked Applications. ASE 2006, Tokyo, Japan, September 2006. | PDF | Postscript (gzipped) |
| [18] | C. Artho, A. Biere, S. Honiden. Enforcer -- Efficient Failure Injection. FM 2006, Hamilton, Canada, August 2006. | PDF | Postscript (gzipped) |
| [17] | C. Artho, A. Biere, S. Honiden. Testing I/O Failures with Enforcer. FM 2006 (tool demonstration track), Hamilton, Canada, August 2006. | PDF | Postscript (gzipped) |
| [16] | C. Artho, A. Biere, S. Honiden, V. Schuppan, P. Eugster, M. Baur, B. Zweimüller, P. Farkas. Advanced Unit Testing -- How to Scale Up a Unit Test Framework. AST 2006, Shanghai, China, May 2006. | PDF | Postscript (gzipped) |
| [15] | C. Artho. A Novel Approach on Centralizing Networked Applications. Poster session of APLAS '05. November 2005. | PDF | Postscript (gzipped) |
| [14] | C. Artho. Combining Static and Dynamic Analysis to Find Multi-threading Faults Beyond Data Races. Diss. ETH Zurich No. 16020, Switzerland, May 2005. Published by Hartung-Gorre Verlag Konstanz, Germany, ISBN 3-89649-997-1, Series of Computer Science, ISSN 1611-0943. | ETH e-collection | Book |
| [13] | C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, R. Washington. Combining Test Case Generation and Runtime Verification. In: ASM issue of Theoretical Computer Science. | Preprint as PDF | Postscript (gzipped) |
| [12] | C. Artho, A. Biere. Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. BYTECODE '05, Edinburgh, Scotland, April 2005. | Full text as PDF | Postscript (gzipped) |
| [11] | C. Artho, A. Biere. Combined Static and Dynamic Analysis. ETH Technical Report #466. Extended version of AIOOL paper. | Full text as PDF | Postscript (gzipped) |
| [10] | C. Artho, A. Biere. Combined Static and Dynamic Analysis. AIOOL '05, Paris, France, January 2005. | Full text as PDF | Postscript (gzipped) |
| [9] | C. Artho, K. Havelund, A. Biere: Using Block-local Atomicity to Detect Stale-value Concurrency Errors. ATVA '04, Taipei, Taiwan, November 2004. | Full text as PDF | Postscript (gzipped) |
| [8] | C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. Zweimüller: JNuke: Efficient Dynamic Analysis for Java. CAV '04, Boston, USA, July 2004. | Full text as PDF | Postscript (gzipped) |
| [7] | C. Artho and K. Havelund: Applying Jlint to Space Exploration Software. VMCAI '04, Venice, Italy, January 2004. | Full text as PDF | Postscript (gzipped) |
| [6] | C. Artho, A. Biere, and K. Havelund: High-level Data Races. In: Journal on Software Testing, Verification and Reliability (STVR), 13(4). Extended Version of the VVEIS '03 paper. | Preprint as PDF | Postscript (gzipped) |
| [5] | C. Artho, A. Biere, and K. Havelund: High-level Data Races. The First International Workshop on Verification and Validation of Enterprise Information Systems (VVEIS'03), Angers, France, April 2003 | Full text as PDF | Postscript (gzipped) |
| [4] | C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu and W. Visser (invited paper, K. Havelund is invited speaker): Experiments with Test Case Generation and Runtime Analysis. 10th International Workshop on Abstract State Machines (ASM 2003), Taormina, Italy, March 2003. | Full text as PDF | Postscript (gzipped) |
| [3] | A. Biere, C. Artho, V. Schuppan: Liveness Checking as Safety Checking. Proceedings of the Seventh International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), Malaga, Spain, July 2002. | Full text as PDF | Postscript (gzipped) |
| [2] | C. Artho, A. Biere: Applying Static Analysis to Large-Scale, Multi-threaded Java Programs. In: D. Grant (Ed.), Proceedings of the 13th Australian Software Engineering Conference (ASWEC 2001), pp. 68 - 75, Canberra, Australia, August 2001. IEEE Computer Society, PR 01254. | Full text as PDF | Postscript |
| [1] | C. Artho: Finding faults in multi-threaded programs. Master's thesis. Institute of Computer Systems, Federal Institute of Technology, Zurich/Austin 2000/01 | Full text as PDF | Postscript (gzipped) |
|
E-mail: c (dot) artho (at) aist (dot) go (dot) jp |
|