CS Department Seminar: Alexander Malkis, (Madrid Institute of Advanced Studies in Software Development Technologies)
March 5, 2012
Title: Verification of Software Barriers
Speaker: Alexander Malkis (Madrid Institute of Advanced Studies in Software Development Technologies) (http://software.imdea.org/people/alexander.malkis/)
Location: Babbio 321
We describe frontiers in verification of the software barrier synchronization primitive. So far most software barrier algorithms have not been mechanically verified. We show preliminary results in automatically proving the correctness of the major software barriers.
Alexander has obtained his Diploma degree from the University of Saarland, Germany, in 2004-2005, for a work on polyedges (= bond animals) under Raimund Seidel. He continued his studies in Saarbrücken and Freiburg, obtaining his PhD thesis in 2010 at the University of Freiburg for a work on verification of multithreaded programs under Andreas Podelski. Directly afterwards he joined IMDEA Software. His current interests are thread-modular reasoning, abstract interpretation for multithreaded programs, and the verification of synchronization primitives.