LEADER 06952nam 22007455 450 001 9910483145503321 005 20200702172634.0 010 $a3-319-06410-X 024 7 $a10.1007/978-3-319-06410-9 035 $a(CKB)3710000000106758 035 $a(DE-He213)978-3-319-06410-9 035 $a(SSID)ssj0001204900 035 $a(PQKBManifestationID)11686566 035 $a(PQKBTitleCode)TC0001204900 035 $a(PQKBWorkID)11198532 035 $a(PQKB)11391885 035 $a(MiAaPQ)EBC3093382 035 $a(PPN)178320463 035 $a(EXLCZ)993710000000106758 100 $a20140418d2014 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFM 2014: Formal Methods $e19th International Symposium, Singapore, May 12-16, 2014. Proceedings /$fedited by Cliff Jones, Pekka Pihlajasaari, Jun Sun 205 $a1st ed. 2014. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2014. 215 $a1 online resource (XVIII, 750 p. 185 illus.) 225 1 $aProgramming and Software Engineering ;$v8442 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-319-06409-6 327 $aValidity 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. 330 $aThis 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. 410 0$aProgramming and Software Engineering ;$v8442 606 $aSoftware engineering 606 $aMathematical logic 606 $aComputer logic 606 $aManagement information systems 606 $aComputer science 606 $aComputers 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aManagement of Computing and Information Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I24067 606 $aComputation by Abstract Devices$3https://scigraph.springernature.com/ontologies/product-market-codes/I16013 615 0$aSoftware engineering. 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aManagement information systems. 615 0$aComputer science. 615 0$aComputers. 615 14$aSoftware Engineering. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aManagement of Computing and Information Systems. 615 24$aComputation by Abstract Devices. 676 $a005.1 702 $aJones$b Cliff$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPihlajasaari$b Pekka$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSun$b Jun$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a9910483145503321 996 $aFM 2014: Formal Methods$92830168 997 $aUNINA