| 2009 | Specifying and Verifying PLC Systems with TLA+. | Hehua Zhang, Stephan Merz, Ming Gu |
| 2009 | Exploring Topological Structure of Boolean Expressions for Test Data Selection. | Lian Yu, Wei Zhao, Xiangdong Fan, Jun Zhu |
| 2009 | An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems. | Yan Xiao, Zhenhua Duan, Pengcheng Nie |
| 2009 | Improve Semantic Web Services Discovery through Similarity Search in Metric Space. | Minghui Wu, Fanwei Zhu, Jia Lv, Tao Jiang, Jing Ying |
| 2009 | Test Data Generation for Derived Types in C Program. | Zheng Wang, Xiao Yu, Tao Sun, Geguang Pu, Zuohua Ding, Jueliang Hu |
| 2009 | DUMS: A Dynamical Updatable Monitoring System for Desktop PCs Used for Distributed Computing. | Jinwei Wang, Huazhi Sun, Jianping Fan |
| 2009 | A Tool for Estimating Memory Usage. | Shengyi Wang, Zongyan Qiu |
| 2009 | Modeling MapReduce with CSP. | Wen Su, Fan Yang, Huibiao Zhu, Qin Li |
| 2009 | Integrating Specification and Programs for System Modeling and Verification. | Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen |
| 2009 | Interpreting a Successful Testing Process: Risk and Actual Coverage. | Marille Stoelinga, Mark Timmer |
| 2009 | Modeling Web Applications and Generating Tests: A Combination and Interactions-guided Approach. | Bo Song, Huaikou Miao |
| 2009 | Modular Development of Certified System Software. | Zhong Shao |
| 2009 | Semantics of Metamodels in UML. | Lijun Shan, Hong Zhu |
| 2009 | Refinement Algebra with Explicit Probabilism. | T. M. Rabehaja, Jeff W. Sanders |
| 2009 | Environment Abstraction with State Clustering and Parameter Truncating. | Hong Pan, Yi Lv, Huimin Lin |
| 2009 | Data Structure Shape Inference and Verification for OO Programs. | Rhys Owen, Hugh Anderson |
| 2009 | Formal Specification and Experiments of an Expressive Human-Computer Ensemble System with Rehearsal. | Tetsuya Mizutani, Tatsuo Suzuki, Masayuki Shio, Yasuwo Ikeda |
| 2009 | Formal Representation and Analysis of a Near Miss Accident in N Sigma-labeled Calculus. | Tetsuya Mizutani, Shigeru Igarashi, Yasuwo Ikeda, Masayuki Shio |
| 2009 | Parameterized Bisimulation Infinite Evolution Mechanism. | Yanfang Ma, Min Zhang, Yixiang Chen |
| 2009 | Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation. | Moritz Martens, Mila E. Majster-Cederbaum |
| 2009 | Automated Test Case Generation Based on Coverage Analysis. | Tim A. Majchrzak, Herbert Kuchen |
| 2009 | Modeling Fault Tolerant Services in Service-Oriented Architecture. | Farzaneh Mahdian, Vahid Rafe, Reza Rafeh, Adel Torkaman Rahmani |
| 2009 | Environmental Simulation of Real-Time Systems with Nested Interrupts. | Guoqiang Li, Shoji Yuen, Masakazu Adachi |
| 2009 | Verification of Population Ring Protocols in PAT. | Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao |
| 2009 | MARS: Metamodel Recovery from Multi-tiered Models Using Grammar Inference. | Qichao Liu, Faizan Javed, Marjan Mernik, Barrett R. Bryant, Jeff Gray, Alan P. Sprague, Dejan Hrncic |