Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato)

  1. Home
  2. Ricerca
  3. Progetti
  4. Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato)
Data inizio
18 febbraio 2013
Durata (mesi) 
36
Dipartimenti
Informatica
Responsabili (o referenti locali)
Bonacina Maria Paola

The thrust of this project is to advance deduction-based software verification by short-circuiting its standard pipeline (static analyzer generates invariants; verifying compiler generates verification conditions; theorem prover proves or disproves them) by using theorem proving to support invariant generation and termination analysis. To this end the project will develop new interpolation techniques and model-constructing decision procedures.

Partecipanti al progetto

Maria Paola Bonacina
Professore ordinario
Nicola Fausto Spoto
Professore associato
Aree di ricerca coinvolte dal progetto
Intelligenza Artificiale
Artificial intelligence
Ingegneria del Software e verifica formale
Formal languages and automata theory
Sicurezza informatica
Software and application security

Attività

Strutture

Condividi