Members
Armin Biere (fmv.jku.at)
Since 2004 Prof. Armin Biere chairs the Institute for Formal Models and
Verification at the Johannes Kepler University in Linz, Austria.
Between 2000 and 2004 he held a position as Assistant Professor within the
Department of Computer Science at ETH Zürich, Switzerland. In 1999 Biere was
working for a start-up company in electronic design automation after one year
as Post-Doc with Edmund Clarke at CMU, Pittsburgh, USA. In 1997 Biere received
a Ph.D. in Computer Science from the University of Karlsruhe, Germany.
Armin Biere is co-inventor of Bounded Model Checking (BMC), which is in
widespread use in industry. He worked on decision procedures for SAT, QBF, and
SMT and implementations of his group rank at the top in many competitions. He
has more than 60 publications, was on the PC of more than 45 international
workshops and conferences, was co-chair of SAT'06 and FMCAD'09, is one of the
editors of the Handbook of Satisfiability, and organizes the Hardware Model
Checking Competition.
Roderick Bloem (iaik.tugraz.at)
Roderick Bloem received his M.Sc. degree in computer science from Leiden University, The Netherlands, in 1996 and his Ph.D. degree in computer science from the University of Colorado, Boulder, in 2001. From 2002 until 2008, he was an Assistant with Graz University of Technology, Graz, Austria. From 2008, he has been a professor of Computer Science at the same university. His research interests is in rigorous methods for systems engineering, including formal verification, fault localization and correction, automatic synthesis of systems from their specifications, and trusted computing. Roderick Bloem has published over three dozen papers at international conferences and journals. He serves on various program committees and has organized the 2009 ACM/IEEE Conference on Methods and Models for Codesign and the 2010 International Conference on Formal Methods for Computer Aided Design.
Krishnendu Chatterjee (ist.ac.at)
Krishnendu Chatterjee received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kharagpur in 2001 and the MS and Ph.D. degree in Computer Science from the University of California at Berkeley in 2004 and 2007, respectively. Since 2009, he has been an Assistant Professor in IST Austria (Institute of Science and Technology Austria). His research interests are in the verification and control of reactive and probabilistic systems, game theoretic problems in verification, logic, and automata theory. Dr. Chatterjee received the President’s Gold Medal from IIT, Kharagpur, the David Sakrison memorial award from UC Berkeley, and the Ackermann award from European Association in Computer Science Logic.
Uwe Egly (kr.tuwien.ac.at)
Uwe Egly is an associate professor and currently vice-dean for academic affairs at TU Wien. He holds a Dipl. Inform. med. degree from Heidelberg University and a Dipl.-Ing. degree from TU Wien In 1994, he got his doctoral degree from TH Darmstadt and obtained his habilitation from TU Wien in 1997. His research interests are in proof theory and proof complexity, knowledge representation and reasoning, computational logic, satisfiability checking for QBFs, argumentation and argumentation frameworks, algorithms for pathplanning, and applications of AI methods in engineering.
Thomas A. Henzinger (ist.ac.at)
Thomas A. Henzinger is President of IST Austria (Institute of Science and Technology Austria) and Adjunct Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, and a Ph.D. degree in Computer Science from Stanford University (1991). He was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98), and Professor (1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbrücken, Germany (1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-09). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is an ISI highly cited researcher, a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a corresponding member of the Austrian Academy of Sciences, a Fellow of the ACM, and a Fellow of the IEEE.
Christoph Kirsch (cs.uni-salzburg.at)
Christoph Kirsch is full professor and holds a chair at the Department of Computer Sciences of the University of Salzburg, Austria. He received his Dr.Ing. degree from Saarland University, Saarbrücken, Germany, in 1999 while at the Max Planck Institute for Computer Science. From 1999 to 2004 he worked as Postdoctoral Researcher at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. His research interests are in concurrent programming and systems, virtual execution environments, and embedded software. Dr. Kirsch co-invented the Giotto and HTL languages, and leads the JAviator UAV project for which he received an IBM faculty award in 2007. He co-founded the International Conference on Embedded Software (EMSOFT) in 2001 and is currently vice-chair of ACM SIGBED. He has been PC co-chair of EMSOFT 2007, general co-chair of ESWEEK 2008, general chair of LCTES 2009, topic co-chair at DATE 2010, and is track chair at RTSS 2010. He is also general chair of EuroSys 2011. He has been invited to serve on program committees of CASE, Coordination, DATE, EMSOFT, EUC, EuroSys, HSCC, ICCAD, JTRES, LCTES, MEMOCODE, OOPSLA, RTAS, RTSS, and VEE.
Laura Kovács (complang.tuwien.ac.at)
Laura Kovács is an FWF Hertha Firnberg Research Fellow at the Institute of Computer Languages of the Vienna University of Technology (TU Wien). Her research deals with the design and development of new theories, technologies, and tools for program verification, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She holds an MSc from the Western University of Timisoara, Romania, and a PhD degree from the Research Institute for Symbolic Computation of the Johannes Kepler University, Linz, Austria. Before joining TU Wien, she was a postdoctoral researcher in the Models and Theory of Computation research group of Prof. Dr. Thomas A. Henzinger at the Swiss Federal Institute of Technology Lausanne (EPFL), and at the Programming Methodology research group of Prof. Dr. Peter Müller at the Swiss Federal Institute of Technology Zürich (ETH).
Ulrich Schmid (ti.tuwien.ac.at)
Ulrich Schmid received his diploma (1985) and Dr.techn. degree (1986) from the Technische Universität Wien (computer science and mathematics). He is now full professor and head of the Embedded Computing Systems Group at TU Vienna's Institut für Technische Informatik. Ulrich Schmid authored and co-authored numerous papers in the field of theoretical and technical computer science and received several awards and prices, like the Austrian START-price 1996. He also spent several years in industrial electronics and embedded systems design. His current research interests focus on the mathematical analysis of fault-tolerant distributed algorithms and real-time systems, with special emphasis on their application in systems-on-chips and networked embedded systems. Ulrich Schmid is member of IEEE Computer Society and EATCS.
Helmut Veith (forsyte.tuwien.ac.at)
Helmut Veith is full professor and head of the Formal Methods in Systems Engineering Group (FORSYTE) at TU Wien (2009-), and an adjunct professor at Carnegie Mellon University (2005-). He holds a diploma in Computational Logic (1994) and a PhD sub auspiciis praesidentis (1998) in Computer Science, both from TU Wien. Prior to his appointment to Vienna, he was holding professor positions in Germany at TU Darmstadt (2008-2009) and TU Munich (2003-2008), and as an associate professor at TU Wien (2000-2003). In 1999-2000, he was a Max Kade fellow in the group of Ed Clarke at Carnegie Mellon University. Helmut Veith was a co-developer of Counterexample-Guided Abstraction Refinement (CEGAR) which has become a central method for software verification; subsequent work on software verification has received an ACM SIGSOFT distinguished paper award. Helmut Veith has been an editor of the LNCS 5000 volume "25 Years of Model Checking", is a co-editor (with Edmund Clarke and Tom Henzinger) of the forthcoming Handbook of Model Checking, and a program chair of LPAR 2008 and CSL 2010. He was an invited speaker at CSL, LPAR, Haifa Verification Conference, Forum Alpbach and other conferences. Helmut Veith has published over 60 papers in model checking, software engineering, computer security and computational logic. His current work is focusing on model checking, software verification and testing, embedded software and computer security.