Theory of computation

The Department's research in this area covers a rich variety of topics, including: automated reasoning, computability, concurrency, cryptographic protocols, design and analysis of algorithms, equational logic and rewriting, logic and verification, modal and temporal logics, pattern matching, probabilistic computation, program analysis, program semantics, proof theory, quantum computation theory, rewrite systems, verification by model checking.

Documents

pdf Brochure di presentazione dell'area  (pdf,  it, 240 KB)
pdf Presentazione Research Day 2017  (pdf,  it, 2429 KB)
Maria Paola Bonacina
Full Professor
Mila Dalla Preda
Associate Professor
Alessandra Di Pierro
Associate Professor
Roberto Giacobazzi
Full Professor
Zsuzsanna Liptak
Associate Professor
Andrea Masini
Full Professor
Isabella Mastroeni
Associate Professor
Massimo Merro
Full Professor
Roberto Posenato
Associate Professor
Romeo Rizzi
Full Professor
Roberto Segala
Full Professor
Ugo Solitro
Assistant Professor
Nicola Fausto Spoto
Associate Professor
Margherita Zorzi
Temporary Assistant Professor
Research interests
Topic People Description
Design and analysis of algorithms standard compliant  ACM 2012
String algorithms Zsuzsanna Liptak
Algorithms and data structures for strings; indexing for string problems; exact pattern matching, approximate pattern matching, string distance measures, storage, compression; problems arising in applications of strings such as computational biology, web data, textual data, big data, musical analysis; string combinatorics,combinatorics on words.
Design and analysis of algorithms for graphs Roberto Posenato
Romeo Rizzi
Design and analysis of algorithms for constraint analysis in graphs.
Formal languages and automata theory standard compliant  ACM 2012
Teoria della dimostrazione e teoria dei tipi Ugo Solitro
Margherita Zorzi
Sistemi deduttivi e di tipo basati su logiche costruttive e sulla logica lineare
Logic standard compliant  ACM 2012
Lambda Calculus Andrea Masini
Margherita Zorzi
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs.
modal and temporal logics Andrea Masini
Margherita Zorzi
Proof theoretical analysis of modal and temporal logics. Modal and temporal logics for security. Distribute logics. Branching a linear temporal logics.
proof theory, Linear logic, Type theory Andrea Masini
Margherita Zorzi
Sequent calculi for modal, linear and temporal logics. Natural deduction systems for modal, linear and temporal logics. Labelled deductive systems. Type systems for CPS. Proof nets for linear and classical logics. Deductive systems for quantum computability.
Software Verification Maria Paola Bonacina
Decision procedures for satisfiability modulo theories and their application to check program properties; invariant generation by theorem proving; interpolating theorem proving; abstraction refinement for either model checking or static analysis by theorem proving
Models of computation standard compliant  ACM 2012
Computability Andrea Masini
Margherita Zorzi
Quantum and probabilistic computability. Implicit Complexity Theory.
Lambda Calculus Alessandra Di Pierro
Margherita Zorzi
Study of extended versions of the typed lambda calculus, in particular of probabilistic typing systems and their expressivity.
Modelli per sistemi ibridi Roberto Segala
Studio di modelli per la rappresentazione di sistemi concorrenti che esibiscono comportamenti sia discreti che continui. Uso dei modelli per l'analisi di sistemi distribuiti di controllo.
Modelli stocastici concorrenti Roberto Segala
Studio di modelli di concorrenza che includono comportamenti stocastici. Uso di tali modelli per l'analisi di sistemi distribuiti e di protocolli che fanno uso di primitive crittografiche.
Models for concurrent, distributed, and mobile systems Massimo Merro
Process calculi for concurrent, distributed, and mobile systems. More recently, process calculi for cyber-physical systems and IoT systems
Quantum computation theory Andrea Masini
Margherita Zorzi
Quantum lambda calculi. Topological quantum computing. Quantum computational complexity. Theory of quantum computable functions. Quantum theory of interaction.
Topological Quantum Computation Alessandra Di Pierro
Re-writing systems for Topological Quantum Computation (TQC) and study of new algorithmic techniques based on the mathematical model of TQC.
Semantics and reasoning standard compliant  ACM 2012
Program semantics Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Ugo Solitro
Nicola Fausto Spoto
Development of semantic models for characterizing security and analysis problems of programming languages
Semantics of concurrent, distributed, and mobile systems Massimo Merro
Semantics of concurrent, distributed, and mobile computations. Associated with these semantic theories come specification techniques and verification technologies for assuring the behaviour of systems
Semantics of Probabilistic Languages Alessandra Di Pierro
Margherita Zorzi
Construction of operational and denotational semantics via linear and abstract algebras.
Gruppi di ricerca
Name Description URL
Algoritmi Il gruppo persegue lo studio degli aspetti strutturali di problemi fondamentali in informatica e dei loro modelli. Lo scopo è porre le basi per la progettazione di algoritmi protocolli e sistemi migliori e comprenderne i limiti computazionali. Aree specifiche di interesse includono: progettazione di algoritimi, strutture dati, algoritmi su stringhe, complessità, ottimizzazione combinatoriale, codici e teoria dell’informazione, machine learning. I problemi investigati hanno forti connessioni con le aree della bioinformatica, delle reti di comunicazione, della ricerca operativa e dell’intelligenza artificiale.
Algoritmi in Bioinformatica e Calcolo Naturale Applicazione di metodi teorici e di analisi dati per modellare l’informazione sottostante ai processi biologici: algoritmi su grafi e stringhe per la biologia dei sistemi; strutture dati avanzate per sequenze di dati; misure di distanza tra sequenze biologiche; calcolo naturale (biotecnologico, e a membrane), riconoscimento di pattern, e apprendimento automatico da dati biomedicali.
ARLette - Laboratorio di Ragionamento Automatico Il gruppo svolge ricerche in Ragionamento Automatico: dimostrazione di teoremi, procedure di decisione, soddisfacibilità modulo assegnamenti, costruzione di modelli, riscrittura, e applicazioni. http://profs.sci.univr.it/~bonacina/ARLette.html
Basi di dati e Sistemi Informativi Questo gruppo di ricercatori si occupa di varie tematiche nell'ambito dei sistemi informativi http://stars.di.univr.it
Bioinformatica e Calcolo Naturale Analisi algoritmica di processi biologici http://bioinformatics.di.univr.it/
Blockchain L'attività del gruppo di ricerca riguarda diverse tematiche relative allo sviluppo e all'applicazione della tecnologia blockchain e dell'infrastruttura degli smart contracts.
ForME - Metodi Formali per la Progettazione di Sistemi Ingegneristici Obiettivo del gruppo di ricerca è applicare metodi formali alla modellazione, verifica e sintesi di sistemi ingegneristici. I domini spaziano dai sistemi temporizzati per andare fino ai sistemi ciberfisici non lineari.
INdAM - Unità di Ricerca dell'Università di Verona Raccogliamo qui le attività scientifiche dell'Unità di Ricerca dell'Istituto Nazionale di alta Matematica INdAM presso l'Università di Verona
Intelligenza Artificiale (IA) Il gruppo svolge ricerche in Intelligenza Artificiale: Ragionamento Automatico, Algoritmi di Ricerca, Rappresentazione della Conoscenza, Apprendimento Automatico, Sistemi Multi-Agenti e applicazioni.
Logica Logica in matematica ed informatica. https://www.logicverona.it/
NeST Progettazione e verifica delle tecnologie di comunicazione in grado di portare efficienza e sostenibilità in applicazioni chiave come industria, agricoltura, domotica, trasporti e gestione del territorio.
Quantum Informatics Laboratory - QUILAB Laboratorio di Informatica Quantistica https://amasini58.wixsite.com/quilab
SPY
Projects
Title Managers Sponsors Starting date Duration (months)
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 2/5/15 11
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 2/18/13 36
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 1/1/13 48
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 1/1/12 24

Activities

Research facilities