E-raamat: FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings

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.