ERCIM Working Group MLQA - User contributions [en]

Abstracts FLoC 2010

2010-08-14T12:45:02Z

Flemming:

__NOTOC__
==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/51/MLQA-BS.pdf slides] here.==

Conceptually comparing the notions of Static Analysis and Model
Checking is delicate. Where are the technical differences, in
the use of logics, abstract interpretation, refinement techniques,
fixpoint computation? Or rather in their pragmatics: the one is fast
but often returns 'don't know', whereas the other may not terminate at
all (cf. Patrick Cousot)? It is hard to agree on a borderline,
and, in fact, earlier recongnized differences vanish as we go.
This is a good sign, as it shows that syngery already happens here,
as is also witnessed by the existence of conferences like VMCAI.
The talk will therefore present a personal view, and a success
story based on this understanding.

==Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/MLQA_2010_MCisSA.pdf slides] here.==

Flow Logic is an approach to the static analysis of programs that has been developed for functional, imperative and object-oriented programming languages and for concurrent, distributed, mobile and cryptographic process calculi. It is often implemented using an efficient differential worklist based solver (the Succinct Solver) working on contraints presented in a stratified version of Alternation-free Least Fixed Point Logic (ALFP).

In this talk we show how to deal with modal logics; to be specific we show how to deal with modal logics in the families CTL, ACTL and alternation-free modal mu calculus. We prove that we obtain an exact characterisation of the semantics of formulae in the modal logics and that we remain within stratified ALFP. The computational complexity of model checking by means of static analysis is as for classical approaches to model checking.

Together with the work of Steffen et al this allows us to conclude that the problems of model checking and static analysis are reducible to each other in many cases. This provides further motivation for transferring methods and techniques between these two approaches to verifying and validating programs and systems.

This is joint work with Hanne Riis Nielson, Fyuyan Zhang and Piotr Filipiuk.

==Marta Kwiatkowska. Quantitative Abstraction Refinement. See [http://wiki.ercim.eu/wg/MLQA/images/9/96/Marta-mlqa10.pdf slides] here.==

Probabilistic model checking has established itself as a valuable technique for formal modelling and analysis of systems that exhibit stochastic behaviour. It has been used to study quantitative properties of a wide range of systems, from randomised communication protocols to biological signalling pathways. In practice, however, scalability quickly becomes a major issue and, for large or even infinite-state systems, abstraction is an essential tool. What is needed are automated and efficient methods for constructing such abstractions.

In non-probabilistic model checking, this is often done using counterexample-guided abstraction-refinement (CEGAR), which takes a simple, coarse abstraction and then repeatedly refines it until it is amenable to model checking. This talk describes recent and ongoing work on quantitative abstraction-refinement techniques, which can be used to automate the process of building abstractions for probabilistic models. This has already been applied to probabilistic verification of software and of real-time systems, where abstraction is essential.

==Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See [http://wiki.ercim.eu/wg/MLQA/images/e/ee/Mlqa10_joost-pieter.pdf slides] here.==

Model checking probabilistic programs, typically represented as
Markov decision processes, is en vogue. Abstraction-refinement
techniques (a la CEGAR) have been developed and parametric model
checking approaches have recently been suggested. Prototypical
tools support these techniques. Their usage for programs whose
invariants are quantitative, i.e., arithmetic expressions in the
program variables, is however limited. An alternative is to re-
sort to static analysis techniques.

We present a constraint-based method for automatically generating quantitative invariants for probabilistic programs. We show how
it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed by
any of currently existing probabilistic model checkers. To our
knowledge, this is the first automated method for quantitative-
invariant generation.

(Joint work with Larissa Meinicke, Annabelle McIver and Carroll
Morgan.)

==Arie Gurfinkel. Partial Models and Software Model-Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/52/Gurfinkel_mlqa2010_6up.pdf slides] here.==

Partial models combine necessary and possible behaviours in a single
model. Since they encode both over- and under-approximation
of the behavior of the underlying system into a single model, they
allow both verification and falsification of a broad class of properties.
Thus, they are a natural choice for abstraction in model-checking.

Yasm is the first symbolic software model-checker to integrate partial models
with the Counterexample-Guided Abstraction Refinement (CEGAR) framework.
Yasm can prove and disprove temporal logic properties with equal effectiveness, and its performance is comparable to standard over-approximating model-checkers.

In this talk, we describe the types of partial models used by Yasm
and highlight some of our recent developments in software model-checking, including proving non-termination (i.e., finding counterexamples to liveness properties) and reasoning about recursive programs.

==Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.==

Model checking is a widely used technique for automatic verification of hardware and software systems. Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems.
''Abstraction'' is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is ''refined'' by adding some of the hidden details back.

In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed.
Finally, we will mention some applications of TVAR and try to convince that it is most useful.

==David Monniaux. Policy iteration for static analysis.==

Static analysis by abstract interpretation has traditionally computed
over-approximations of least fixed points (loops or recursive functions)
using Kleene iteration accelerated by widening operators. In recent
years, techniques inspired from game theory have been applied to
fixpoint problems in certain abstract domains: min-policy iterations (E.
Goubault's group) and max-policy iterations (H. Seidl's group). We shall
outline these techniques.

Finally, we shall discuss recent results, obtained with T. Gawlitza,
about the computation of least fixed points from succinct
representations of programs, giving the same precision as explicitly
distinguishing all program paths but with the same exponential
complexity as the coarse analysis that merges program paths (a naive
approach would incur double exponential complexity). The succinct
representation is exploited through SMT-solving.

We would appreciate insights for possible applications of such
techniques to succinct representations of e.g. probabilistic systems.

==Michael Huth. From validating quantitative models to generating valid ones. See [http://wiki.ercim.eu/wg/MLQA/images/b/b6/HuthMLQA10Talk.pdf slides] here.==

Verification techniques for quantitative systems typically require a system model as object of their investigations. Probabilistic model checking is a representative example of this successful approach.

However, emerging needs and constraints of quantitative systems no longer allow for, or benefit from, a complete decoupling of the development of a system from its a posteriori verification.

We paint a somewhat personal picture of what this may mean in terms of challenges and opportunities for those who research the construction of valid quantitative systems.

Go back to [[MLQA 2010|MLQA meeting at FLoC 2010]]

MLQA 2010

2010-08-14T12:10:57Z

Flemming:

The second annual meeting of the MLQA working group took place on Friday July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting was:

* '''Static Analysis versus Model Checking''': similarities, differences, synergies

The event consisted of a number of '''invited talks''', a [[Poster Session at MLQA 2010|'''poster session''']] and a '''business meeting'''. The purpose of invited talks was to cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen. At the poster session mainly the recent research of the participants and the work in progress was being presented. The long-lasting aim of the meeting was to lay the foundations for future research collaborations on challenging research problems.

--------------------------------------------------

See [http://wiki.ercim.eu/wg/MLQA/images/2/27/Handout.pdf '''Handout'''] of the meeting and [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] from the business meeting. See [[Poster Session at MLQA 2010]].

'''Programme for Friday, July 9'th 2010'''

(You can see the abstracts and slides of the talks by clicking on the talk titles).

Friday 9.00-10.00

* Bernhard Steffen. [[Abstracts FLoC 2010#Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See slides here.| From the How to the What: Static Analysis via Model Checking.]]
* Flemming Nielson. [[Abstracts FLoC 2010#Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See slides here.|Model Checking is Static Analysis of Modal Logic.]]

Friday 10.00-10.30

* Coffee & Poster Session

Friday 10.30-12.30

* Marta Kwiatkowska. [[Abstracts FLoC 2010#Marta Kwiatkowska. Quantitative Abstraction Refinement. See slides here.|Quantitative Abstraction Refinement.]]
* Joost-Pieter Katoen. [[Abstracts FLoC 2010#Joost-Pieter Katoen. Invariant Generation for Probabilistic Programs. See slides here.|Invariant Generation for Probabilistic Programs.]]
* Arie Gurfinkel. [[Abstracts FLoC 2010#Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See slides here.|Partial Models and Software Model-Checking.]]
* Orna Grumberg. [[Abstracts FLoC 2010#Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.|The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.]]

Friday 12.30-14.00

* Lunch

Friday 14.00-15.00

* David Monniaux. [[Abstracts FLoC 2010#David Monniaux. Policy iteration for static analysis.|Policy iteration for static analysis.]]
* Michael Huth. [[Abstracts FLoC 2010#Michael Huth. From validating quantitative models to generating valid ones. See slides here.|From validating quantitative models to generating valid ones.]]

Friday 15.00-15.30

* Coffee & Poster Session

Friday 15.30-17.00

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations. See [http://wiki.ercim.eu/wg/MLQA/images/a/a5/MLQA_2010_Minutes.pdf '''Minutes'''] taken during the meeting.

Main Page

2010-07-14T11:03:15Z

Flemming:

== ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) ==

[[Image:Image002.png|frame]] Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will

# consider process models formally described by transition systems, automata or process calculi,
# consider logics for expressing stochastic and continuous properties as well as discrete ones,
# focus on algorithms, theory and tools, and
# study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.

The MLQA home page: http://wiki.ercim.eu/wg/MLQA

The goal of this working group is to create a venue for knowledge sharing in this exciting area, for creating a network also for young researchers, for sharing tools developed within the field, for discussing research directions, and eventually to formulate a European project or network on formal quantitative analysis.

The working group will be open also to researchers outside of ERCIM (and outside of Europe).

== Past events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]] (9'th July, 2010)

[[March 2009: Kick-Off meeting in York]] (28'th March 2009)

Group Activities

2010-07-14T11:02:50Z

Flemming:

== Upcoming events ==

2011: Annual Meeting (details to be posted later)

== Past events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]] (9'th July, 2010)

[[March 2009: Kick-Off meeting in York]] (28'th March 2009)

== Related events ==

The QAPL workshop at ETAPS in Paphos, 27-28 March, 2010:
http://qav.comlab.ox.ac.uk/qapl10/

The QAPL summer school in Bertinoro, 21-26 June, 2010:
http://www.sti.uniurb.it/events/sfm10qapl/

List of Group Members

2010-07-14T11:01:08Z

Flemming:

== Individual Memberships ==

The group is open to all interested -- please sign up as indicated under Contact in the leftmost column.

== Chair and Steering Committee ==

At the MLQA 2010 Meeting the attendees elected a Chair that reports to ERCIM and a Steering Committee to ensure that the many good suggestions from the meeting be put into action.

* Flemming Nielson (Chair)
* Diego Latella
* Joost-Pieter Katoen
* Herbert Wiklicky
* Erik de Vink
* Catuscia Palamidessi

== Proposing Institutions ==

At present the following institutions, that are members of the national organisations taking part in ERCIM, support the MLQA working group (in alphabetical order and just one contact person per site):

* CNR (Italy) / Diego Latella
* CWI (Holland) / Jan Rutten
* INRIA (France) / Catuscia Palamidessi
* Oxford University (England) / Marta Kwiatkowska
* RWTH Aachen University (Germany) / Joost-Pieter Katoen
* Technical University of Berlin (Germany) / Uwe Nestmann
* Technical University of Denmark / Flemming Nielson
* Trinity College (Ireland) / Matthew Hennessy
* Universita’ di Firenze (Italy) / Rocco De Nicola
* University of Trento (Italy) / Paola Quaglia
* University of Edinburgh (Scotland) / Stephen Gilmore
* Universität des Saarlandes (Germany) / Holger Hermanns
* University of Aalborg (Denmark) / Kim Guldstrand Larsen

List of Group Members

2010-07-14T11:00:39Z

Flemming:

== Individual Memberships ==

The group is open to all interested -- please sign up as indicated under Contact in the leftmost column.

== Proposing Institutions ==

At present the following institutions, that are members of the national organisations taking part in ERCIM, support the MLQA working group (in alphabetical order and just one contact person per site):

* CNR (Italy) / Diego Latella
* CWI (Holland) / Jan Rutten
* INRIA (France) / Catuscia Palamidessi
* Oxford University (England) / Marta Kwiatkowska
* RWTH Aachen University (Germany) / Joost-Pieter Katoen
* Technical University of Berlin (Germany) / Uwe Nestmann
* Technical University of Denmark / Flemming Nielson
* Trinity College (Ireland) / Matthew Hennessy
* Universita’ di Firenze (Italy) / Rocco De Nicola
* University of Trento (Italy) / Paola Quaglia
* University of Edinburgh (Scotland) / Stephen Gilmore
* Universität des Saarlandes (Germany) / Holger Hermanns
* University of Aalborg (Denmark) / Kim Guldstrand Larsen

== Chair and Steering Committee ==

At the MLQA 2010 Meeting the attendees elected a Chair that reports to ERCIM and a Steering Committee to ensure that the many good suggestions from the meeting be put into action.

* Flemming Nielson (Chair)
* Diego Latella
* Joost-Pieter Katoen
* Herbert Wiklicky
* Erik de Vink
* Catuscia Palamidessi

Steering Committee

2010-07-14T10:58:49Z

Flemming:

At the MLQA 2010 Meeting the attendees elected a Chair that reports to ERCIM and a Steering Committee to ensure that the many good suggestions from the meeting be put into action.
== Chair of MLQA ==
* Flemming Nielson
== Steering Committee ==
* Flemming Nielson (Chair)
* Diego Latella
* Joost-Pieter Katoen
* Herbert Wiklicky
* Erik de Vink
* Catuscia Palamidessi

Steering Committee

2010-07-14T10:57:06Z

Flemming: New page: At the MLQA 2010 Meeting the attendees elected a Chair that reports to ERCIM: Flemming Nielson The attendees also elected a Steering Committee to ensure that the many good suggestions fro...

At the MLQA 2010 Meeting the attendees elected a Chair that reports to ERCIM:
Flemming Nielson
The attendees also elected a Steering Committee to ensure that the many good suggestions from the meeting be put into action:
Flemming Nielson (Chair)
Diego Latella
Joost-Pieter Katoen
Herbert Wiklicky
Erik de Vink
Catuscia Palamidessi

MediaWiki:Sidebar

2010-07-14T10:54:56Z

Flemming:

MLQA 2010

2010-03-10T09:31:49Z

Flemming:

The second annual meeting of the MLQA working group will take place on '''Friday July 9'th 2010''' as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* '''Static Analysis versus Model Checking''': similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems. As part of this there will be a poster session; instructions for how to submit posters will be forthcoming.

'''Draft Programme for Friday, July 9'th 2010'''

Friday 9.00-10.00

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

Friday 10.00-10.30

* Coffee & Poster Session

Friday 10.30-12.30

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)
* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

Friday 12.30-14.00

* Lunch

Friday 14.00-15.00

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

Friday 15.00-15.30

* Coffee & Poster Session

Friday 15.30-17.00

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations

'''Registration for the meeting''' should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-03-10T09:31:21Z

Flemming:

The second annual meeting of the MLQA working group will take place on '''July 9'th 2010''' as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* '''Static Analysis versus Model Checking''': similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems. As part of this there will be a poster session; instructions for how to submit posters will be forthcoming.

'''Draft Programme for July 9'th'''

Friday 9.00-10.00

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

Friday 10.00-10.30

* Coffee & Poster Session

Friday 10.30-12.30

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)
* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

Friday 12.30-14.00

* Lunch

Friday 14.00-15.00

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

Friday 15.00-15.30

* Coffee & Poster Session

Friday 15.30-17.00

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations

'''Registration for the meeting''' should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-03-10T09:29:44Z

Flemming:

The second annual meeting of the MLQA working group will take place on '''July 9'th 2010''' as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* '''Static Analysis versus Model Checking''': similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems. As part of this there will be a poster session; instructions for how to submit posters will be forthcoming.

'Draft Programme'''

Friday 9.00-10.00 (July 9'th)

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

Friday 10.00-10.30 (July 9'th) / Draft Programme

* Coffee & Poster Session

Friday 10.30-12.30 (July 9'th) / Draft Programme

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)
* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

Friday 12.30-14.00 (July 9'th) / Draft Programme

* Lunch

Friday 14.00-15.00 (July 9'th) / Draft Programme

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

Friday 15.00-15.30 (July 9'th) / Draft Programme

* Coffee & Poster Session

Friday 15.30-17.00 (July 9'th) / Draft Programme

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-03-10T09:27:22Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems. As part of this there will be a poster session; instructions for how to submit posters will be forthcoming.

Friday 9.00-10.00 (July 9'th) / Draft Programme

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

Friday 10.00-10.30 (July 9'th) / Draft Programme

* Coffee & Poster Session

Friday 10.30-12.30 (July 9'th) / Draft Programme

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)
* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

Friday 12.30-14.00 (July 9'th) / Draft Programme

* Lunch

Friday 14.00-15.00 (July 9'th) / Draft Programme

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

Friday 15.00-15.30 (July 9'th) / Draft Programme

* Coffee & Poster Session

Friday 15.30-17.00 (July 9'th) / Draft Programme

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-03-10T09:25:22Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems. As part of this there will be a poster session; instructions for how to submit posters will be forthcoming.

Friday 9.00-10.00 / Draft Programme

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

Friday 10.00-10.30 / Draft Programme

* Coffee & Poster Session

Friday 10.30-12.30 / Draft Programmme

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)
* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

Friday 12.30-14.00 / Draft Programme

* Lunch

Friday 14.00-15.00 / Draft Programme

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

Friday 15.00-15.30 / Draft Programme

* Coffee & Poster Session

Friday 15.30-17.00 / Draft Programme

* MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-03-10T09:21:03Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

We should also like to lay the foundations for future research collaborations on challenging research problems.

The draft programme is as follows:

Friday 9.00-10.00

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)

* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

On top of which we will have:

* MLQA Business Meeting (open to all attendees) about the future of MLQA

It will also be possible for attendees to present their own work, either in a poster session or by short 1-slide presentations; the format has not yet been decided.

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

The meeting is likely to start at 9am and to finish around 5pm or 6pm.

MLQA 2010

2010-02-17T08:09:30Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

The following list of presentations have been confirmed (but titles are tentative):

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)

* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

On top of which we will have:

* MLQA Business Meeting (open to all attendees) about the future of MLQA

It will also be possible for attendees to present their own work, either in a poster session or by short 1-slide presentations; the format has not yet been decided.

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

The meeting is likely to start at 9am and to finish around 5pm or 6pm.

MLQA 2010

2010-02-17T08:05:42Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

* Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

The following list of presentations have been confirmed (but titles are tentative):

* Bernhard Steffen (on performing static analysis by doing model checking)
* Flemming Nielson (on performing model checking by doing static analysis)

* Marta Kwiatkowska (on quantitative model checking)
* Joost-Pieter Katoen (on quantitative model checking)

* Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)
* Orna Grumberg (on the use of abstraction in model checking)

* David Monniaux (on operations research in static analysis and model checking)
* Michael Huth (on modelling and analysing control of access and risk)

On top of which we will have:

* MLQA Business Meeting (open to all attendees) about the future of MLQA

It will also be possible for attendees to present their own work, either in a poster session or by short 1-slide presentations; the format has not yet been decided.

Registration for the meeting should be part of registering for FLoC; I am told that the registration fees are likely to be:
* Early Academic 70.00, Early Student 42.00
* Regular Academic 100.00, Regular Student 58.00
* Late Academic 115.00, Late Student 66.00
All prices are in UK Pounds.

MLQA 2010

2010-01-22T13:01:43Z

Flemming:

MLQA 2010

2010-01-12T07:27:52Z

Flemming:

MLQA 2010

2010-01-12T07:27:03Z

Flemming:

MLQA 2010

2010-01-12T07:26:32Z

Flemming:

MLQA 2010

2010-01-11T07:52:22Z

Flemming:

MLQA 2010

2010-01-10T10:47:18Z

Flemming:

MLQA 2010

2010-01-10T10:44:48Z

Flemming:

The second annual meeting of the MLQA working group will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh (Scotland). The theme of the meeting is:

Static Analysis versus Model Checking: similarities, differences, synergies

The aim is to create a vibrant event consisting mainly of a number of invited talks that will cover some of the historical developments, survey the links established, establish state-of-the-art, identify the problems still worth pursuing and give a perspective on the implications and (novel) applications that can be foreseen.

The following presentations have been confirmed so far (but titles are tentative):

Bernhard Steffen (on performing static analysis by doing model checking)
Flemming Nielson (on performing model checking by doing static analysis)

Marta Kwiatkowska (on quantitative model checking)
Joost-Pieter Katoen (on quantitative model checking)

Marsha Chechik / Arie Gurfinkel (on the use of abstraction in model checking)

MediaWiki:Sidebar

2009-12-17T08:19:26Z

Flemming:

MediaWiki:Sidebar

2009-12-16T12:47:17Z

Flemming:

Group Activities

2009-12-01T15:12:12Z

Flemming:

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]] (9'th July, 2010)

== Past events ==

[[March 2009: Kick-Off meeting in York]] (28'th March 2009)

== Related events ==

The QAPL workshop at ETAPS in Paphos, 27-28 March, 2010:
http://qav.comlab.ox.ac.uk/qapl10/

The QAPL summer school in Bertinoro, 21-26 June, 2010:
http://www.sti.uniurb.it/events/sfm10qapl/

Contact

2009-12-01T15:10:08Z

Flemming:

==Mailing list==
A mailing list has been established for this working group with the homepage:
https://lists.ercim.org/wws/info/wg-mlqa-alert.
The purpose of the mailing list is to spread information concerning MLQA activities to all interested persons.

You can add yourself as a subscriber in the following way:
# Login into the webpage https://lists.ercim.org/wws/info/wg-mlqa-alert by inputing your e-mail and password. If you are new to the list, click on the "First login ?"-link on the left menu, input your e-mail and click on "Send me my password" button. You will receive the password by the e-mail.
# Click on the "Subscribe"-link in the menu on the left.

You can remove your subscription in the following way:
# Login into https://lists.ercim.org/wws/info/wg-mlqa-alert.
# Click on the "Unsubscribe"-link in the menu on the left.

You can post a message to the mailing list by sending it first to <mlqa(at)imm.dtu.dk>. The moderators of the mailing list will post it to the whole mailing list.

==Contact person==
Professor Flemming Nielson, DTU Informatics <mlqa(at)imm.dtu.dk>

List of Group Members

2009-12-01T15:09:41Z

Flemming:

MLQA 2010

2009-12-01T15:06:54Z

Flemming:

The next MLQA meeting will take place on July 9'th 2010 as part of FLoC 2010 in Edinburgh; details to be provided after Christmas.

Group Activities

2009-12-01T15:05:30Z

Flemming: /* Upcoming events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]] (9'th July, 2010)

== Past events ==

[[March 2009: Kick-Off meeting in York]] (28'th March 2009)

Group Activities

2009-12-01T15:04:49Z

Flemming: /* Past events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]]

== Past events ==

[[March 2009: Kick-Off meeting in York]] (28'th March 2009)

Group Activities

2009-12-01T15:04:31Z

Flemming: /* Past events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]]

== Past events ==

[[March 2009: Kick-Off meeting in York]] (29. March 2009)

Group Activities

2009-12-01T15:04:13Z

Flemming: /* Past events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]]

== Past events ==

[[March 2009: Kick-Off meeting in York] (29. March 2009)]

Group Activities

2009-12-01T15:03:34Z

Flemming: /* Past events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]]

== Past events ==

[[March 2009: Kick-Off meeting in York (March 28, 2009)]]

Group Activities

2009-12-01T15:02:59Z

Flemming: /* Past events */

== Upcoming events ==

[[July 2010: MLQA meeting at FLoC 2010, Edinburgh]]

== Past events ==

[[28.March 2009: Kick-Off meeting in York]]

Press

2009-11-06T15:09:32Z

Flemming: New page: This page is temporarily blank.

This page is temporarily blank.

MediaWiki:Sidebar

2009-11-06T15:08:55Z

Flemming: