Principal Investigators

arise-cropped

eziobartocci
Ezio Bartocci is an Assistant Professor at the Faculty of Informatics, Cyber-Physical Systems Group at the Vienna University of Technology. The primary focus of his research is to develop formal and computational methods, tools and techniques which support the modeling and automated analysis of complex computational systems, including software systems, embedded systems and biological systems.

Previously he was a post-doctoral researcher at the Department of Computer Science (Research Scientist – from March 2011) and at the Department of Applied Math and Statistics (Research Associate – from February 2010) of the State University of New York at Stony Brook, working with Prof. James Glimm, Prof. Radu Grosu and Prof. Scott. A. Smolka. His research area, in the framework of the NSF Expeditions in Computing project CMACS, was the Computational Modelling and Analysis of Cardiac Dynamics for Prediction and Control of Cardiac Arrhythmia. He received the B.S. degree in Computer Science and the M.S. degree in Bioinformatics from the University of Camerino in Italy, in 2002 and 2005, respectively. During my M.S. degree in Bioinformatics he won a scholarship (from June 2003 to Feb 2004) funded by the MIUR project Oncology Over Internet (O2I). In 2009 he got a Ph.D. in Information Science and Complex Systems from the University of Camerino, under the supervision of Prof. Flavio Corradini. In 2014 he earned the National Italian Habilitation as Associate Professor in Computer Science by the Italian Ministry of Education, Universities and Research.

He also co-chaired several international events, such as HSB 2012, the First International Workshop on Hybrid Systems and Biology, SPIN 2013, the 20th Intern. Symposium on Model Checking Software, the CSRV-2014, the First Intl. Competition of Software Runtime Verification in Canada, the Medical CPS track at Isola 2014 and in 2015 he will co-chair in Vienna the 15th Intl. Conference on Runtime Verification.

Website

Armin BiereSince 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.

Website

Roderick BloemRoderick 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.

Website

Krishnendu ChatterjeeKrishnendu 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.

Website

Uwe EglyUwe 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.

Website

radu
Radu Grosu is a Full Professor, and the Head of the Institute of Computer Engineering, at the Faculty of Informatics, of the Vienna University of Technology.
Grosu is also the Head of the Cyber-Physical-Systems Group within the Institute of Computer-Engineering, and a Research Professor at the Department of Computer Science, of the State University of New York at Stony Brook, USA.
The research interests of Radu Grosu include the modeling, the analysis and the control of cyber-physical systems and of biological systems.

The applications focus of Radu Grosu includes distributed automotive and avionic systems, autonomous mobility, green operating systems, mobile ad-hoc networks, cardiac-cell networks, and genetic regulatory networks.
Radu Grosu is the recipient of the National Science Foundation Career Award, the State University of New York Research Foundation Promising Inventor Award, the Association for Computing Machinery Service Award, and is an elected member of the International Federation for Information Processing, Working Group 2.2.
Before receiving his appointment at the Vienna University of Technology, Radu Grosu was an Associate Professor in the Department of Computer Science, of the State University of New York at Stony Brook, where he co- directed the Concurrent-Systems Laboratory and co-founded the Systems-Biology Laboratory.

Radu Grosu earned his doctorate (Dr.rer.nat.) in Computer Science from the Faculty of Informatics of the Technical University München, Germany. He was subsequently a Research Associate in the Department of Computer and Information Science, of the University of Pennsylvania, USA, and an Assistant Professor in the Department of Computer Science, of the State University of New York at Stony Brook, USA.
Website

Thomas A. HenzingerThomas 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 KirschChristoph 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.

Website

Laura KovácsSince April 2016, Laura Kovács Laura Kovacs is a full professor of computer science at the Vienna University of Technology (TU Wien).
She also holds a part-time associate professorship at the Chalmers University of Technology, Sweden.
Her research deals with the design and development of new theories, technologies, and tools for program analysis, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theorem prover. In 2014, she received the prestigious Wallenberg Academy Fellowship and an ERC Starting Grant. 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. After her PhD studies, from 2007 to 2010 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). From 2010 to 2013, she was a FWF Hertha Firnberg Research Fellow and an assistant professor at the Institute of Computer Languages of the TU Wien. Since 2012, she holds a habilitation degree in computer science from the TU Wien.
Website

Ulrich SchmidUlrich 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.

MS_farbe
Martina Seidl is an Assistant Professor at the Institute for Formal Models
and Verification at the Johannes Kepler University Linz. Further, she
is research associate of the Business Informatics Group at the Vienna
University of Technology, from which she also received her PhD in 2007.
Her research interests include various aspects of automated reasoning
and verification techniques based on SAT and QBF as well as topics of
model-based development like the evolution of software models.
She is co-organizer of the TAP 2014 conference, the QBF 2014 workshop,
as well as the QBF Gallery 2014, the competition for QBF solvers.

Website

 
 
 

ana
Ana Sokolova is an Assistant Professor (tenure track) at the Department of Computer Sciences, University of Salzburg. Her research deals with concurrency, (relaxations of) semantics of concurrent objects, probabilistic systems, and coalgebras. She holds an MSc from the St.Cyril and Methodius University in Skopje, Macedonia, and PhD from Eindhoven University of Technology, The Netherlands. Before her current position, she was a postdoctoral researcher with Prof. Bart Jacobs at the Radboud University Nijmegen, a postdoctoral researcher with Prof. Christoph Kirsch at the University of Salzburg, and an Elise Richter Research Fellow.

Website

Helmut Veith Helmut Veith is a professor of Computer Science at Vienna University of Technology, Austria, and an Adjunct Professor at Carnegie Mellon University, Pittsburgh. Prior to his appointment in Vienna, he had professor positions at TU Darmstadt (2008-2009) and TU Munich (2003-2008). He is the speaker of the Doctoral College “Logical Methods in Computer Science”, and vice-speaker of the Austrian research network “Rigorous Systems Engineering”. Veith is a coeditor of the forthcoming Handbook of Model Checking, PC co-chair of LPAR 2008, CSL 2010, CAV 2013, and FMCAD 2015, and co-chair of the Vienna Summer of Logic 2014, the largest conference in the history of logic. He
has published more than 100 papers in computer-aided verification, software engineering, computer security, and logic in computer science. He is best known for his role in the development of Counterexample-guided Abstraction Refinement (CEGAR) which is a key ingredient in modern model checkers for software and hardware. His awards include a PhD award sub auspiciis praesidentis by the Austrian president, and an ACM Distinguished Paper Award for work on the software model checker MAGIC.

Website

georg Georg Weissenbacher is currently a tenure-track assistant professor in the Formal Methods group at the Institute for Information Systems of Vienna University of Technology. He is leading a WWTF-funded Vienna Research Group for Young Investigators.
Until recently, Georg worked as a postdoctoral research associate in Prof Sharad Malik’s group at the department of electrical engineering of Princeton University.
He received a Diploma from Graz University of Technology in Austria, started my doctoral studies at ETH Zurich (Switzerland) and completed my DPhil in computer science at the University of Oxford in 2010 (under the supervision of Dr Daniel Kröning). His dissertation is concerned with the automated verification of software. His doctoral studies were generously supported through a Microsoft European PhD scholarship.
While pursuing his degree, Georg gained practical experience working as a software developer at the Austrian companies Joanneum Research and HS-Art. He interned at the Danish company IFAD, and at Microsoft Research Redmond (WA) and Cambridge (UK). After his undergraduate studies, Georg spent one year at the Austrian Research Centers in Vienna as a software engineer.
His research interests are automated formal verification techniques, static analysis, and decision procedures. He is the co-author of over a dozen peer reviewed papers on these topics.
Georg enjoys teaching and assists courses since his undergraduate studies. He has recently taught a course on formal verification at Princeton University. He also co-authored a textbook on digital circuit design.
Website

 

zuleger
Florian Zuleger is an assistant professor at the Technical University of Vienna, where he obtained his PhD under the supervision of Helmut Veith. He is interested in static and dynamic approaches to program analysis and in applying automata theory and logic to verification. His current research focuses on termination and bound analysis, shape analysis, and automated grading for online courses.

Website