Formal Methods and Software Engineering

Invited Talks.- Fostering Proof Scores in CafeOBJ.- Exploiting Partial Success in Applying Automated Formal Methods.- Multicore Embedded Systems: The Timing Problem and Possible Solutions.- Theorem Proving and Decision Procedures.- Applying PVS Background Theories and Proof Strategies in Invariant Based Programming.- Proof Obligation Generation and Discharging for Recursive Definitions in VDM.- Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq.- Decision Procedures for the Temporal Verification of Concurrent Lists.- An Improved Decision Procedure for Propositional Projection Temporal Logic.- Web Services and Workflow.- A Semantic Model for Service Composition with Coordination Time Delays.- Compensable WorkFlow Nets.- Automatically Testing Web Services Choreography with Assertions.- Applying Ordinary Differential Equations to the Performance Analysis of Service Composition.- Verification I.- Verifying Heap-Manipulating Programs with Unknown Procedure Calls.- API Conformance Verification for Java Programs.- Assume-Guarantee Reasoning with Local Specifications.- Automating Coinduction with Case Analysis.- Applications of Formal Methods.- Enhanced Semantic Access to Formal Software Models.- Making Pattern- and Model-Based Software Development More Rigorous.- Practical Parameterised Session Types.- A Formal Verification Study on the Rotterdam Storm Surge Barrier.- Verification II.- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems.- Automated Multiparameterised Verification by Cut-Offs.- Automating Cut-off for Multi-parameterized Systems.- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors.- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP.- Probability and Concurrency.- Model Checking Hierarchical Probabilistic Systems.- Trace-Driven Verification of Multithreaded Programs.- Closed Form Approximations for Steady State