Upcoming Events

Dr. Andres Goens , The University of Edinburgh, School of Informatics

Towards compilers for correct-by-construction hardware design

20.09.2022 (Tuesday) , 16:00 - 17:30
Barkhausen-Bau, Room BAR E85 // Online Access below , Dresden


Verification and formal methods have long been embraced by hardware manufacturers. However, these are usually used late in the design process, at the Register Transfer Level.   On the other hand, verification in programming languages, while less widespread, has seen many promising advances. In this talk we will explore ongoing work to bring some of these advances to hardware design methods. By raising the level of abstraction, we can reason about designs at an earlier stage in the design process. We explore using the Lean  theorem prover to build domain-specific languages for pipeline design, as well as  verify properties about memory consistency models and the existence of side channels. We also discuss language methods, for streamlining this process and improving proof automation.

Zoom access:     https://tu-dresden.zoom.us/j/66375953176?pwd=MlE2WEdrZlhBZGJZT0lOU0RRK1UzUT09

Meeting ID:         663 7595 3176

Passcode:            3HhBjt+j


Everbody welcome!

Go back