National Institute of Advanced Industrial Science and Technology (AIST)
Research Institute for Secure Systems (RISEC)
|
|
National Institute of Advanced Industrial Science and Technology (AIST)
|
Senior Researcher, Research Institute for Secure Systems (RISEC), National Institute of Advanced Industrial Science and Technology (AIST).
 |
Contact:National Institute of Advanced Industrial Science and Technology (AIST)Research Institute for Secure Systems (RISEC) AIST Amagasaki Nakoji 3-11-46 Amagasaki Hyogo 661-0974 Japan Phone: +81 (0)6 6494 7813 Fax: +81 (0)6 6494 8073 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 my 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.
| [53] | C. Artho, K. Suzaki, R. di Cosmo, R. Treinen, S. Zacchiroli. Why Do Software Packages Conflict? 9th Working Conference on Mining Software Repositories, June 2012, Zurich, Switzerland. | PDF (preprint) | Postscript (gzipped) |
| [52] | K. Suzaki, K. Iijima, T. Yagi, C. Artho. Effects of Memory Randomization, Sanitization and Page Cache on Memory Deduplication. 5th European Workshop on System Security (EuroSec2012), April 2012, Bern, Switzerland. | PDF (preprint) |
| [51] | I. Andjelkovic, C. Artho. Trace Server: A Tool for Storing, Querying and Analyzing Execution Traces. JPF Workshop 2011, November 2011, Lawrence, USA. | PDF (preprint) | Postscript (gzipped) |
| [50] | W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto. Model Checking Distributed Systems by Combining Caching and Process Checkpointing. ASE 2011, November 2011, Lawrence, USA. | PDF (preprint) |
| [49] | K. Suzaki, K. Iijima, T. Yagi, C. Artho. Software Side Channel Attack on Memory Deduplication. Poster session of ACM Symposium on Operating Systems Principles (SOSP) 2011, October 2011, Cascals, Portugal. | PDF (preprint) |
| [48] | C. Artho, K. Suzaki, R. di Cosmo, S. Zacchiroli. Sources of Inter-package Conflicts in Debian. Workshop on Logics for Component Configuration (LoCoCo 2011), short presentation, September 2011, Perugia, Italy. | PDF (preprint) |
| [47] | K. Suzaki, K. Iijima, T. Yagi, C. Artho. Memory Deduplication as a Threat to the Guest OS. European Workshop on System Security (EuroSec 2011), April 2011, Salzburg, Austria. | PDF (preprint) |
| [46] | K. Suzaki, K. Iijima, T. Yagi, C. Artho, Y. Watanabe. Effect of Disk Prefetching of Guest OS on Storage Deduplication. Workshop on Runtime Environments/Systems, Layering, and Virtualized Environments (RESoLVE 2011), March 2011, Newport Beach, USA. | |
| [45] | C. Artho, W. Leungwattanakit, M. Hagiya, E. Platon, Y. Tanabe, M. Yamamoto. Cache-based Model Checking of Networked Software. DNSA 2010, December 2010, Hiroshima, Japan. | PDF (preprint) | Postscript (gzipped) |
| [44] | C. Artho. Run-time Verification of Networked Software. RV 2010, November 2010, St. Juliens, Malta. | PDF (preprint) | Postscript (gzipped) |
| [43] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, M. Yamamoto. Model Checking of Concurrent Algorithms: From Java to C. DIPES 2010, September 2010, Brisbane, Australia. | PDF | Postscript (gzipped) |
| [42] | K. Suzaki, T. Yagi, K. Iijima, A. Nguyen, C. Artho, Y. Watanabe. Moving from logical sharing of guest OS to physical sharing of deduplication on virtual machine. HotSec 2010, July 2010, Washington D.C., USA. | |
| [41] | C. Artho. Iterative Delta Debugging. Int. Journal on Software Tools for Technology Transfer (STTT), 13(3). Springer, 2011 (electronic version: 2010). | PDF (preprint) |
| [40] | C. Artho. Separation of Transitions, Actions, and Exceptions in Model-based Testing. Eurocast 2009 post-proceedings, LNCS 5717. | PDF | Postscript (gzipped) |
| [39] | C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, M. Yamamoto. Cache-Based Model Checking of Networked Applications: From Linear to Branching Time. ASE 2009, November 2009, Auckland, New Zealand. | PDF | Postscript (gzipped) |
| [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. | DOI (linking to 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. | PDF | Postscript (gzipped) |
| [11] | C. Artho, A. Biere. Combined Static and Dynamic Analysis. ETH Technical Report #466. Extended version of AIOOL paper. | PDF | Postscript (gzipped) |
| [10] | C. Artho, A. Biere. Combined Static and Dynamic Analysis. AIOOL '05, Paris, France, January 2005. | 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. | 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. | PDF | Postscript (gzipped) |
| [7] | C. Artho and K. Havelund: Applying Jlint to Space Exploration Software. VMCAI '04, Venice, Italy, January 2004. | 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 | 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. | 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. | 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. | 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 | PDF | Postscript (gzipped) |
|
E-mail: c (dot) artho (at) aist (dot) go (dot) jp |
|