Abstracts FLoC 2010 - Revision history

Nataliya at 09:19, 23 August 2010

2010-08-23T09:19:04Z

← Older revision		Revision as of 09:19, 23 August 2010
Line 65:		Line 65:
	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.		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.==		==Orna Grumberg. The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/b/b4/MLQA-9-7.pdf slides] here.==

	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.		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.

Flemming at 12:45, 14 August 2010

2010-08-14T12:45:02Z

← Older revision		Revision as of 12:45, 14 August 2010
Line 50:		Line 50:
	Morgan.)		Morgan.)

	==~~Marsha Chechik and~~ Arie Gurfinkel. Partial Models and Software Model-Checking. See [http://wiki.ercim.eu/wg/MLQA/images/5/52/Gurfinkel_mlqa2010_6up.pdf slides] here.==		==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		Partial models combine necessary and possible behaviours in a single

Nataliya at 12:21, 20 July 2010

2010-07-20T12:21:01Z

← Older revision		Revision as of 12:21, 20 July 2010
Line 102:		Line 102:
	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.		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 [[~~July 2010:~~ MLQA ~~meeting at FLoC~~ 2010~~, Edinburgh~~\|MLQA meeting at FLoC 2010]]		Go back to [[MLQA 2010\|MLQA meeting at FLoC 2010]]

Nataliya at 12:28, 12 July 2010

2010-07-12T12:28:50Z

Nataliya at 12:25, 12 July 2010

2010-07-12T12:25:54Z

← Older revision		Revision as of 12:25, 12 July 2010
Line 1:		Line 1:
	__NOTOC__		__NOTOC__
	==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/MLQA-BS.pdf slides] here.==		==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		Conceptually comparing the notions of Static Analysis and Model

Nataliya at 12:21, 12 July 2010

2010-07-12T12:21:46Z

← Older revision		Revision as of 12:21, 12 July 2010
Line 1:		Line 1:
	__NOTOC__		__NOTOC__
	==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/~~MLQA_2010_MCisSA~~.pdf slides] here.==		==Bernhard Steffen. From the How to the What: Static Analysis via Model Checking. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/MLQA-BS.pdf slides] here.==

	Conceptually comparing the notions of Static Analysis and Model		Conceptually comparing the notions of Static Analysis and Model

Nataliya at 12:21, 12 July 2010

2010-07-12T12:21:14Z

Nataliya at 12:12, 12 July 2010

2010-07-12T12:12:48Z

← Older revision		Revision as of 12:12, 12 July 2010
Line 14:		Line 14:
	story based on this understanding.		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.==		==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).		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).

Nataliya at 12:12, 12 July 2010

2010-07-12T12:12:37Z

← Older revision		Revision as of 12:12, 12 July 2010
Line 14:		Line 14:
	story based on this understanding.		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.==		==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).		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).

Nataliya at 12:12, 12 July 2010

2010-07-12T12:12:20Z

← Older revision		Revision as of 12:12, 12 July 2010
Line 14:		Line 14:
	story based on this understanding.		story based on this understanding.

	==Flemming Nielson. Model Checking is Static Analysis of Modal Logic. See [[~~MLQA2010MCisSA~~.pdf\|slides]] here.==		==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).		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).

← Older revision		Revision as of 12:28, 12 July 2010
Line 24:		Line 24:
	This is joint work with Hanne Riis Nielson, Fyuyan Zhang and Piotr Filipiuk.		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/4/4b/~~MLQA_2010_MCisSA~~.pdf slides] here.==		==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.		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.
Line 30:		Line 30:
	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.		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/4/4b/~~MLQA_2010_MCisSA~~.pdf slides] here.==		==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		Model checking probabilistic programs, typically represented as
Line 50:		Line 50:
	Morgan.)		Morgan.)

	==Marsha Chechik and Arie Gurfinkel. Partial Models and Software Model-Checking. See [http://wiki.ercim.eu/wg/MLQA/images/4/4b/~~MLQA_2010_MCisSA~~.pdf slides] here.==		==Marsha Chechik and 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		Partial models combine necessary and possible behaviours in a single
Line 94:		Line 94:
	techniques to succinct representations of e.g. probabilistic systems.		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/4/4b/~~MLQA_2010_MCisSA~~.pdf slides] here.==		==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.		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.