Integrated Formal Methods

12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings
1. Auflage 2016
ISBN: 978-3-319-33692-3
Verlag: Springer International Publishing

Buch, Englisch, 538 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 8248 g

Reihe: Programming and Software Engineering

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.

Zielgruppe

Research

Autoren/Hrsg.

Huisman, Marieke

Ábrahám, Erika

Fachgebiete

• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Software Engineering Modellierung, UML, SysML
• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmier- und Skriptsprachen
• Mathematik | Informatik EDV | Informatik Informatik Logik, formale Sprachen, Automaten

Inhaltsverzeichnis

Invited Contributions.- Can Formal Methods
Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated
Reasoning for Program Analysis.- Program verification.- On Type Checking
Delta-Oriented Product Lines.- Verifying a priority scheduler for an SCJ
runtime environment.- Why Just Boogie? Translating Between Intermediate Verification
Languages.- Probabilistic systems.- Statistical Approximation of Optimal
Schedulers for Probabilistic Timed Automata.- Probabilistic Formal Analysis of
App Usage to Inform Redesign.- Extension of PRISM by Synthesis of Optimal
Timeouts in Fixed-Delay CTMC.- Concurrency.- Monitoring Multi-threaded Component-Based
Systems.- A Generalised Theory of Interface Automata, Component Compatibility and
Error.- On Implementing a Monitor-Oriented Programming Framework for Actor
Systems.- Towards a Thread-Local Proof Technique for Starvation Freedom.- Reasoning
about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems.-
A Formal Model of the Safety-Critical Java Level 2 Paradigm.- Safety and
liveness.- Deciding Monadic Second Order Logic over omega-words by Specialized Finite
Automata.- Property Preservation for Extension Patterns of State Transition
Diagrams.- Symbolic Reachability Analysis of B through ProB and LTSmin.- Model
learning.- Enhancing Automata Learning by Log-Based Metrics.- Refactoring of
Legacy Software using Model Learning and Equivalence Checking: an Industrial
Experience Report.- On Robust Malware Classifiers by Verifying Unwanted
Behaviours.- SAT and SMT solving.- Efficient Deadlock-Freedom Checking using
Local Analysis and SAT Solving.- SMT Solvers for Validation of B and Event-B
models.- Avoiding Medication Conflicts for Patients with Multimorbidities.- Testing.-
Temporal Random Testing for Spark Streaming.- Combining Static Analysis and
Testing for Deadlock Detection.- Fuzzing JavaScript Engine APIs.- Theorem
proving and constraint satisfaction.- A Component-based Approach to Hybrid
SystemsSafety Verification.- Verifying Pointer Programs using Separation Logic
and Invariant Based Programming in Isabelle.- A Constraint Satisfaction Method
for Configuring Non-Local Service Interfaces.- Case studies.- Rule-based
Consistency Checking of Railway Infrastructure Designs.- Formal Verification of
Safety PLC Based Control Software.- Enabling Static Driver Verifier using
Microsoft Azure.