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 Transformation.- Verification of a Transactional Memory Manager under Hardware Failures and Restarts.- SCJ: Memory-Safety Checking without Annotations.- Refactoring, Refinement and Reasoning: A Logical Characterization for Hybrid Systems.- Object Propositions.- Flexible Invariants through Semantic Collaboration.- Efficient Tight Field Bounds Computation Based on Shape Predicates.- A Graph-Based Transformation Reduction to Reach UPPAAL States Faster.- Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison.- Efficient Self-composition for Weakest Precondition Calculi.- Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections.- Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic.- A Modular Theory of Object Orientation in Higher-Order UTP.- Formalizing and Verifying a Modern Build Language.- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification.- Formally Verifying Graphics FPU: An Intel® Experience.- MDP-Based Reliability Analysis of an Ambient Assisted Living System.- Diagnosing Industrial Business Processes: Early Experiences.- Formal Verification of Lunar Rover Control Software Using UPPAAL.- Formal Verification of a Descent Guidance Control Program of a Lunar Lander.