| 2009 | Verifying Semistructured Data Normalization Using SWRL. | Yuan-Fang Li, Jing Sun, Gillian Dobbie, Scott Uk-Jin Lee, Hai H. Wang |
| 2009 | Spontaneous Detection of Infinite Loops and Livelocks in Dynamic Testing of Concurrent Programs. | Che-Sheng Lin, Gwan-Hwan Hwang |
| 2009 | Algorithms for Computing Weak Bisimulation Equivalence. | Weisong Li |
| 2009 | Verification and Performance Analysis for Embedded Systems. | Kim Guldstrand Larsen |
| 2009 | Semantics for Communicating Actors with Interdependent Real-Time Deadlines. | Istvan Knoll, Anders P. Ravn, Arne Skou |
| 2009 | Verifying the Implementation of an Operating System Scheduler. | Moritz Kleine, Bjrn Bartels, Thomas Gthel, Sabine Glesner |
| 2009 | G-BLAST: BLAST Manager in an Heterogeneous Distributed Environment. | Dong-Wook Kim, Tae-Sung Jung, Dae-Won Kim, Seong-Hyeuk Nam, Hyuk-Ryul Kwon, Sang-Haeng Choi, Hyung-Dae Koh, Han-Suk Choi, Hong-Seog Park |
| 2009 | Domain Hierarchies: A Basic Theoretical Framework for Integrating Software Domains. | Pierre Kelsen, Qin Ma |
| 2009 | On Testing 1-Safe Petri Nets. | Guy-Vincent Jourdan, Gregor von Bochmann |
| 2009 | The Logical Approach to Low-Level Stack Reasoning. | Xinyu Jiang, Yu Guo, Yiyun Chen |
| 2009 | Representing Aspects in Design. | Saqib Iqbal, Gary Allen |
| 2009 | A Framework and Language Support for Automatic Dynamic Testing of Workflow Management Systems. | Gwan-Hwan Hwang, Che-Sheng Lin, Li-Te Tsao, Kuei-Huan Chen, Yan-You Li |
| 2009 | Measuring the Survivability of Object-Oriented Software. | Jueliang Hu, Zuohua Ding, Jing Liu, Ling Yin |
| 2009 | Heap Memory Requirements Analysis via Separation Logic. | Guanhua He, Chenguang Luo |
| 2009 | Consistency Checking for LSC Specifications. | Hai-Feng Guo, Wen Zheng, Mahadevan Subramaniam |
| 2009 | Automated Verification Using Unified Control Flows. | Cristian Gherghina, Cristina David |
| 2009 | Formal Reasoning about Concurrent Assembly Code with Reentrant Locks. | Ming Fu, Yu Zhang, Yong Li |
| 2009 | Program Repair as Sound Optimization of Broken Programs. | Bernd Fischer, Ando Saabas, Tarmo Uustalu |
| 2009 | Probabilistic Coordination Language for Component Dynamic Composition. | Dehui Du, Ling Yin |
| 2009 | Towards Expressive Specification and Efficient Model Checking. | Jin Song Dong, Jun Sun |
| 2009 | Formal Approaches to Deadlock Analysis in Competitions of Shared Web Resources. | Jieqi Ding, Han Zhu, Huibiao Zhu, Qin Li |
| 2009 | Verifying Self-stabilizing Population Protocols with Coq. | Yuxin Deng, Jean-Franois Monin |
| 2009 | Bounded Model Checking of ACTL Formulae. | Wei Chen, Wenhui Zhang |
| 2009 | Constructing Program Invariants via Solving QBF. | Shikun Chen, Zhoujun Li, Mengjun Li |
| 2009 | State Visibility and Communication in Unifying Theories of Programming. | Andrew Butterfield, Pawel Gancarski, Jim Woodcock |