Kategorier
Events

DIREC TALKS: Formal Verification and Machine Learning Joining Forces

Formal Verification and Machine Learning Joining Forces

The growing pervasiveness of computerised systems such as intelligent traffic control or energy supply makes our society vulnerable to faults or attacks on such systems. Rigorous software engineering methods and supporting efficient verification tools are crucial to encounter this threat.

In this DIREC talk Kim Guldstrand Larsen will present and discuss how to combine formal verification and AI in order to obtain optimal AND guaranteed safe strategies.

The ultimate goal of synthesis is to disrupt traditional software development. Rather than tedious manual programming with endless testing and revision effort, synthesis comes with the promise of automatic correct-by-construction control software.

In formal verification synthesis has a long history for discrete systems dating back to Church’s problem concerning realization of logic specifications by automata. Within AI the use of (deep) reinforcement learning (Q- and M-learning) has emerged as a popular method for learning optimal control strategies through training, e.g. as applied by autonomous driving.

The formal verification approach and the AI approach to synthesis are highly complementary: Formal verification synthesis comes with absolute guarantees but are computationally expensive with resulting strategies being extremely large. In contrast, AI synthesis comes with no guarantees but is highly scalable with neural networks providing compact strategy representation.

Kim Guldstrand Larsen will present the tool UPPAAL Stratego that combines symbolic techniques with reinforcement learning to achieve (near-)optimality and safety for hybrid Markov decision processes and highlight some of the applications that include water management, traffic light control, and energy aware building.

Emphasis will be on the challenges of implementing learning algorithms, argue for their convergence and designing data structures for compact and understandable strategy representation.

KIM GULDSTRAND LARSEN

PROFESSOR OF COMPUTER SCIENCE,
AALBORG UNIVERSITY

Speaker

KIM GULDSTRAND LARSEN

Kim Guldstrand Larsen is a Professor of Computer Science at Aalborg University since 1993. He received Honorary Doctorate from Uppsala University (1999), ENS Cachan (2007), International Chair at INRIA (2016) and Distinguished Professor at North-Eastern University, Shenyang, China (2018). His research interests cover modeling, verification, performance analysis of real-time and embedded systems with applications to concurrency theory, model checking and machine learning.  

He is the prime investigator of the verification tool UPPAAL for which he received the CAV Award in 2013. Other prizes received include Danish Citation Laureates Award, Thomson Scientific Award as the most cited Danish Computer Scientist in the period 1990-2004 (2005), Grundfos Prize (2016), Ridder af Dannebrog (2007). He is member of the Royal Danish Academy of Sciences and Letters, The Danish Academy of Technical Science, where he is Digital wiseman. Also, he is member of the Academia Europaea.

In 2015 he received the prestigious ERC Advanced Grant (LASSO), and in 2021 he won Villum Investigator Grant (S4OS).  He has been PI and director of several large centers and initiatives including CISS (Center for Embedded Software systems, 2002-2008), MT-LAB (Villum-Kahn Rasmussen Center of Excellence, 2009-2013), IDEA4CPS (Danish-Chinese Research Center, 2011-2017), INFINIT National ICT Innovation Network, 2009-2020), DiCyPS (Innovation Fund Center, 2015-2021). Finally, he is co-founder of the companies UP4ALL (2000), ATS (2017) and VeriAal (2020).

Kategorier
Events

Digital Tech Summit 2021

Mød landets ypperste forskere og startups på Digital Tech Summit

Digital Tech Summit bliver Nordens største udstillingsvindue for digitale teknologier, forskningsmiljøer, virksomheder og startups.

Konferencens hovedtaler er EU-kommissionens ledende næstformand Margrethe Vestager, der vil dele sine visioner for et stærkt europæisk digitalt lederskab gennem målrettede forsknings-og teknologisatsninger, særligt med fokus på, hvordan vi udvikler og anvender kunstig intelligens.

Et andet hovednavn er Serge Belongie, direktør for det nye AI Pioneer Centre, skal sende dansk forskning i kunstig intelligens helt til tops. Han indvier publikum i nogle de nyeste forskningsområder inden for brug af computer vision og billedkendelse, som vil kunne styrke samfundet i de kommende år.

Blandt keynote-speakere er også professor Jan Madsen fra DTU, der vil tale om Embedded AI and hardware. Professor Kaj Grønbæk fra AU deltager i Digital Tech Summit Grand Closing, der er en samtale mellem Rikke Hvilshøj, direktør i Dansk IT samt Rikke Hougaard Zeberg, der er direktør i DI Digital.

Her er et lille udpluk af oplægsholdere:
Mød professor Mikkel Baun Kjærgaard fra SDU i en Scientific Talk, hvor han taler om Software Technologies for connecting IoT and Robotics.

Professor Kim Guldstrand Larsen fra AAU taler om Digital Energy – using IoT, Big Data and AI for the Green Transition. Kim deltager også i en session med professor Christian S. Jensen fra AAU om digitalization in Vehicular Transportation.

Mød også asociate professor Claus Brabrand, der i en Scientific Talk taler om increasing diversity in IT education.

Messen byder også på et stort startupområde, hvor der pt. er tilmeldt 60 startups på tværs af de danske universiteter – det foregår i samarbejde med Open Entrepreneurship.

Gert Læssøe Mikkelsen fra Alexandra Instituttet deltager i en Business Talk om Security by design – why is it not happening.

Der er desuden masterclasses, pitch event, matchmaking og læringsworkshop ( i samarbejde med Kring Innovation).


På messen kan henved 5000 besøgende møde 70 udstillende virksomheder, heriblandt GN Group, Netcompany, Novo, Siemens, AMBU, 3Shape, der viser deres nyeste digitale teknologiske løsninger frem og inviterer jobkandidater indenfor. På messens start-upområde præsenteres helt nye forretningsideer og universiteternes samlede startup-økosystem.

Hele programmet kan ses her