AIST Logo

National Institute of Advanced Industrial Science and Technology (AIST)
Information Technology Research Institute

Cyrille Artho

Senior Researcher, Information Technology Research Institute (ITRI), National Institute of Advanced Industrial Science and Technology (AIST).

Portrait

Contact:

New address (as of 2015-09-08):
National Institute of Advanced Industrial Science and Technology (AIST)
Information Technology Research Institute (ITRI)
AIST Ikeda
Midorigaoka 1-8-31
Ikeda
Osaka 563-8577 Japan

Phone: +81 (0)6 6494 7813
Fax: +81 (0)72 751 9949
E-mail: c (dot) artho (at) aist (dot) go (dot) jp

About me

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. I obtained my Ph.D. at ETH Zurich in 2005. In that work, I investigated different approaches for finding faults in multi-threaded programs. In particular, in joint work with NASA Ames I found that high-level data races can show potential problems in concurrent software even if individual data accesses are safe.

After obtaining my Ph.D., I moved to Tokyo, where I worked for two years at the National Institute of Informatics as a Postdoctoral Researcher. From April 2007 onwards, I worked at the National Institute of Advanced Industrial Science and Technology (AIST), where I currently work as Senior Researcher.

In recent work, I extended my work on concurrent software to networked programs. To analyze concurrency exhaustively, I lead the development of the Java PathFinder extension "net-iocache", so networked software can be used in that tool. Furthermore, I developed my own model-based test tool Modbat, which is specialized for generating tests for networked software.

My CV

Teaching

Tools

List of Publications (as of May 2016)

Click on the number for the bibtex entry. All full-text versions served from this page are preprints of the paper; for the official version, please consult the publisher.

If some more recent publications are not on this list, please check my DBLP page for a more up-to-date version.

[83] C. Artho, G. Rousset, Q. Gros. Precondition Coverage in Software Testing. 1st Int. Workshop on Validating Software Tests (VST 2016), March 2016, Osaka, Japan. PDF
[82] C. Artho, L. Ma. Classification of Randomly Generated Test Cases. 1st Int. Workshop on Validating Software Tests (VST 2016), March 2016, Osaka, Japan. PDF
[81] C. Artho, M. Seidl, Q. Gros, E. Choi, T. Kitamura, A. Mori, R. Ramler, Y. Yamagata. Model-based Testing of Stateful APIs with Modbat. Int. Conf. on Automated Software Engineering (ASE 2015), November 2015, Lincoln, USA. PDF
[80] L. Ma, C. Artho, C. Zhang, H. Sato, J. Gmeiner, R. Ramler. GRT: An Automated Test Generated using Orchestrated Program Analysis. Int. Conf. on Automated Software Engineering (ASE 2015), November 2015, Lincoln, USA. PDF
[79] L. Ma, C. Artho, C. Zhang, H. Sato, J. Gmeiner, R. Ramler. GRT: Program-Analysis-Guided Random Testing. Int. Conf. on Automated Software Engineering (ASE 2015), November 2015, Lincoln, USA. ACM SIGSOFT Distinguished Paper Award. PDF
[78] F. Weitl, N. Sebih, C. Artho, M. Hagiya, Y. Tanabe, Y. Yamagata, M. Yamamoto. Cardinality of UDP Transmission Outcomes. Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium (SETTA 2015), November 2015, Nanjing, China. PDF
[77] C. Artho, K. Havelund, R. Kumar, Y. Yamagata. Domain-Specific Languages with Scala. Int. Conf. on Formal Engineering Methods (ICFEM 2015), November 2015, Paris, France. PDF
[76] C. Artho, K. Suzaki, M. Hagiya, W. Leungwattanakit, R. Potter, E. Platon, Y. Tanabe, F. Weitl, M. Yamamoto. Using Checkpointing and Virtualization for Fault Injection. Int. Journal of Networking and Computing (IJNC), 5(2), pp. 347-372. IJNC, 2015. PDF
[75] N. Sebih, M. Hagiya, F. Weitl, M. Yamamoto, C. Artho, Y. Tanabe. Software Model Checking of UDP-based Distributed Applications. Int. Journal of Networking and Computing (IJNC), 5(2), pp. 373-402. IJNC, 2015. PDF
[74] T. Kitamura, A. Yamada, G. Hatayama, C. Artho, E. Choi, N. Do, Y. Oiwa, S. Sakuragi. Combinatorial Testing using Tree-based Test Models with Propositional Logic Constraints. IEEE Int. Conf. on Software Quality, Reliability and Security, (QRS 2015), August 2015, Vancouver, Canada. QRS 2015 best paper award PDF
[73] E. Choi, T. Kitamura, C. Artho, A. Yamada, Y. Oiwa. Priority Integration for Weighted Combinatorial Testing. 39th IEEE Annual Computer Software and Applications Conf. (COMPSAC 2015), July 2015, Taichung, Taiwan. PDF
[72] L. Ma, C. Artho, Z. Cheng, H. Sato, M. Hagiya, Y. Tanabe, M. Yamamoto. GRT at the SBST 2015 Tool Competition. 8th Int. Workshop on Search-Based Software Testing (SBST), May 2015, Florence, Italy. Best tool (competition winner) PDF
[71] A. Yamada, T. Kitamura, C. Artho, E. Choi, Y. Oiwa, A. Biere. Optimization of Combinatorial Testing by Incremental SAT Solving. 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015), April 2015, Graz, Austria. PDF
[70] N. Sebih, F. Weitl, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto. Software Model Checking of UDP-based Distributed Applications. 2nd Int. Symposium on Computing and Networking (CANDAR 2014), December 2014, Shizuoka, Japan. PDF
[69] C. Artho, M. Hagiya, W. Leungwattakit, E. Platon, R. Potter, K. Suzaki, Y. Tanabe, F. Weitl, M. Yamamoto. Using Checkpointing and Virtualization for Fault Injection. 2nd Int. Symposium on Computing and Networking (CANDAR 2014), December 2014, Shizuoka, Japan. PDF
[68] L. Ma, C. Artho, C. Zhang, H. Sato. Efficient testing of software product lines via centralization (short paper) Generative Programming: Concepts and Experiences (GPCE 2014), September 2014, Vasteras, Sweden. PDF
[67] E. Choi, T. Kitamura, C. Artho, Y. Oiwa. Design of Prioritized N-Wise Testing. Int. Conf. on Testing Software and Systems (ICTSS 2014), September 2014, Madrid, Spain. PDF
[66] L. Ma, C. Artho, H. Sato. Project Centralization Based on Graph Coloring. ACM 29th Int. Symposium on Applied Computing (SAC 2014), March 2014, Gyeongju, South Korea. PDF
[65] W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto, K. Takahashi. Modular Software Model Checking for Distributed Systems. IEEE Trans. on Softw. Eng., 40(5), IEEE, May 2014. PDF
[64] L. Ma, C. Artho, H. Sato. Managing Product Variants by Project Centralization. Lecture Notes on Software Engineering, 2(2), IACSIT press, January 2014. PDF
[63] L. Ma, C. Artho, H. Sato. Improving Automatic Centralization by Version Separation. IPSJ Transactions on Programming, 6(4), IPSJ, December 2013. PDF
[62] C. Artho, M. Hagiya, R. Potter, Y. Tanabe, F. Weitl, M. Yamamoto. Software Model Checking for Distributed Systems with Selector-Based, Non-Blocking Communication. 28th Int. Conf. on Automated Software Engineering (ASE 2013), November 2013, Palo Alto, USA. PDF
[61] R. Potter, C. Artho, K. Suzaki, M. Hagiya. A Knoppix-based Demonstration Environment for JPF. SIGSOFT Softw. Eng. Notes, 39(1), JPF Workshop 2013, November 2013, Palo Alto, USA. PDF
[60] C. Artho, K. Hayamizu, R. Ramler, Y. Yamagata. With an Open Mind: How to Write Good Models. 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2013), October 2013, Queenstown, New Zealand. PDF
[59] C. Artho, A. Biere, M. Hagiya, M. Seidl, E. Platon, Y. Tanabe, M. Yamamoto. Modbat: A Model-based API Tester for Event-driven Systems. 9th Haifa Verification Conference (HVC 2013), November 2013, Haifa, Israel. PDF
[58] J. Mund, R. Huuck, A. Fehnker, C. Artho. The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis. 11th Int. Symposium on Automated Technology for Verification and Analysis (ATVA 2013), October 2013, Hanoi, Vietnam. PDF
[57] L. Ma, C. Artho, H. Sato. Analyzing Multi-process Java Program by Automatic Centralization. 2nd IEEE Int. Workshop on Tools in Process (TiP), July 2013, Kyoto, Japan. PDF
[56] A. Biere, M. Seidl, C. Artho. Model-based Testing for Verification Backends. Tests and Proofs (TAP) 2013, June 2013, Budapest, Hungary. PDF
[55] K. Suzaki, K. Iijima, T. Yagi, C. Artho. Implementation of a Memory Disclosure Attack on Memory Deduplication of Virtual Machines. IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences, E96-A(1), IEICE, January 2013. PDF
[54] C. Artho, A. Biere, M. Hagiya, R. Potter, R. Ramler, Y. Tanabe, F. Weitl, M. Yamamoto. Modbat: A model-based API tester for event-driven systems. Short paper (tool demo) at the Dependable Systems Workshop 2012, December 2012, Kobe, Japan. PDF
[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 | 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
[51] I. Andjelkovic, C. Artho. Trace Server: A Tool for Storing, Querying and Analyzing Execution Traces. JPF Workshop 2011, November 2011, Lawrence, USA. PDF | 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
[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
[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
[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
[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. PDF
[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 | Postscript (gzipped)
[44] C. Artho. Run-time Verification of Networked Software. RV 2010, November 2010, St. Juliens, Malta. PDF | 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. PDF
[41] C. Artho. Iterative Delta Debugging. Int. Journal on Software Tools for Technology Transfer (STTT), 13(3). Springer, 2011 (electronic version: 2010). PDF
[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. 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), 2003. Extended Version of the VVEIS '03 paper. 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. Most influential ASWEC paper award (awarded in 2013). 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

AIST Logo