MCUNLEASH

Model Checking Unleashed

Coordinatore	UNIVERSITAET KASSEL    more Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie.
Nazionalità Coordinatore	Germany [DE]
Totale costo	1˙364˙405 €
EC contributo	1˙364˙405 €
Programma	FP7-IDEAS-ERC Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013)
Code Call	ERC-2010-StG_20091028
Funding Scheme	ERC-SG
Anno di inizio	2010
Periodo (anno-mese-giorno)	2010-12-01   -   2015-11-30

 Partecipanti

#	participant	country	role	EC contrib. [€]
1	UNIVERSITAET KASSEL  Organization address address: MONCHEBERGSTRASSE 19 city: KASSEL postcode: 34125 contact info Titolo: Ms. Nome: Sigrid Cognome: Reinhard Email: send email Telefono: 495618000000 Fax: 495618000000	DE (KASSEL)	hostInstitution	1˙364˙405.40
2	UNIVERSITAET KASSEL  Organization address address: MONCHEBERGSTRASSE 19 city: KASSEL postcode: 34125 contact info Titolo: Prof. Nome: Martin Cognome: Lange Email: send email Telefono: +49 561 8046261 Fax: +49 561 8046627	DE (KASSEL)	hostInstitution	1˙364˙405.40

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'Model checking is a technique which is being used successfully in automatic program. More than 25 years of research on model checking has brought forward various techniques and tricks which can handle complex tasks or just massive structures as caused by the state-space explosion problem for instance. Mathematically, the model checking problem is to determine whether or not a given relational structure is a model of a given formula, typically of a temporal logic. In the domain of program verification, very weak temporal logics suffice in order to express relevant properties. Temporal logics of higher expressive power can naturally express more complex properties. In particular, there already are logics which can express all kinds of decision problems in the range of NP and above. In this project we will investigate the use of advanced model checking techniques for the solving of decision and computation problems in all kinds of diverse areas like bio-informatics, database querying, network routing, computational linguistics, etc. We will, for example, identify important problems in this area, encode them as model checking problems in logics of suitable expressive power, and use partial evaluation, manual optimisations, and the vast toolbox of model checking specialisations in order to obtain new and competitive algorithms for and insights into such problems. We will design suitable temporal logics where there are none, and build model checking algorithms which serve as a generic starting point for the solving of such problems.'