MARC Record from harvard_bibliographic_metadata

LEADER: 05766nam a22005535a 4500
001 014020875-5
005 20140620185800.0
008 140418s2014 gw | s ||0| 0|eng d
020 $a9783319064109
020 $a9783319064109
020 $a9783319064093
024 7 $a10.1007/978-3-319-06410-9$2doi
035 $a(Springer)9783319064109
040 $aSpringer
050 4 $aQA76.758
072 7 $aUMZ$2bicssc
072 7 $aCOM051230$2bisacsh
082 04 $a005.1$223
100 1 $aJones, Cliff,$eeditor.
245 10 $aFM 2014: Formal Methods :$b19th International Symposium, Singapore, May 12-16, 2014. Proceedings /$cedited by Cliff Jones, Pekka Pihlajasaari, Jun Sun.
264 1 $aCham :$bSpringer International Publishing :$bImprint: Springer,$c2014.
300 $aXVIII, 750 p. 185 illus.$bonline resource.
336 $atext$btxt$2rdacontent
337 $acomputer$bc$2rdamedia
338 $aonline resource$bcr$2rdacarrier
347 $atext file$bPDF$2rda
490 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v8442
505 0 $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 --
505 0 $aTemporal 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 --
505 0 $aCompositional 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 --
505 0 $aA 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.
520 $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.
650 20 $aSoftware engineering.
650 10 $aComputer science.
650 0 $aComputer science.
650 0 $aSoftware engineering.
650 0 $aLogic design.
650 0 $aInformation Systems.
650 24 $aMathematical Logic and Formal Languages.
650 24 $aLogics and Meanings of Programs.
650 24 $aMathematical Logic and Formal Languages.
650 24 $aManagement of Computing and Information Systems.
650 24 $aComputation by Abstract Devices.
700 1 $aSun, Jun,$eeditor.
700 1 $aPihlajasaari, Pekka,$eeditor.
776 08 $iPrinted edition:$z9783319064093
830 0 $aLecture Notes in Computer Science ;$v8442.
988 $a20140502
906 $0VEN