Synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software -- Synthesis of satisfiability procedures from theorem-proving strategies

  1. Home
  2. Research
  3. Projects
  4. Synthesis of deduction-based decision procedures with applications to the automatic formal analysis of software -- Synthesis of satisfiability procedures from theorem-proving strategies
Starting date
November 21, 2003
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Bonacina Maria Paola
URL
http://profs.sci.univr.it/~bonacina/prin2003.html
Keyword
Automated reasoning, decision procedures, model checking

As a growing number of critical applications depends on software reliability, software validation needs flexible, powerful and cost-effective techniques, that yet are easy to use. This project addresses these needs by developing and applying high-performance deduction technology to support automated formal analysis of software. Its approach combines the advantages of highly expressive logical reasoning and specialized decision procedures to yield efficient, push-button techniques.

Sponsors:

Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department

Project participants

Maria Paola Bonacina
Full Professor

Collaboratori esterni

Massimo Benerecetti
Università degli Studi di Napoli Federico II
Alessandro Armando
Università degli Studi di Genova
Silvio Ranise
INRIA Lorraine Ricercatore
Research areas involved in the project
Intelligenza Artificiale
Artificial intelligence
Publications
Title Authors Year
Canonical ground Horn theories Bonacina, Maria Paola; Nachum, Dershowitz 2013
New results on rewrite-based satisfiability procedures Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz 2009
Abstract canonical inference Bonacina, Maria Paola; Nachum, Dershowitz 2007
Rewrite-based satisfiability procedures for recursive data structures Bonacina, Maria Paola; Echenim, Bertrand Mnacho 2007
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz 2005
On handling distinct objects in the superposition calculus Stephan, Schulz; Bonacina, Maria Paola 2005
Towards a unified model of search in theorem proving: subgoal-reduction strategies Bonacina, Maria Paola 2005

Activities

Research facilities

Share