cam a22 5 4500 317151126 CHVBK 20201009192930.0 m d cr |n |||||||| 140625s2014 gw |||| s 0 0|eng d 978-3-319-06410-9 978-3-319-06409-3 (print) 10.1007/978-3-319-06410-9 doi (SERSOL)ssj0001204900 (IDSSG)000655519 (WaSeSS)ssj0001204900 WaSeSS QA76.758 UMZ bicssc COM051230 bisacsh 005.1 23 DEAGID8F3A6320ABCB163C1257FF1005C3B33 iCapture Jones Cliff editor FM 2014: Formal Methods [Elektronische Daten] 19th International Symposium, Singapore, May 12-16, 2014. Proceedings edited by Cliff Jones, Pekka Pihlajasaari, Jun Sun Cham Springer International Publishing Imprint: Springer 2014 1 online resource (XVIII, 750 p. 185 illus.) online resource text file PDF rda Lecture Notes in Computer Science 0302-9743 8442 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. Lizenzbedingungen können den Zugang einschränken. License restrictions may limit access. This book constitutes the refereed proceedings of the 19th International Symposium on Formal Methods, FM 2014, held in Singapore, May 2014. The 45 papers presented together with 3 invited talks were carefully reviewed and selected from 150 submissions. The focus of the papers is on the following topics: Interdisciplinary Formal Methods, Practical Applications of Formal Methods in Industrial and Research Settings, Experimental Validation of Tools and Methods as well as Construction and Evolution of Formal Methods Tools. Computer science Software engineering Logic design Information Systems Pihlajasaari Pekka editor Sun Jun editor SpringerLink (Online service) Printed edition 9783319064093 https://link.springer.com/10.1007/978-3-319-06410-9 Uni Basel: Volltext https://link.springer.com/openurl?genre=book&isbn=978-3-319-06409-3 Uni Bern: Volltext BK020053 XK020053 XK020000 Springer Computer Science eBooks 2014 English/International E-Books von 360MarcUpdates SpringerLINK Lecture Notes in Computer Science Contemporary (1997-2014) noalma ids I IDSSG HSG HSG ONL HONL000655519 IDSBB A145 A145 145VT IDSBB B405 B405 405VT IDSBB 100 1- Jones Cliff editor IDSBB 490 1- Lecture Notes in Computer Science 0302-9743 8442 IDSBB 700 1- Pihlajasaari Pekka editor IDSBB 700 1- Sun Jun editor IDSBB 710 2- SpringerLink (Online service) IDSBB 776 08 Printed edition 9783319064093 IDSBB 856 40 https://link.springer.com/10.1007/978-3-319-06410-9 Uni Basel: Volltext IDSBB 856 40 https://link.springer.com/openurl?genre=book&isbn=978-3-319-06409-3 Uni Bern: Volltext IDSSG 490 0- Lecture Notes in Computer Science 8442 IDSSG 700 1- Jones Cliff IDSSG 700 1- Pihlajasaari Pekka IDSSG 700 1- Sun Jun IDSSG 856 4- https://doi.org/10.1007/978-3-319-06410-9 Full text for the University of St. Gallen SWISSBIB 317151126