LEADER 00000nam a22005535i 4500 
001    978-3-319-06410-9 
003    DE-He213 
005    20151204163218.0 
007    cr nn 008mamaa 
008    140418s2014    gw |    s    |||| 0|eng d 
020    9783319064109|9978-3-319-06410-9 
024 7  10.1007/978-3-319-06410-9|2doi 
040    |dES-ZaU 
072  7 UMZ|2bicssc 
072  7 COM051230|2bisacsh 
082 04 005.1|223 
245 00 FM 2014: Formal Methods|h[electronic resource] :|b19th 
       International Symposium, Singapore, May 12-16, 2014. 
       Proceedings /|cedited by Cliff Jones, Pekka Pihlajasaari, 
       Jun Sun. 
264  1 Cham :|bSpringer International Publishing :|bImprint: 
       Springer,|c2014. 
300    XVIII, 750 p. 185 illus.|bonline resource. 
336    text|btxt|2rdacontent 
337    computer|bc|2rdamedia 
338    online resource|bcr|2rdacarrier 
347    text file|bPDF|2rda 
490 1  Lecture Notes in Computer Science,|x0302-9743 ;|v8442 
490 0  Springer eBooks.|aComputer Science 
505 0  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. 
520    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. 
650  0 Computer science. 
650  0 Software engineering. 
650  0 Computers. 
650  0 Computer logic. 
650  0 Mathematical logic. 
650  0 Management information systems. 
650 14 Computer Science. 
650 24 Software Engineering. 
650 24 Mathematical Logic and Formal Languages. 
650 24 Logics and Meanings of Programs. 
650 24 Management of Computing and Information Systems. 
650 24 Computation by Abstract Devices. 
700 1  Jones, Cliff.,|eeditor. 
700 1  Pihlajasaari, Pekka.,|eeditor. 
700 1  Sun, Jun.,|eeditor. 
710 2  SpringerLink (Online service) 
773 0  |tSpringer eBooks 
776 08 |iPrinted edition:|z9783319064093 
830  0 Lecture Notes in Computer Science,|x0302-9743 ;|v8442 
856 40 |uhttps://cuarzo.unizar.es:9443/login?url=https://
       dx.doi.org/10.1007/978-3-319-06410-9|zAcceso al texto 
       completo