Formal Methods and Software Engineering

Toward Practical Application of Formal Methods in Software Lifecycle Processes.- Formal Methods in the Aerospace Industry: Follow the Money.- Applying Term Rewriting to Speech Recognition of Numbers.- Variable Permissions for Concurrency Verification.- A Concurrent Temporal Programming Model with Atomic Blocks.- A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs.- Towards a Formal Verification Methodology for Collective Robotic Systems.- Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS.- Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic.- Quantitative Program Dependence Graphs.- Quantitative Analysis of Information Flow Using Theorem Proving.- Modeling and Verification of Probabilistic Actor Systems Using pRebeca.- Modular Verification of OO Programs with Interfaces.- Separation Predicates: A Taste of Separation Logic in First-Order Logic.- The Confinement Problem in the Presence of Faults.- Verification of ATL Transformations Using Transformation Models and Model Finders.- Automatic Generation of Provably Correct Embedded Systems.- Complementary Methodologies for Developing Hybrid Systems with Event-B.- A Temporal Logic with Mean-Payoff Constraints.- Time Constraints with Temporal Logic Programming.- Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System.- Equational Abstraction Refinement for Certified Tree Regular Model Checking.- SMT-Based False Positive Elimination in Static Program Analysis.- Predicate Analysis with Block-Abstraction Memoization.- Heuristic-Guided Abstraction Refinement for Concurrent Systems.- More Anti-chain Based Refinement Checking.- An Analytical and Experimental Comparison of CSP Extensions and Tools.- Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization.- Annotations for Alloy: Automated Incremental Analysis Using Domain Specific Solvers.- State Space c-Reductions of Concurrent Systems in Rewriting Logic.- A Practical Loop Invariant Generation Approach Based on Random Testing, Constraint Solving and Verification.- ConSMutate: SQL Mutants for Guiding Concolic Testing of Database Applications.- Demonic Testing of Concurrent Programs.- Towards Certified Runtime Verification.