FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings

Front Matter....Pages -
Validity Checking of Putback Transformations in Bidirectional Programming....Pages 1-15
Proof Engineering Considered Essential....Pages 16-21
Engineering UToPiA ....Pages 22-41
40 Years of Formal Methods....Pages 42-61
A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes....Pages 62-77
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools....Pages 78-93
Definition, Semantics, and Analysis of Multirate Synchronous AADL....Pages 94-109
 TrustFound : Towards a Formal Foundation for Model Checking Trusted Computing Platforms....Pages 110-126
The VerCors Tool for Verification of Concurrent Programs....Pages 127-131
Knowledge-Based Automated Repair of Authentication Protocols....Pages 132-147
A Simplified Z Semantics for Presentation Interaction Models....Pages 148-162
Log Analysis for Data Protection Accountability....Pages 163-178
Automatic Compositional Synthesis of Distributed Systems....Pages 179-193
Automated Real Proving in PVS via MetiTarski....Pages 194-199
Quiescent Consistency: Defining and Verifying Relaxed Linearizability....Pages 200-214
Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol....Pages 215-229
Contracts in Practice....Pages 230-246
When Equivalence and Bisimulation Join Forces in Probabilistic Automata....Pages 247-262
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs....Pages 263-278
Proof Patterns for Formal Methods....Pages 279-295
Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System....Pages 296-311
 iscas M c : A Web-Based Probabilistic Model Checker....Pages 312-317
Invariants, Well-Founded Statements and Real-Time Program Algebra....Pages 318-334
Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis....Pages 335-350
A Symbolic Algorithm for the Analysis of Robust Timed Automata....Pages 351-366
Revisiting Compatibility of Input-Output Modal Transition Systems....Pages 367-381
Co-induction Simply....Pages 382-398
Management of Time Requirements in Component-Based Systems....Pages 399-415
Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning....Pages 416-431
Formal Verification of Operational Transformation....Pages 432-448
Verification of a Transactional Memory Manager under Hardware Failures and Restarts....Pages 449-464
SCJ: Memory-Safety Checking without Annotations....Pages 465-480
Refactoring, Refinement, and Reasoning....Pages 481-496
Object Propositions....Pages 497-513
Flexible Invariants through Semantic Collaboration....Pages 514-530
Efficient Tight Field Bounds Computation Based on Shape Predicates....Pages 531-546
A Graph-Based Transformation Reduction to Reach UPPAAL States Faster....Pages 547-562
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison....Pages 563-578
Efficient Self-composition for Weakest Precondition Calculi....Pages 579-594
Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections....Pages 595-610
Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic....Pages 611-626
A Modular Theory of Object Orientation in Higher-Order UTP....Pages 627-642
Formalizing and Verifying a Modern Build Language....Pages 643-657
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification....Pages 658-672
Formally Verifying Graphics FPU....Pages 673-687
MDP-Based Reliability Analysis of an Ambient Assisted Living System....Pages 688-702
Diagnosing Industrial Business Processes: Early Experiences....Pages 703-717
Formal Verification of Lunar Rover Control Software Using UPPAAL....Pages 718-732
Formal Verification of a Descent Guidance Control Program of a Lunar Lander....Pages 733-748
Back Matter....Pages -