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
Sistemi intelligenti
Artificial intelligence
Informatica teorica
Formal languages and automata theory
Ingegneria del Software e Sicurezza
Software and application security

Activities

Research facilities