Satellite Events
iFM 2016 is co-located with and hosts the following events:
The 6th International Symposium on Unifying Theories of Programming (UTP 2016)
Co-located with iFM 2016.
June 4 - 5
Based on the pioneering work on Unifying Theories of Programming by Tony Hoare, He Jifeng, and others, the aims of the UTP Symposium series are to:
-
continue to reaffirm the significance of the ongoing UTP research,
-
encourage efforts to advance it by providing a focus for the sharing of results by those already actively contributing, and
-
raise awareness of the benefits of such unifying theoretical frameworks among the wider computer science and software engineering communities.
PrePost (Pre- and Post-Deployment Verification Techniques)
June 4
The workshop will be to bring together researchers working in the field of computer-aided validation and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems and runtime verification. We will also welcome contributions related to tools and applications of pre- and post-deployment verification.
iFMCloud'16: The First International Workshop on Formal Methods for and on the Cloud
June 4
Cloud solutions are increasingly used for a plethora of purposes, including solving memory-intensive and computation-intensive problems. Ensuring the reliability, availability, scalability, and security of cloud solutions, as networked distributed systems with properties such as dynamic reallocation of resources, is a challenging problem that requires rigorous modelling, analysis, and verification tools. Such tools can be devised using the techniques provided by the formal methods community. On the other hand, many formal analysis and verification tools are memory-intensive and computation-intensive solutions, which can benefit from the cloud technology. In this workshop, we intend to bring together researchers and practitioners from the two fields of formal methods and cloud computing – as well as experts in related fields such as computer and communication networks, and distributed systems – to discuss how the two fields can benefit from each other, and identify the challenges that need to be addressed for successful collaboration of the two fields.
Workshop on Verification and Validation of Cyber-Physical Systems (V2CPS)
June 4
The workshop on Verification and Validation of Cyber-Physical Systems is targeted at methods related to different aspects of cyber-physical systems with an emphasize on non-functional properties initiated from the physical world. A cyber-physical system (CPS) is an integration of networked computational and physical processes with meaningful inter-effects; the former monitors, controls, and affects the latter, while the latter also impacts the former.
CPSs have applications in a wide-range of systems spanning robotics, transportation, communication, infrastructure, energy, and manufacturing. Many safety-critical systems such as chemical processes, medical devices, aircraft flight control, and automotive systems, are indeed CPS. The advanced capabilities of CPS require complex software and synthesis algorithms, which are hard to verify. In fact, many problems in this area are undecidable. Thus, a major step is to find particular abstractions of such systems which might be algorithmically verifiable regarding specific properties of such systems, describing the partial/overall behaviours of CPSs.
The ultimate goal is to bring together researchers and experts of the fields of formal verification and CPS to cover the theme of this workshop, namely a wide spectrum of verification and validation methods including (but not limited to) control, simulation, formal methods, etc.
PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'16)
June 5
A Doctoral Symposium will be held in conjunction with Integrated Formal Methods 2016. This aims to provide a helpful environment in which selected PhD students can present and discuss their ongoing work, meet other students working on similar topics, and receive helpful advice and feedback from a panel of researchers and academics.
Web site
ICT COST Action IC1402 - Runtime Verification beyond Monitoring (ARVI) Meeting
June 4-5
The COST Action ARVI will hold a meeting in conjunction with the PrePost workshop. A management committee meeting will take place on Sunday, June 5.
Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behaviour. RV has emerged in recent years as a practical application of formal verification, and a less ad hoc approach to conventional testing by building monitors from formal specifications.
There is a great potential applicability of RV beyond software reliability, if one allows monitors to interact back with the observed system, and generalizes to new domains beyond computers programs (like hardware, devices, cloud computing and even human centric systems). Given the European leadership in computer based industries, novel applications of RV to these areas can have an enormous impact in terms of the new class of designs enabled and their reliability and cost effectiveness.