Keynote
We have the pleasure of welcoming our keynote speakers at CompSys'21.
| Monday June 28th, 1:00-2:00pm |
| Ultrafast magnetism and Brain-inspired approaches for Green ICT |
| By Prof. Dr. Theo Rasing |
| Radboud University, Institute for Molecules and Materials, Nijmegen, the Netherlands |
| Abstract The explosive growth of digital data use and storage has led to an enormous rise in global energy consumption of Information and Communication Technology (ICT), which already stands at 7% of the world electricity consumption1. New ICT technologies, such as Artificial Intelligence push this exponentially increasing energy requirement even more, though the underlying hardware paradigm is utterly inefficient: tasks like pattern recognition can be performed by the human brain with only 20W, while conventional (super)computers require 10 MW. Therefore, the development of radically new physical principles that combine energy-efficiency with high speeds and high densities is crucial for a sustainable future. One of those is the use of non-thermodynamic routes that promises orders of magnitude faster and more energy efficient manipulation of bits2. Another one is neuromorphic computing, that is inspired by the notion that our brain uses a million times less energy than a supercomputer while, at least for some tasks, it even outperforms the latter. In this talk, I will discuss the state of the art in ultrafast manipulation of magnetic bits and present some first results3 to implement brain-inspired computing concepts in magnetic materials that operate close to these ultimate limits. [1] Lannoo, B. Energy consumption of ICT Networks. TREND Final Workshop Brussels (2013), PDF. [2] A. Kirilyuk, A. V. Kimel and Th. Rasing, Ultrafast optical manipulation of magnetic order, Rev. Mod. Phys. 82, 2731-2784 (2010). [3] A. Chakravarty, J.H. Mentink, C. S. Davies, K. Yamada, A.V. Kimel and Th. Rasing, Supervised learning of an opto-magnetic neural network with ultrashort laser pulses, Appl. Phys. Lett. 114, 192407 (2019) |
| Short bio Theo Rasing is professor of physics at Radboud University, Nijmegen, member of the Royal Dutch Academy of Arts and Sciences and Academia Europaea, honorary professor Wuhan University of Technology, honorary member Ioffe Institute in St. Petersburg, recipient ERC Synergy Grant 2019, ERC Advanced Grant 2013 and Spinoza Award 2008, highest scientific award of the Netherlands. His research focuses on the study and control of the properties of functional (molecular/ photonic/magnetic) nanomaterials on ultrafast (femtosecond) timescales. He has co-authored over 500 papers (h= 61, WoS), including 43 Physical Review Letters and 18 in Nature Group journals and co-inventor on 4 patent applications. A Physical Review Letters of 2007 was mentioned as a Breakthrough of the year by Science. |
| Tuesday June 29th, 1:00pm-2:00pm |
| Automated Verification of Parallel Nested DFS with the VerCors verifier |
| Prof. Dr. Marieke Huisman |
| University of Twente |
| Abstract The VerCors verifier is a tool set for the verification of parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. In this talk I will first give an overview of the VerCors verifier, and how it has been used for the verification of many different parallel and concurrent algorithms. In the second part of my talk I will zoom in on the verification of a parallel model checking algorithm. Model checking algorithms are typically complex algorithms whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging, and is often done manually. Model checking algorithms are often parallelized for efficiency reasons, which makes them even more error-prone, and thus we need to use mechanized techniques to reason about their correctness. I will show how we used Vercors to mechanically verify the parallel nested depth first algorithm of Laarman et al. We also show how having a mechanized proof supports the easy verification of various optimizations of the algorithm. As far as we are aware, this is the first deductive verification of a multi-core model checking algorithm. |
| Short bio Marieke Huisman is well-known for her work on program verification and specification, and software reliability. At the University of Twente, she leads the Formal Methods and Tools group. In 2011, she obtained an ERC Starting Grant for the VerCors project on the verification of concurrent software, where she studied practical verification of concurrent programs, and developed verification techniques for advanced programming and specification constructs. All verifications are supported by the VerCors tool set. In follow-up projects, the results have been expanded to programming languages for other parallel computing paradigms, such as GPUs and distribution (EU project CARP, NWO Top project VerDi). She currently is working on adding support to reason at a more abstract level, and to increase the level of automation of the verification process, as part of her NWO VICI project Mercedes (2018 - 2022). In 2013, she received the Netherlands Prize for ICT research 2013. |
