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
Bioinformatica e informatica medica
Artificial intelligence  (DI)
Intelligenza Artificiale
Artificial intelligence  (DI)
Algebra, Geometria e Logica Matematica
Formal languages and automata theory  (DI)
Algoritmi, Logica e teoria della computazione
Formal languages and automata theory  (DI)  (DI)
Ingegneria del Software e verifica formale
Formal languages and automata theory  (DI)
Sicurezza informatica
Software and application security  (DI)
Ingegneria del Software e verifica formale
Software and application security  (DI)

Attività

Aree di ricerca

Gruppi di ricerca

Dottorati di Ricerca

Strutture

Condividi