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, 357 KB)
pdf Presentazione Research Day 2016  (pdf,  it, 6700 KB)
Maria Paola Bonacina
Full Professor
Davide Bresolin
Research Assistants
Mila Dalla Preda
Temporary Assistant Professor
Alessandra Di Pierro
Associate Professor
Roberto Giacobazzi
Full Professor
Zsuzsanna Liptak
Assistant Professor
Andrea Masini
Full Professor
Isabella Mastroeni
Associate Professor
Massimo Merro
Associate Professor
Roberto Posenato
Assistant Professor
Romeo Rizzi
Associate Professor
Roberto Segala
Full Professor
Ugo Solitro
Assistant Professor
Nicola Fausto Spoto
Associate Professor
Skills
Topic People Description ISI-CRUI
Theory of computation - Design and analysis of algorithms standard compliant  ACM 2012
Design and analysis of algorithms for graphs Roberto Posenato
Romeo Rizzi
Design and analysis of algorithms for constraint analysis in graphs. Computer Science & Engineering
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. Computer Science & Engineering
Theory of computation - Formal languages and automata theory standard compliant  ACM 2012
Teoria della dimostrazione e teoria dei tipi Gianluigi Bellin
Ugo Solitro
Sistemi deduttivi e di tipo basati su logiche costruttive e sulla logica lineare Computer Science & Engineering
Theory of computation - Logic standard compliant  ACM 2012
Lambda Calculus Andrea Masini
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs. Computer Science & Engineering
Logiche non classiche (intuizionista, lineare, modale, temporale) Davide Bresolin
Computer Science & Engineering
modal and temporal logics Andrea Masini
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
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 Computer Science & Engineering
Theory of computation - Models of computation standard compliant  ACM 2012
Computability Andrea Masini
Quantum and probabilistic computability. Implicit Complexity Theory. Computer Science & Engineering
Lambda Calculus Alessandra Di Pierro
Study of extended versions of the typed lambda calculus, in particular of probabilistic typing systems and their expressivity.
Modelli per sistemi ibridi Davide Bresolin
Marta Capiluppi
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. Computer Science & Engineering
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. Computer Science & Engineering
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 Computer Science & Engineering
Quantum computation theory Andrea Masini
Quantum lambda calculi. Topological quantum computing. Quantum computational complexity. Theory of quantum computable functions. Quantum theory of interaction. Computer Science & Engineering
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.
Theory of computation - Semantics and reasoning standard compliant  ACM 2012
Semantics Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Durica Nikolic
Ugo Solitro
Nicola Fausto Spoto
Computer Science & Engineering
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 Computer Science & Engineering
Semantics of Probabilistic Languages Alessandra Di Pierro
Construction of operational and denotational semantics via linear and abstract algebras.
Gruppi di ricerca
Name Description URL
ARLette Ricerca in ragionamento automatico 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/
Logica Logica in matematica ed informatica. https://logicseminarverona.wordpress.com/
Progettazione di sistemi elettronici (ESD - Electronic Systems Design) Tecniche per la progettazione automatica di sistemi elettronici, basate su linguaggi formali e metodologie corrette per costruzioni o formalmente verificate http://esd.scienze.univr.it/
QUILAB Quantum Informatics Laboratory
Robotica Il gruppo di ricerca si occupa di robotica non convenzionale
SPY
Projects
Title Managers Sponsors Starting date Duration (months)
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 1/1/13 48
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 1/1/12 24
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 2/5/15 11
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 1/1/13 30
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 2/18/13 36

Activities

Research facilities