FM 2015 : formal methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings

This book constitutes the refereed proceedings of the 20th International Symposium on Formal Methods, FM 2015, held in Oslo, Norway, in June 2015. The 30 full papers and 2 short papers presented were carefully reviewed and selected from 124 submissions. The papers cover a wide spectrum of all the different aspects of the use of and the research on formal methods for software development. Front Matter....Pages 1-14 Front Matter....Pages 1-1 Resource Analysis: From Sequential to Concurrent and Distributed Programs....Pages 3-17 AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned....Pages 18-19 Front Matter....Pages 21-21 Automated Circular Assume-Guarantee Reasoning....Pages 23-39 Narrowing Operators on Template Abstract Domains....Pages 40-56 Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification....Pages 57-72 Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures....Pages 73-89 A Specification Language for Static and Runtime Verification of Data and Control Properties....Pages 90-107 Certificates for Parameterized Model Checking....Pages 108-125 Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes....Pages 126-142 Verifying Opacity of a Transactional Mutex Lock....Pages 143-160 A Framework for Correctness Criteria on Weak Memory Models....Pages 161-177 Semantics-Preserving Simplification of Real-World Firewall Rule Sets....Pages 178-194 Parameter Synthesis Through Temporal Logic Specifications....Pages 195-212 Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL....Pages 213-230 Probabilistic Bisimulation for Realistic Schedulers....Pages 231-247 Automated Verification of RPC Stub Code....Pages 248-264 Property-Driven Fence Insertion Using Reorder Bounded Model Checking....Pages 265-272 Verifying the Safety of a Flight-Critical System....Pages 273-290 Front Matter....Pages 291-307 Proving Safety with Trace Automata and Bounded Model Checking....Pages 308-324 Verifying Parameterized Timed Security Protocols....Pages 21-21 Abstraction of Elementary Hybrid Systems by Variable Transformation....Pages 325-341 Using Real-Time Maude to Model Check Energy Consumption Behavior....Pages 342-359 Static Differential Program Analysis for Software-Defined Networks....Pages 360-377 A Fully Verified Container Library....Pages 378-394 Counterexamples for Expected Rewards....Pages 395-413 The Semantics of Cardinality-Based Feature Models via Formal Languages....Pages 414-434 Axiomatization of Typed First-Order Logic....Pages 435-452 Model-Based Problem Solving for University Timetable Validation and Improvement....Pages 453-469 Certified Reasoning with Infinity....Pages 470-486 Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems....Pages 487-495 Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions....Pages 496-513 Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking....Pages 514-531 Front Matter....Pages 532-550 Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking....Pages 551-569 Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems....Pages 571-571 Software Development and Authentication for Arms Control Information Barriers....Pages 573-576 Analyzing the Restart Behavior of Industrial Control Applications....Pages 577-580 Case Study: Static Security Analysis of the Android Goldfish Kernel....Pages 581-584 Practices for Formal Models as Documents: Evolution of VDM Application to “Mobile FeliCa” IC Chip Firmware....Pages 585-588 Front Matter....Pages 589-592 Formal Virtual Modelling and Data Verification for Supervision Systems....Pages 593-596 Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests....Pages 571-571 Formalizing the Concept Phase of Product Development....Pages 597-600 Back Matter....Pages 601-604 ....Pages 605-608