FM 2009: Formal Methods | Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings | Ana Cavalcanti (u. a.) | Taschenbuch | xvii | Englisch | 2009 | Springer, Berlin - Paperback

EAN (ISBN-13): 9783642050886
ISBN (ISBN-10): 3642050883
Hardcover
Paperback
Publishing year: 2009
Publisher: Springer Berlin
820 Pages
Weight: 1,182 kg
Language: eng/Englisch

Book in our database since 2008-05-09T21:42:05+01:00 (London)
Book found last time on 2024-09-01T03:43:55+01:00 (London)
ISBN/EAN: 9783642050886

ISBN - alternate spelling:
3-642-05088-3, 978-3-642-05088-6
Alternate spelling and related search-keywords:
Book author: cavalcanti, dams, dennis
Book title: eindhoven, joaquin sorolla, 2009, lecture notes computer science, congress proceedings, world computer, berlin november

---

Information from Publisher

Author: Ana Cavalcanti; Dennis Dams
Title: Programming and Software Engineering; Lecture Notes in Computer Science; FM 2009: Formal Methods - Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings
Publisher: Springer; Springer Berlin
820 Pages
Publishing year: 2009-10-26
Berlin; Heidelberg; DE
Language: English
106,99 € (DE)
109,99 € (AT)
118,00 CHF (CH)
Available
XVII, 820 p.

BC; Hardcover, Softcover / Informatik, EDV/Informatik; Software Engineering; Verstehen; Informatik; B-method; C programming language; calculus; communication protocols; complexity; constraint solving; design; distributed systems; formal modeling; formal specification; logic; model checking; model-based testing; statistics; verification; Software Engineering; User Interfaces and Human Computer Interaction; Computer Science Logic and Foundations of Programming; Compilers and Interpreters; Programming Techniques; Mensch-Computer-Interaktion; Theoretische Informatik; Compiler und Übersetzer; Computerprogrammierung und Softwareentwicklung; EA

Invited Papers.- Formal Methods for Privacy.- What Can Formal Methods Bring to Systems Biology?.- Guess and Verify – Back to the Future.- Verification, Testing and Statistics.- Security, Probability and Nearly Fair Coins in the Cryptographers’ Café.- Model Checking I.- Recursive Abstractions for Parameterized Systems.- Abstract Model Checking without Computing the Abstraction.- Three-Valued Spotlight Abstractions.- Fair Model Checking with Process Counter Abstraction.- Compositionality.- Systematic Development of Trustworthy Component Systems.- Partial Order Reductions Using Compositional Confluence Detection.- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition.- Verification.- Abstract Specification of the UBIFS File System for Flash Memory.- Inferring Mealy Machines.- Formal Management of CAD/CAM Processes.- Concurrency.- Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way.- Symbolic Predictive Analysis for Concurrent Programs.- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study.- Refinement.- Sums and Lovers: Case Studies in Security, Compositionality and Refinement.- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing.- Model Checking Linearizability via Refinement.- Static Analysis.- It’s Doomed; We Can Prove It.- “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis.- Field-Sensitive Value Analysis by Field-Insensitive Analysis.- Theorem Proving.- Making Temporal Logic Calculational: A Tool for Unification and Discovery.- A Tableau for CTL*.- Certifiable Specification and Verification of C Programs.- Formal Reasoning about Expectation Properties for Continuous Random Variables.- Semantics.-The Denotational Semantics of slotted-Circus.- Unifying Probability with Nondeterminism.- Towards an Operational Semantics for Alloy.- A Robust Semantics Hides Fewer Errors.- Special Track: Industrial Applications I.- Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks.- Formal Verification of Avionics Software Products.- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.- Object-Orientation.- Connecting UML and VDM++ with Open Tool Support.- Language and Tool Support for Class and State Machine Refinement in UML-B.- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects.- Abstract Object Creation in Dynamic Logic.- Pointers.- Reasoning about Memory Layouts.- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis.- Real-Time.- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery.- Verifying Real-Time Systems against Scenario-Based Requirements.- Special Track: Tools and Industrial Applications II.- Formal Specification of a Cardiac Pacing System.- Automated Property Verification for Large Scale B Models.- Reduced Execution Semantics of MPI: From Theory to Practice.- Model Checking II.- A Metric Encoding for Bounded Model Checking.- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method.- Verifying Information Flow Control over Unbounded Processes.- Specification and Verification of Web Applications in Rewriting Logic.- Industry-Day Abstracts.- Verifying the Microsoft Hyper-V Hypervisor with VCC.- Industrial Practice in Formal Methods: A Review.- Model-Based GUI Testing Using Uppaal  at Novo Nordisk.