Speakers


The confirmed speakers are as follows.

SAT Day (3rd July)

Gilles Audemard, Université d’Artois
Gilles Audemard is a professor in the Artois University, located in the north of France. His researches focusses on satisfiabilty, quantified boolean formulas, SAT based problems and constraint satisfaction problems. He is an author of the Glucose SAT solver.
Armin Biere, Johannes Kepler University
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. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques. He is the author and co-author of more than 180 papers. 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 67 medals including 37 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, the HVC’15 award on the most influential work in the last five years in formal verification, simulation, and testing, and the ETAPS 2017 Test of Time Award.
Marijn Heule, University of Texas at Austin
Marijn Heule is a Research Assistant Professor at the University of Texas at Austin who received his PhD at Delft University of Technology (2008). His contributions to SAT solving have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof-producing techniques are used in many state-of-the-art solvers. Dr. Heule is one of the editors of the Handbook of Satisfiability and co-organized the SAT competitions in recent years. Four of his recent publications were awarded best paper at the SAT, TACAS, CADE, and HVC conferences.

SMT Day (4th July)

Alberto Griggio, FBK-IRST
Alberto Griggio is a Researcher at Fondazione Bruno Kessler (FBK). His current research interests include formal methods, SAT, SMT, model checking and safety assessment of both finite and infinite-state systems. He develops the MathSAT 5 SMT solver and is a contributor to the nuXmv symbolic model checker.
Pascal Fontaine, Université de Lorraine
Pascal Fontaine is an assistant professor (maître de conférence) at Université de Lorraine, Nancy (France) and conducts research within the INRIA group VeriDis, a joint team at LORIA and Max-Planck-Institut für Informatik, Saarbrücken. He is a contributor to the the veriT SMT solver.
Aina Niemetz, Stanford University
Aina Niemetz is a researcher at Stanford University. She is one of the developers and maintainers of the SMT solver Boolector and is currently working on the SMT solver CVC4. Her research focus is on various aspects of Satisfiability Modulo Theories (SMT), in particular procedures for bit-vectors, arrays and uninterpreted functions.
Mathias Preiner, Stanford University
Mathias Preiner is a researcher at Stanford University. He is one of the developers and maintainers of the SMT solver Boolector and is currently working on the SMT solver CVC4. His current research interests include (incremental) solving techniques for bit-vectors, arrays and lambdas in the context of Satisfiability Modulo Theories (SMT).
Martin Brain, University of Oxford
Martin Nyx Brain is a project lead at University of Oxford. He designs, develops and deploys a range of program analysis and SMT based tools and technologies for companies such Altran, Toyota, BTC and DSTL using CVC4 and CPROVER. People have kindly referred to him as “knowing a thing or two about reasoning about floating-point using SMT” and when he gets time he attempts to arrange mathematics to understand where difficulty in SMT problems comes from.

Automated Reasoning Day (5th July)

Uwe Waldmann, MPI Saarbrücken
Uwe Waldmann is a researcher at Max Planck Institute for Informatics in Saarbrücken. He obtained his Ph.D. from Saarland University in 1997. His research focuses on various aspects of automated theorem proving and verification. In particular, he is working on combinations and extensions of saturation-based first-order proof calculi and other deductive systems. Uwe Waldmann received a test-of-time award at LICS and two teaching awards from the CS Department of Saarland University.
Stephan Schulz, DHBW Stuttgart
Stephan Schulz is a professor of computer science at DHBW Stuttgart. He is teaching logic and foundational topics of computer science. Among his particular interests are efficient implementations of automated reasoning systems and intelligent search control for automatic theorem provers. His long-term vision is the integration of high-performance inference machines and machine-learning techniques to realise a system that can robustly reason in a wide variety of domains. He is at primary developer of the theorem prover E.
Laura Kovacs, Vienna University of Technology (TU Wien)
Laura Kovács is a full professor at the Faculty of Informatics of Vienna University of Technology (TU Wien). She also holds a part-time professor position at the Department of Computer Science and Engineering of the Chalmers University of Technology. In her research, Laura Kovács 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 a co-developer of the Vampire theorem prover. In 2014, she received the Wallenberg Academy Fellowship and an ERC Starting Grant.
Martin Suda, Vienna University of Technology (TU Wien)
Martin Suda is a postdoc in the group of Laura Kovács at the Vienna University of Technology, Austria. Before coming to Vienna, he was a postdoc at Andrei Voronkov’s group at the University of Manchester. As one of the main developers of Vampire, he recently contributed to extensions of the AVATAR architecture, new clausification algorithms and preprocessing techniques, and the support for interpolation. Besides automated theorem proving, his research interest include temporal reasoning, automated planning and QBF proof theory.

Computer Algebra and Applications Day (6th July)

Matthew England, Coventry University
Matthew England is a Senior Lecturer in Computer Science at Coventry University, UK. His research is in the field of Computer Algebra and Symbolic Computation, in particular Cylindrical Algebraic Decomposition (CAD): a key procedure for quantifier elimination and other problems in non-linear real arithmetic. Recent work includes: adaptations the core CAD algorithm to take advantage of the logical structure in problems; optimisations to the algorithm via man made and machine learned heuristics; and applications in bio-chemical systems, economic reasoning and computation with multi-valued functions.
John Abbott, Università degli Studi di Genova
John Abbott is a researcher at Università degli Studi di Genova (Italy). His work interests include several areas of computer algebra including Groebner bases, modular methods, and polynomial factorization. He is the main developer of the software library CoCoALib, and the system CoCoA-5.
Arie Gurfinkel, University of Waterloo
Arie Gurfinkel is an Associate Professor in the department of Electrical and Computer Engineering with a cross appointment at the Cheriton School of Computer Science at the University of Waterloo. The goal of his research is to help developing, testing, and verifying complex computer systems through automation. His primary focus areas are Automated Program Analysis, Software Model Checking, Automated Reasoning, and Abstract Interpretation.
Philipp Rümmer, Uppsala University
Philipp Rümmer is researcher at Uppsala University, Sweden. His interests include various forms of program verification, deductive verification and model checking, as well as underlying techniques such as theorem proving and SMT.