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

  1. Home
  2. Research
  3. Projects
  4. Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato)
Starting date
February 18, 2013
Duration (months)
36
Departments
Computer Science
Managers or local contacts
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.

Project participants

Maria Paola Bonacina
Full Professor
Nicola Fausto Spoto
Associate Professor
Research areas involved in the project
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)

Activities

Research areas

Research groups

PhD Programmes

Research facilities

Share