| Keynote Talks |
| Program Verification Through Computer Algebra / Chaochen Zhou |
| JML's Rich, Inherited Specifications for Behavioral Subtypes / Gary T. Leavens |
| Three Perspectives in Formal Engineering / John McDermid ; Andy Galloway |
| Specification and Verification |
| A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces / Bernhard Beckert ; Gerd Beuster |
| Applying Timed Interval Calculus to Simulink Diagrams / Chunqing Chen ; Jin Song Dong |
| Reducing Model Checking of the Few to the One / E. Allen Emerson ; Richard J. Trefler ; Thomas Wahl |
| Induction-Guided Falsification / Kazuhiro Ogata ; Masahiro Nakano ; Weiqiang Kong ; Kokichi Futatsugi |
| Verifying [chi] Models of Industrial Systems with Spin / Nikola Trcka |
| Stateful Dynamic Partial-Order Reduction / Xiaodong Yi ; Ji Wang ; Xuejun Yang |
| Internetware and Web-Based Systems |
| User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition / Xiaoning Ding ; Jun Wei ; Tao Huang |
| Environment Ontology-Based Capability Specification for Web Service Discovery / Puwei Wang ; Zhi Jin ; Lin Liu |
| Scenario-Based Component Behavior Derivation / Yan Zhang ; Jun Hu ; Xiaofeng Yu ; Tian Zhang ; Xuandong Li ; Guoliang Zheng |
| Verification of Computation Orchestration Via Timed Automata / Yang Liu ; Jun Sun ; Xian Zhang |
| Towards the Semantics for Web Service Choreography Description Language / Jing Li ; Jifeng He ; Geguang Pu ; Huibiao Zhu |
| Type Checking Choreography Description Language / Hongli Yang ; Xiangpeng Zhao ; Zongyan Qiu ; Chao Cai |
| Concurrent, Communicating, Timing and Probabilistic Systems |
| Formalising Progress Properties of Non-blocking Programs / Brijesh Dongol |
| Towards a Fully Generic Theory of Data / Douglas A. Creager ; Andrew C. Simpson |
| Verifying Statemate Statecharts Using CSP and FDR / A. W. Roscoe ; Z. Wu |
| A Reasoning Method for Timed CSP Based on Constraint Solving / Ping Hao |
| Mapping RT-LOTOS Specifications into Time Petri Nets / Tarek Sadani ; Marc Boyer ; Pierre de Saqui-Sannes ; Jean-Pierre Courtiat |
| Reasoning Algebraically About Probabilistic Loops / Larissa Meinicke ; Ian J. Hayes |
| Object and Component Orientation |
| Formal Verification of the Heap Manager of an Operating System Using Separation Logic / Nicolas Marti ; Reynald Affeldt ; Akinori Yonezawa |
| A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs / Bart Jacobs ; Jan Smans ; Frank Piessens ; Wolfram Schulte |
| Model Checking Dynamic UML Consistency / Quan Long |
| Testing and Model Checking |
| Conditions for Avoiding Controllability Problems in Distributed Testing / Jessica Chen ; Lihua Duan |
| Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm / Samira Tasharofi ; Sepand Ansari ; Marjan Sirjani |
| Checking the Conformance of Java Classes Against Algebraic Specifications / Isabel Nunes ; Antonia Lopes ; Vasco Vasconcelos ; Joao Abreu ; Luis S. Reis |
| Incremental Slicing / Heike Wehrheim |
| Assume-Guarantee Software Verification Based on Game Semantics / Aleksandar Dimovski ; Ranko Lazic |
| Optimized Execution of Deterministic Blocks in Java PathFinder / Marcelo d'Amorim ; Ahmed Sobeih ; Darko Marinov |
| Tools |
| A Tool for a Formal Pattern Modeling Language / Soon-Kyeong Kim ; David Carrington |
| An Open Extensible Tool Environment for Event-B / Jean-Raymond Abrial ; Michael Butler ; Stefan Hallerstede ; Laurent Voisin |
| Tool for Translating Simulink Models into Input Language of a Model Checker / Meenakshi B. ; Abhishek Bhatnagar ; Sudeepa Roy |
| Fault-Tolerance and Security |
| Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices / Tim McComb ; Luke Wildman |
| A Language for Modeling Network Availability / Luigia Petre ; Kaisa Sere ; Marina Walden |
| Multi-process Systems Analysis Using Event B: Application to Group Communication Systems / J. Christian Attiogbe |
| Specification and Refinement |
| Issues in Implementing a Model Checker for Z / John Derrick ; Siobhan North ; Tony Simons |
| Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking / Leo Freitas ; Ana Cavalcanti ; Jim Woodcock |
| Discovering Likely Method Specifications / Nikolai Tillmann ; Feng Chen |
| Time Aware Modelling and Analysis of Multiclocked VLSI Systems / Tomi Westerlund ; Juha Plosila |
| SALT-Structured Assertion Language for Temporal Logic / Andreas Bauer ; Martin Leucker ; Jonathan Streit |
| Author Index |
| Keynote Talks |
| Program Verification Through Computer Algebra / Chaochen Zhou |
| JML's Rich, Inherited Specifications for Behavioral Subtypes / Gary T. Leavens |
図書