Integrated Formal Methods (eBook, PDF)

12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings
Redaktion: Ábrahám, Erika; Huisman, Marieke

• Format: PDF

Produktbeschreibung

This book constitutes the refereed proceedings of the 12th International Conference on Integrated Formal Methods, IFM 2016, held in Reykjavik, Iceland, in June 2016. The 33 papers presented in this volume were carefully reviewed and selected from 99 submissions. They were organized in topical sections named: invited contributions; program verification; probabilistic systems; concurrency; safety and liveness; model learning; SAT and SMT solving; testing; theorem proving and constraint satisfaction; case studies.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer Nature Switzerland
• Seitenzahl: 538
• Erscheinungstermin: 23. Mai 2016
• Englisch
• ISBN-13: 9783319336930
• Artikelnr.: 53150811

Inhaltsangabe

Invited Contributions.- Can Formal MethodsImprove the Efficiency of Code Reviews.-Symbolic Computation and AutomatedReasoning for Program Analysis.- Program verification.- On Type CheckingDelta-Oriented Product Lines.- Verifying a priority scheduler for an SCJruntime environment.- Why Just Boogie? Translating Between Intermediate VerificationLanguages.- Probabilistic systems.- Statistical Approximation of OptimalSchedulers for Probabilistic Timed Automata.- Probabilistic Formal Analysis ofApp Usage to Inform Redesign.- Extension of PRISM by Synthesis of OptimalTimeouts in Fixed-Delay CTMC.- Concurrency.- Monitoring Multi-threaded Component-BasedSystems.- A Generalised Theory of Interface Automata, Component Compatibility andError.- On Implementing a Monitor-Oriented Programming Framework for ActorSystems.- Towards a Thread-Local Proof Technique for Starvation Freedom.- Reasoningabout Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems.-A Formal Model of the Safety-Critical Java Level 2 Paradigm.- Safety andliveness.- Deciding Monadic Second Order Logic over omega-words by Specialized FiniteAutomata.- Property Preservation for Extension Patterns of State TransitionDiagrams.- Symbolic Reachability Analysis of B through ProB and LTSmin.- Modellearning.- Enhancing Automata Learning by Log-Based Metrics.- Refactoring ofLegacy Software using Model Learning and Equivalence Checking: an IndustrialExperience Report.- On Robust Malware Classifiers by Verifying UnwantedBehaviours.- SAT and SMT solving.- Efficient Deadlock-Freedom Checking usingLocal Analysis and SAT Solving.- SMT Solvers for Validation of B and Event-Bmodels.- Avoiding Medication Conflicts for Patients with Multimorbidities.- Testing.-Temporal Random Testing for Spark Streaming.- Combining Static Analysis andTesting for Deadlock Detection.- Fuzzing JavaScript Engine APIs.- Theoremproving and constraint satisfaction.- A Component-based Approach to HybridSystemsSafety Verification.- Verifying Pointer Programs using Separation Logicand Invariant Based Programming in Isabelle.- A Constraint Satisfaction Methodfor Configuring Non-Local Service Interfaces.- Case studies.- Rule-basedConsistency Checking of Railway Infrastructure Designs.- Formal Verification ofSafety PLC Based Control Software.- Enabling Static Driver Verifier usingMicrosoft Azure.