FM 2014: Formal Methods

Validity Checking of Put back Transformations in Bidirectional Programming.- Proof Engineering Considered Essential.- Engineering UToPiA: Formal Semantics for CML.- 40 Years of Formal Methods: Some Obstacles and Some Possibilities?.- A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes.- Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.- Definition, Semantics and Analysis of Multi rate Synchronous AADL.- Trust Found: Towards a Formal Foundation for Model Checking Trusted Computing Platforms.- The VerCors Tool for Verification of Concurrent Programs.- Knowledge-Based Automated Repair of Authentication Protocols.- A Simplified Z Semantics for Presentation Interaction Models.- Log Analysis for Data Protection Accountability.- Automatic Compositional Synthesis of Distributed Systems.- Automated Real Proving in PVS via MetiTarski.- Quiescent Consistency: Defining and Verifying Relaxed Linearizability.- Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol.- Contracts in Practice.- When Equivalence and Bisimulation Join Forces in Probabilistic Automata.- Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs.- Proof Patterns for Formal Methods.- Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System.- IscasMc: A Web-Based Probabilistic Model Checker.- Invariants, Well-Founded Statements and Real-Time Program Algebra.- Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis.- A Symbolic Algorithm for the Analysis of Robust Timed Automata.- Revisiting Compatibility of Input-Output Modal Transition Systems.- Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier.- Management of Time Requirements in Component-Based Systems.- Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning.- Formal Verification of Operational