Quantities in Formal Methods
QFM 2012, the 1st workshop on Quantities in Formal Methods, will take place in Paris on 28 August 2012. It is associated with the 18th International Symposium on Formal Methods (FM2012), held at CNAM Paris 27-31 August.
Objective and Scope
This workshop will focus on quantities in modeling, verification, and synthesis. Modern applications of formal methods require to reason formally on quantities such as time, resources, or probabilities. Standard formal methods and tools have gotten very good at modeling (and verifying) qualitative properties: whether or not certain events will occur. During the last years, these methods and tools have been extended to also cover quantitative aspects, notably leading to tools like e.g. UPPAAL (for real-time systems), PRISM (for probabilistic systems), and PHAVer (for hybrid systems). A lot of work remains to be done however before these tools can be used in the industrial applications at which they are aiming. Particular issues are as follows:
- Almost all current methods and tools are not robust, in the sense that small changes in the quantitative inputs (e.g. due to measurement errors) can lead to large changes in the verification result. This is not desirable, and fixing it requires a paradigm switch away from the Boolean verification domain to real-valued domains.
- Most currently used algorithms for quantitative verification (and synthesis) are not efficient enough and do not scale well for industrial-size systems. New approaches, such as e.g. simulation-based statistical model checking, seem promising in this regard; but it is an open question how to apply them to synthesis.
- Almost all current methods and tools focus on only one quantitative aspect: either time, or resources, or probabilities. Integration of these formalisms is an active research area.
The aim of this workshop is to create a forum where current and new application areas can be discussed together with verification techniques that might apply to them. All researchers with an interest in systems exhibiting quantitative behaviour are welcome. In particular, papers on or related to the following topics are solicitated:
- Formal modeling, verification, and synthesis of quantitative behavior: timed, continuous and hybrid, probabilistic, costs and rewards, expected-value etc.
- Data structures for quantitative methods
- Quantitative techniques in refinement, simulation and bisimulation
- Quantitative algebraic and rewriting techniques
- Robustness of quantitative methods
- Industrial case-studies on any (combination) of the above, e.g. hardware verification and performance evaluation, security systems with probabilistic behavior, risk analysis in safety-critical systems, quantitative aspects of wireless networks, etc.
QFM will be held 28 August 2012, associated with the 18th International Symposium on Formal Methods (FM2012).
QFM embraces an inclusive formula that emphasizes interaction and discussion. Researchers are encouraged to submit new results, work in progress, work already published, or work submitted for publication elsewhere. Submissions will be judged on general quality and prospective interest to workshop participants. Papers will go through a usual peer-review process using Easychair and be reviewed by at least three reviewers.
The workshop itself will feature contributed talks, invited talks, and possibly a discussion session. It will last one day. Workshop proceedings will be published in EPTCS, and we will invite authors of selected papers for journal publication afterwards.