Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, ProceedingsCarlo A. Furia, Kirsten Winter This book constitutes the refereed proceedings of the 14th International Conference on Integrated Formal Methods, IFM 2018, held in Maynooth, Ireland, in September 2018. |
Contents
| 1 | |
| 20 | |
Differences Between KeY and OpenJML | 30 |
Design and Verification of RestartRobust Industrial Control Software | 47 |
Efficiently Characterizing the Undefined Requests of a RuleBased System | 69 |
Study of Integrating Random and Symbolic Testing for ObjectOriented Software | 89 |
Making Linearizability Compositional for Partially Ordered Executions | 110 |
Computing Minimal Executions Using SMT and CPSA | 130 |
Probabilistic Verification of Timing Constraints in Automotive Systems Using UPPAALSMC | 236 |
Facilitating the Implementation of Distributed Systems with Heterogeneous Interactions | 255 |
StateoftheArt Model Checking for B and EventB Using ProB and LTSmin | 275 |
Towards a Formal Notion of Impact Metric for CyberPhysical Attacks | 296 |
An Application to Production Logistics | 316 |
Branching Temporal Logic of Calls and Returns for Pushdown Systems | 326 |
Repair and Generation of Formal Models Using Synthesis | 346 |
ModeAware Concolic Testing for PLC Software | 367 |
A Precise Pictorial Language for Array Invariants | 151 |
Necessity Meets Opportunity | 161 |
Formal Modelling of Software Defined Networking | 172 |
ResourceAware Virtually Timed Ambients | 194 |
Stateful Behavioral Types for Active Objects | 214 |
Formalisation of SysMLKAOS Goal Assignments with B System Component Decompositions | 377 |
Analysing AWNSpecifications Using mCRL2 Extended Abstract | 398 |
Author Index | 419 |
Other editions - View all
Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth ... Carlo A. Furia,Kirsten Winter No preview available - 2018 |
Common terms and phrases
abstract algorithm analysis AODV approach attack BCARET behaviour benchmarks bisimulation buffer Carma causal linearizability Cham communication Comput configuration constraints context defined Definition denoted dynamic symbolic execution EAST-ADL ensure evaluation Event-B example formal methods formal verification formula function global goal HDBIP Heidelberg implementation input interactions interface invariant IoT systems iterative Java JDart JDoop label labelled transition system language LNCS logic LTSMIN machine MapReduce mCRL2 model checking module nodes OpenJML operation parameters partial order reduction ports postcondition predicate PROB probabilistic process algebra process calculus protocol relation restart-robust RoboChart rules runtime satisfied Sect semantics sensors sequence simulation specification Springer subsystem switch synthesis TACAS techniques temporal logic testing tick tion tool transition transition relation translation undefined requests unit testing updates UPPAAL-SMC valid values verification virtually timed ambients