演讲人：Holger Hermanns

德国Saarland大学计算机科学系教授、欧洲科学院院士

Academician of the Academy of Europe, full professor at the Department of Computer Science at Saarland University, holding the chair for Dependable Systems and Software. His research interests include modeling and verification of concurrent systems, resource-aware embedded systems, and compositional performance and dependability evaluation, including dependable energy distribution grids. Holger Hermanns co-chaired the program committees of major international conferences such as TACAS 2006, CONCUR 2006, CAV 2007, and QEST 2012. He serves on the steering committees of ETAPS, TACAS and QEST. He is president of the association "Friends of Dagstuhl e.V.", and vice president of the association "ETAPS e.V.".

Talk 1: How good is your embedded design, if at all?

Abstract: Performance, dependability, and security are notoriously difficult to quantify at system design time. Yet, design decisions are known to be the prime source of difficult-to-fix embedded problems. While for low budget or experimental designs it might suffice to perform some back-of-the-envelope calculations, a few component measurements, a bit of spread sheeting, maybe a rough Matlab model. But for mission critical or high volume applications deeper behavioral evaluations are needed early in the design process. This keynote will discuss a modest approach to deriving design-time guarantees for complex embedded behaviors, leveraging foundational insights to practical problems. The approach revolves around the stochastic timed automata formalism, and is supported by a portfolio of quantitative model checking techniques. This modest approach is exemplified in the context of different power-aware embedded applications.

Talk 2: Concurrent Programming Education in the Post-Java Era

Abstract: Many-core architectures-service orientation-business processes-app technology-pervasive systems -organic computing. All these are en vogue topics in computing practice. At their common core, they all revolve around ways to master and exploit concurrency. Unfortunately, concurrency is a notoriously difficult subject to master. Our students are facing the challenge. Do we educate them properly?

This presentation asks for concerted efforts to make our foundational concurrency education apt for the concurrency challenges. As a potential nucleus it presents , an open platform for light weight education of the core principles of concurrency theory and practice. This is wrapped in a simple, yet executable pseudocode notation, and features ways to study semantic as well pragmatic aspects of concurrent programming, covering both message-passing and shared-memory paradigms.

时间和地点

2 pm-3.20pm, 2015-10-16， 广楼G105.
 
 

演讲人：Joost-Pieter Katoen

德国RWTH Aachen大学计算机科学系教授、欧洲科学院院士

Academician of the Academy of Europe, full professor at the RWTH Aachen University in the Software Modeling and Verification (MOVES) group and part-time associated to the Formal Methods & Tools group at the University of Twente. His research include analysis of reactive, stochastic, real-time, and hybrid systems, formal software verification, in particular model checking, formal semantics of programming and modeling languages, formal modeling and analysis of distributed computing, concurrency theory. Joost-Pieter Katoen co-chaired the program committees of major international conferences such as CONCUR 2011. He serves on the steering committees of ETAPS, STTT, CONCUR and QEST.

Talk: Probabilistic Programming: A True Verification Challenge

Probabilistic programs are sequential programs with two added features:

(1) The ability to draw values at random from (possibly parametric) probability distributions;

(2) The ability to condition values of variables in a program through observations.

In this talk, I will address the following elementary issues of probabilistic programs: what do they mean? How to determine loop invariants? How to analyze parametric programs? And how hard is it to prove that a program almost surely terminates, i.e., terminates with probability one?

 

时间和地点

3.30pm-4.30pm, 2015-10-16， 广楼G105.