Мини-курсы профессоров Университета Лугано

Общая информация
ЛекторН. Шарыгина
Семестросень 2015
Дата начала05.09.2015
Количество пар8
Язык курсарусский

Краткие курсы профессоров факультета информатики Университета Лугано, Швейцария

Профессора Университета Лугано представят учебные программы магистерских и PhD программ факультета информатики и прочтут краткие курсы для студентов Санкт-Петербургских вузов по следующим предметам: программный анализ и формальные методы верификации; системы распределенного вычисления и методы их качественной оценки; методы геометрических вычислений и их применения в системах машинного зрения; и параллельные вычисления и численное моделирование.

Все лекции будут прочитаны на английском языке.

Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Presentation of USI and its study programs
(05.09.2015 - 16:30 - 17:15)

2. Методы геометрических вычислений и их применения в системах машинного зрения (Michael Bronstein)
(05.09.2015 - 17:20 - 18:55)

Michael Bronstein, University of Lugano, Switzerland / Perceptual Computing, Intel, Israel


The last decade has witnessed a series of technological breakthroughs in the acquisition, processing, and analysis of 3D geometric data, enabling applications that are revolutionizing our way of interaction with computers and pushing the boundaries of computer vision applications to super-human abilities. In this talk, I will tell a personal account of academic and industrial research in this exciting field.


Michael Bronstein is a professor in the Faculty of Informatics at the University of Lugano (USI), Switzerland and a Research Scientist at the Perceptual Computing group, Intel, Israel. Michael got his B.Sc. in Electrical Engineering (2002) and Ph.D. in Computer Science (2007), both from the Technion, Israel. His main research interests are theoretical and computational methods in spectral and metric geometry and their application to problems in computer vision, pattern recognition, computer graphics, image processing, and machine learning. His research appeared in international media and was recognized by numerous awards. In 2012, Michael received the highly competitive European Research Council (ERC) grant. In 2014, he was invited as a Young Scientist to the World Economic Forum New Champions meeting, an honor bestowed on forty world's leading scientists under the age of 40. Besides academic work, Michael is actively involved in the industry. He was the co-founder of the Silicon Valley start-up company Novafora, where he served as VP of technology (2006-2009), responsible for the development of algorithms for large-scale video analysis. He was a co-founder and one of the principal inventors and technologists at Invision, an Israeli startup developing 3D sensing technology acquired by Intel in 2012. His technology is now the core of the Intel RealSense 3D camera integrated into new generation computers.

3. Методы геометрических вычислений и их применения в системах машинного зрения (Michael Bronstein) - продолжение
(05.09.2015 - 19:05 - 20:50)

4. Программный анализ и формальные методы верификации (Natasha Sharygina)
(06.09.2015 - 11:15 - 12:50)


In the last decades there has been a considerable investment in the development of automatic techniques and tools with the goal of making the verification of hardware and software fully automatic. Among various approaches, Model Checking is highly appreciated for its exhaustiveness and degree of automation: once a model (of hardware or software) and a property (desired behavior) are given, a tool can be run to explore all possible behaviors of the model, determining whether the property is satisfied. The main difficulty connected with Model Checking is that for complex systems the size of the model often becomes too large to be handled in a reasonable amount of time (state space explosion). A remarkable improvement can be obtained by means of symbolic techniques: the model is encoded together with the property in a first order logic formula, valid if and only if the property is satisfied. One of the most successful symbolic techniques, Bounded Model Checking, is employed in several contexts and relies on efficient and robust tools such as SAT-Solvers or SMT-Solvers, whose performance have constantly improved along the years. The use of Abstraction is another important paradigm for mitigating the state explosion problem. The idea is to map the original model into a smaller abstract model, less expensive to check; this kind of approximation might introduce spurious behaviors, that have to be removed by means of a refinement phase. Since the seminal work of McMillan, the use of Craig's interpolants in model checking has been gaining a considerable attention; in particular, interpolants have been successfully exploited both in the context of Bounded Model Checking and Abstraction, where they guide the refinement phase. Given an unsatisfiable formula A^B, symbolic encoding of a violating behavior of the system (where A represents the behavior and B denotes the property), an interpolant I can be seen as an abstraction of A "guided" by B. As there are techniques available to construct different interpolants for a formula, it is fundamental to understand which interpolant has the highest "quality". Many scientific publications tend to associate the quality of interpolants with their size, in terms of number of occurrences of variables and operators. However, the size, as many other structural characteristics, are not necessarily connected with the interpolants effectiveness in the verification effort. This talk focuses on the notion of quality of interpolants and presents our recent research results identifying the features that characterize good interpolants, and outlines the new techniques that guide the generation of interpolants in order to improve the performance of state-of-the-art Model Checking approaches.


Natasha Sharygina is a Professor of Informatics at the University of Lugano, Switzerland and an adjunct Professor at School of Computer Science, Carnegie Mellon University, Pittsburgh, USA. Prof. Sharygina received a Ph.D. degree from the University of Texas at Austin, USA in 2002. Her professional experience includes consulting at Bell Labs, Lucent Technologies at the Computing Sciences Research in 2000-2001 and a research faculty position at Carnegie Mellon University, SEI in 2002-2005. Prof. Sharygina directs the USI Formal Verification and Security group whose research deals with improving the program development process through formal methods of specification and verification. Prof. Sharygina´s interests lie in software and hardware verification, temporal logics, model checking, SAT/SMT methods, and concurrent and distributed computing. Prof. Sharygina´s current focus is on applying automated formal methods to problems in computer security, electronic design automation, and program analysis. Prof. Sharygina is the recipient of various awards among which are the ACM recognition of service award and CMU Technical Excellence awards. Prof. Sharygina´s research has been funded by multiple grants including the CMU SEI Independent R&D grants, EU COST program, Tasso Career, the Swiss National Foundation, and Hasler Foundation awards.Prof. Sharygina has authored more than 80 research papers in areas of formal verification, and system design. She served on program committees of various conferences (e.g., CAV, TACAS, FMCAD, SPIN), given keynote and invited presentations, and co-chaired several workshops in the area of formal verification. Prof. Sharygina chaired program committees of FMCAD 2010 and CAV 2013, the major conferences in computer-aided verification and design.

5. Программный анализ и формальные методы верификации (Natasha Sharygina) - продолжение
(06.09.2015 - 13:00 - 14:35)

6. Вопросы и ответы
(06.09.2015 - 14:35 - 15:00)

7. Presentation of USI and its study programs
(12.09.2015 - 16:30 - 17:15)

8. Системы распределенного вычисления и методы их качественной оценки (Fernando Pedone)
(12.09.2015 - 17:20 - 18:55)


Many current internet services have stringent availability and performance requirements. High availability entails tolerating component failures and is typically accomplished with replication. For many online services, “high performance” essentially means the ability to serve an arbitrarily large load, something that can be achieved if the service can scale throughput when provided with additional resources (e.g., processors). In light of the requirements of modern services, combining high availability and high performance without sacrificing consistency is a challenging endeavor of utmost importance. This course will review state-machine replication (SMR), one of the most fundamental approaches to replication, and survey the latest techniques to turn SMR scalable.


Fernando Pedone is a full professor in the Faculty of Informatics at the University of Lugano (USI), Switzerland, and has been also affiliated with Cornell University, EPFL, and Hewlett-Packard Laboratories (HP Labs). He received the Ph.D. degree from EPFL in 1999. His research interests include the theory and practice of distributed systems and distributed data management systems. Fernando Pedone has authored more than 100 scientific papers and 6 patents. He is co-editor of the book "Replication: theory and practice", Springer 2010.

9. Системы распределенного вычисления и методы их качественной оценки (Fernando Pedone) - продолжение
(12.09.2015 - 19:05 - 20:50)

10. Параллельные вычисления и численное моделирование (Olaf Schenk)
(13.09.2015 - 11:15 - 12:50)


Are you interested in using Europe’s faster supercomputers (and getting ECTS credit points for doing so)? Would you like to learn how to write programs for parallel supercomputers, such as a Cray or a cluster of Graphics Processing Units? The course on supercomputing and simulations presents advanced topics in parallel computing and numerical simulation for prospective computational/software engineers. The course is designed to teach students how to program parallel computers to efficiently solve challenging problems in science and engineering, where very fast computers are required either to perform complex simulations or to analyze enormous datasets. It covers basic principles architectures, and algorithms of parallel systems. The course is structured in two parts: (i) introduction into supercomputing and applications, and (ii) and overview on basic graph partitioning parallel algorithm.


Olaf Schenk is a professor at the Institute of Computational Science within the Department of Informatics at the Universita della Svizzera italiana, Switzerland. He graduated in Applied Mathematics from Karlsruhe Institute of Technology (KIT), Germany, and earned his PhD in 2001 from the Department of Information Technology and Electrical Engineering of ETH Zurich, and a venia legendi from the Department of Mathematics and Computer Science from the University of Basel in 2009. He conducts research in numerical algorithms, computational science, and software tools for high-performance scientific computing. Olaf Schenk is a member of the Society for Industrial and Applied Mathematics (SIAM), the Association for Computing Machinery (ACM) and the Institute for Electrical and Electronic Engineers (IEEE). He is a recipient of an IBM faculty award (2009) and two leadership computing awards from the U.S. Department of Energy (2012, 2013). He serves on the editorial board of the SIAM Journal for Scientific Computing and on the project leadership team of the Swiss Platform for Advanced Scientific Computing (PASC).

11. Параллельные вычисления и численное моделирование (Olaf Schenk) - продолжение
(13.09.2015 - 13:00 - 14:35)

12. Вопросы и ответы
(13.09.2015 - 14:35 - 15:00)

Ваша оценка: Пусто Средняя: 5 (3 голосов)
Share |