Abstract is missing.
- Fostering Proof Scores in CafeOBJKokichi Futatsugi. 1-20 [doi]
- Exploiting Partial Success in Applying Automated Formal MethodsMatthew B. Dwyer. 21 [doi]
- Multicore Embedded Systems: The Timing Problem and Possible SolutionsWang Yi. 22-23 [doi]
- Applying PVS Background Theories and Proof Strategies in Invariant Based ProgrammingJohannes Eriksson, Ralph-Johan Back. 24-39 [doi]
- Proof Obligation Generation and Discharging for Recursive Definitions in VDMAugusto Ribeiro, Peter Gorm Larsen. 40-55 [doi]
- Correct-by-Construction Model Transformations from Partially Ordered Specifications in CoqIman Poernomo, Jeffrey Terrell. 56-73 [doi]
- Decision Procedures for the Temporal Verification of Concurrent ListsAlejandro Sánchez, César Sánchez. 74-89 [doi]
- An Improved Decision Procedure for Propositional Projection Temporal LogicZhenhua Duan, Cong Tian. 90-105 [doi]
- A Semantic Model for Service Composition with Coordination Time DelaysNatallia Kokash, Behnaz Changizi, Farhad Arbab. 106-121 [doi]
- Compensable WorkFlow NetsFazle Rabbi, Hao Wang, Wendy MacCaull. 122-137 [doi]
- Automatically Testing Web Services Choreography with AssertionsLei Zhou, Jing Ping, Hao Xiao, Zheng Wang, Geguang Pu, Zuohua Ding. 138-154 [doi]
- Applying Ordinary Differential Equations to the Performance Analysis of Service CompositionZuohua Ding, Hui Shen, Jing Liu. 155-170 [doi]
- Verifying Heap-Manipulating Programs with Unknown Procedure CallsShengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin. 171-187 [doi]
- API Conformance Verification for Java ProgramsXin Li, H. James Hoover, Piotr Rudnicki. 188-203 [doi]
- Assume-Guarantee Reasoning with Local SpecificationsAlessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu 0002. 204-219 [doi]
- Automating Coinduction with Case AnalysisEugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu. 220-236 [doi]
- Enhanced Semantic Access to Formal Software ModelsHai H. Wang, Danica Damljanovic, Jing Sun. 237-252 [doi]
- Making Pattern- and Model-Based Software Development More RigorousDenis Hatebur, Maritta Heisel. 253-269 [doi]
- Practical Parameterised Session TypesAndi Bejleri. 270-286 [doi]
- A Formal Verification Study on the Rotterdam Storm Surge BarrierKen Madlener, Sjaak Smetsers, Marko C. J. D. van Eekelen. 287-302 [doi]
- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time SystemsJosé Meseguer, Peter Csaba Ölveczky. 303-320 [doi]
- Automated Multiparameterised Verification by Cut-OffsAntti Siirtola. 321-337 [doi]
- Automating Cut-off for Multi-parameterized SystemsYoussef Hanna, David Samuelson, Samik Basu, Hridesh Rajan. 338-354 [doi]
- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined MicroprocessorsMiroslav N. Velev, Ping Gao 0002. 355-370 [doi]
- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSPIslam Abdelhalim, James Sharp, Steve A. Schneider, Helen Treharne. 371-387 [doi]
- Model Checking Hierarchical Probabilistic SystemsJun Sun 0001, Songzheng Song, Yang Liu 0003. 388-403 [doi]
- Trace-Driven Verification of Multithreaded ProgramsZijiang Yang, Karem Sakallah. 404-419 [doi]
- Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join NetworkJonathan Billington, Guy Edward Gallasch. 420-435 [doi]
- Reasoning about Safety and Progress Using ContractsImene Ben Hafaiedh, Susanne Graf, Sophie Quinton. 436-451 [doi]
- Abstract Program Slicing: From Theory towards an ImplementationIsabella Mastroeni, Durica Nikolic. 452-467 [doi]
- Loop Invariant Synthesis in a Combined DomainShengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin. 468-484 [doi]
- Software Metrics in Static Program AnalysisAndreas Vogelsang, Ansgar Fehnker, Ralf Huuck, Wolfgang Reif. 485-500 [doi]
- A Combination of Forward and Backward Reachability Analysis MethodsKazuhiro Ogata, Kokichi Futatsugi. 501-517 [doi]
- Model Checking a Model Checker: A Code Contract Combined ApproachJun Sun 0001, Yang Liu 0003, Bin Cheng. 518-533 [doi]
- On Symmetries and Spotlights - Verifying Parameterised SystemsNils Timm, Heike Wehrheim. 534-548 [doi]
- A Methodology for Automatic Diagnosability AnalysisJonathan Ezekiel, Alessio Lomuscio. 549-564 [doi]
- Making the Right Cut in Model Checking Data-Intensive Timed SystemsRüdiger Ehlers, Michael Gerke 0002, Hans-Jörg Peter. 565-580 [doi]
- Comparison of Model Checking Tools for Information SystemsMarc Frappier, Benoît Fraikin, Romain Chossart, Raphaël Chane-Yack-Fa, Mohammed Ouenzar. 581-596 [doi]
- A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming ModelScott West, Sebastian Nanz, Bertrand Meyer. 597-612 [doi]
- Model-Driven Protocol Design Based on Component Oriented ModelingPrabhu Shankar Kaliappan, Hartmut König, Sebastian Schmerl. 613-629 [doi]
- Laws of Pattern CompositionHong Zhu, Ian Bayley. 630-645 [doi]
- Dynamic Resource Reallocation between Deployment ComponentsEinar Broch Johnsen, Olaf Owe, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa. 646-661 [doi]
- A Pattern System to Support Refining Informal Ideas into Formal ExpressionsXi Wang, Shaoying Liu, Huaikou Miao. 662-677 [doi]
- Specification Translation of State Machines from Equational Theories into Rewrite TheoriesMin Zhang, Kazuhiro Ogata, Masaki Nakamura. 678-693 [doi]
- Alternating Interval Based Temporal LogicsCong Tian, Zhenhua Duan. 694-709 [doi]