December 11-13, 2020
Martin Nyx Brain is a lecturer at City, University of London and a senior research fellow at University of Oxford. His work is broadly within the areas of automated reasoning and automated verification of software for safety and security. On the automated reasoning side he mostly works on SAT / SMT solvers, including being the co-author of the SMT-LIB theory of floating-point and developing the CVC4 floating-point theory solver. In automated verification he mainly focuses on low-level and embedded software in C, C++ and Ada using a combination of abstract interpretation, symbolic execution and deductive verification and tools including SPARK and CBMC / CPROVER.
Guy Katz is an assistant professor at the Hebrew University of Jerusalem, Israel. He received his Ph.D. at the Weizmann Institute of Science in 2015. His research interests lie at the intersection between Formal Methods and Software Engineering, and in particular in the application of formal methods to software systems with components generated via machine learning.
Since 2004 Prof. Armin Biere is a Full Professor for Computer Science at the Johannes Kepler University in Linz, Austria, and chairs the Institute for Formal Models and Verification. 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. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques. His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 57 medals including 32 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential in the first 20 years of TACAS in 2014, and the ETAPS 2017 Test of Time Award.