Abstract is missing.
- An Implementation Framework for Optimizing Test Case Generation Using Model CheckingLonghui Chang, Huaikou Miao, Gongzheng Lu. 3-16 [doi]
- Applying GA with Tabu list for Automatically Generating Test Cases Based on Formal SpecificationYuqin Zhou, Taku Sugihara, Yuji Sato. 17-31 [doi]
- Development of a Software Tool to Support Traceability-Based Inspection of SOFL SpecificationsJinghua Zhang, Shaoying Liu. 32-46 [doi]
- Unified Bounded Model Checking for MSVLBin Yu, Zhenhua Duan, Cong Tian. 49-61 [doi]
- An Over-Approximation Forward Analysis for Nested Timed AutomataYunqing Wen, Guoqiang Li 0001, Shoji Yuen. 62-80 [doi]
- Adopting Variable Dependency in Animation for Presenting the Behaviour of ProcessMo Li, Shaoying Liu. 81-93 [doi]
- Using Alloy in Introductory Courses of Formal MethodsShin Nakajima. 97-110 [doi]
- Automatic Verification for Later-Correspondence of Security ProtocolsXiaofei Xie, Xiaohong Li, Yang Liu, Li Li, Ruitao Feng, Zhiyong Feng. 111-126 [doi]
- Combining Separation Logic and Projection Temporal Logic to Reason About Non-blocking ConcurrencyXiaoxiao Yang. 127-144 [doi]
- Formal Semantics of Orc Based on TLA+Zhen You, Jinyun Xue, Qimin Hu, Yi Hong. 147-163 [doi]
- Incremental Points-to Analysis for Java via Edit PropagationYuting Chen, Qiuwei Shi, Weikai Miao. 164-178 [doi]
- A Memory Management Mechanism for MSVLKai Yang, Zhenhua Duan, Cong Tian. 179-188 [doi]