Marijn Heule

Marijn Heule is a Research Scientist at the University of Texas at Austin. He received his PhD at Delft University of Technology in the Netherlands in 2008. His research focusses on solving hard combinatorial problems in areas such as formal verification and number theory. Most of his contributions are related to practical satisfiability solving. He is one of the editors of the Handbook of Satisfiability and an associate editor of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT).

Clark Barrett

Clark Barrett is an Associate Professor of Computer Science at New York University. He received his PhD from Stanford University in 2003, advised by David Dill. His PhD thesis laid the groundwork for the architecture of modern Satisfiability Modulo Theories (SMT) solvers. He has written numerous articles on the subject and built several systems, the latest of which is CVC4. Professor Barrett was a founder of the SMT competition, and helps lead the SMT-LIB initiative, an effort to create standards and develop resources for the SMT community. He received the IBM Software Quality Innovation Award in 2008 for CVC3, and he was the recipient of the Haifa Verification Conference award in 2010 for his pioneering work in SMT.

Pascal Fontaine

Pascal Fontaine is maître de conférences in Nancy at the University of Lorraine and he is affiliated to Inria for his research. He obtained his PhD from the University of Liège, Belgium, in 2004, and works in Nancy since then. In his early days as a researcher, he was involved in the development of the haRVey SMT solver. Lateron he initiated, together with David Déharbe, the development of the veriT SMT solver. In 2006, proof production for SMT solvers and proof reconstruction from SMT proofs started to capture his interest, as necessary mechanisms to make SMT technologies available in other tools. He is also concerned with proof representation and proof compression.

Leonardo de Moura

Leonardo de Moura is a Principal Researcher in the RiSE group at Microsoft Research. He joined Microsoft in 2006, before that he was a Computer Scientist at SRI International. His research areas include automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is a new open source theorem prover being developed from scratch. Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. He received the Haifa Verification Conference Award in 2010. In 2014, the Z3 tool paper received "The most influential tool paper in the first 20 years of TACAS" award.

Break

Stephan Schulz

Stephan Schulz studied computer science at the University of Kaiserlautern.  Parts of his undergraduate work on proof extraction, structuring, and presentation for the distributed equational prover DISCOUNT have survived through Waldmeister and now migrated into Mathematica.

After graduation, he joined the Automated Reasoning Group at TU Munich. There he started the development of the well-known first-order theorem prover E. His PhD was awarded for research into using experience from previous proofs to learn heuristics for proof search in E.

Stephan spend time as Post-Doc and visiting lecturer at several universities and research institutes. He is now a professor at DHBW Stuttgart.

As part of this ongoing work, he cooperated with Geoff Sutcliffe, Koen Claessen, and Allen Van Gelder to define the TPTP-3/TSTP language for first-order proofs, and with Sutcliffe, Claessen and Peter Baumgartner to extend it to simply typed first-order logic.

E 1.8, the latest released version of the prover, implements not only TPTP-3 style proof output, but also a new method to produce these proofs with minimal overhead.

Christoph Benzmüller

In 2012, Christoph Benzmüller was awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG). In this position he is currently affiliated with Freie Universität Berlin, Germany, where he holds a venia legendi in Mathematics (and Computer Science). Previously, Christoph held positions as Full Professor for Artificial Intelligence and Formal Methods at the International University in Bruchsal, Germany, and as an Associate and Assistant Professor in Computer Science at Saarland University, Saarbrücken, Germany. Recently, Christoph received major international recognition for his research (jointly with Bruno Woltzenlogel-Paleo) on the formalization and automation of Kurt Gödel's ontological argument for the existence of God on the computer.

Christoph Benzmüller received his PhD (1999) and his Habilitation (2007) in Computer Science from Saarland University. His PhD, titled 'Equality and Extensionality in Higher-Order Theorem Proving', was supported by a grant of the 'Studienstiftung des Deutschen Volkes' and was partly conducted at Carnegie Mellon University, Pittsburgh, USA. Core research interests of Christoph include the theory, implementation, and application of reasoning systems for expressive logics, including classical and non-classical first-order and higher-order logics.

Break

Makarius Wenzel

Makarius Wenzel is, together with Tobias Nipkow and Lawrence Paulson, one of the principal developers of the Isabelle theorem prover. In particular he is responsible for the design of the Isar structured proof language and the recent PIDE (jedit) interface. He has also been instrumental (with David Matthews) in increasing parallelism in Isabelle, to the point where it really speeds up interactive work in practice. But he is involved in almost all other aspects of the tool.

Christine Paulin-Mohring

Christine Paulin-Mohring is a Professor at Université Paris-Sud 11 since 1997. She obtained her PhD in 1989 from Université Paris 7, working under the supervision of Gérard Huet at INRIA Rocquencourt and Ecole Normale Supérieure on the early version of the Calculus of Constructions. She spent 8 years as a CNRS Researcher at Ecole Normale Supérieure in Lyon, where she contributed to the development of the Coq proof assistant especially on the aspects concerning inductive definitions and program extraction. She lead the research group ProVal (INRIA Saclay - Île-de-France, Université Paris-Sud and CNRS) until 2011, working on the use of proof technologies for developing correct programs. Her recent work includes the development of a Coq library ALEA to reason on randomized programs.

Lunch

Dale Miller

Dale Miller received his PhD in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and a department head at Pennsylvania State University. He has held visiting positions at the universities of Aix-Marseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research at INRIA-Saclay where he is the Scientific Leader of the Parsifal team.

Miller is the editor-in-chief of the ACM Transactions on Computational Logic and is a member of editorial board of the Journal of Automated Reasoning. In 2014 he was a PC chair for CSL and LICS. In 2011 he was awarded an ERC Advanced Grant and the LICS Test-of-Time award for a 1991 paper he co-authored. Miller works on various topics in computational logic including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates.

Gilles Dowek

Gilles Dowek is a researcher at Inria in the Deducteam team. He is interested in the formalization of mathematics (type theory, set theory, nominal logics, etc.), in proof processing systems (proof-checking, automated theorem proving, etc.), in the design of quantum programming languages and in the safety of aerospace systems. He is also a consultant for the National Institute of Aerospace, a lab of the NASA Langley research center. Among other things, he has participated to the development and the proof of ACCoRD, an Airborne Coordinated Conflict Resolution and Detection system. In the past, he has been a professor at École Polytechnique. More generally, he is interested in education and he tries to draw the attention of the administration to the need of introducing computer science in K-12. Finally, he is also interested in the philosophy of sciences.

Alessio Guglielmi

Alessio Guglielmi is a proof theory researcher who teaches theoretical
computer science at the University of Bath. In the past he worked at INRIA and
Technische Universität Dresden, after obtaining a PhD in Pisa. His main
contribution is a methodology called deep inference. It consists in freely
composing proofs via logical connectives, so generalising Gentzen formalisms.
Deep inference allows us to deal with logics that escape Gentzen proof theory,
such as some modal and substructural logics, and to understand normalisation
as a more general and natural phenomenon than previously thought. Deep
inference also gives us access to much smaller analytic proofs than other
proof-theoretic methodologies do.

Break

Program Verification (B Method)
(paper, slides)

Jean-Raymond Abrial

Jean-Raymond Abrial is the co-inventor of various formal method approaches: Z, B and Event-B. He is the author of the "B-book" (CUP 1996), which presents the B-Method. He published recently a new book "Modeling in Event-B: System and Software Engineering" (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform tool for Event-B (funded by the European Project "Rodin"). After that, he was a researcher also at ETH Zurich, working on a new European Project called "Deploy" till May 2009. More recently, he is a consultant for another European Project: "Advance". He is also frequently invited in China giving some formal method courses in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world.

Gilles Barthe

Gilles Barthe is a professor at the IMDEA Software Institute since April 2008. His research interests include formal methods, programming languages and program verification, software and system security, and cryptography, and foundations of mathematics and computer science. Since 2006, he has been working on the development of formal verification tools for cryptography.

Alexander Leitsch

Alexander Leitsch is professor of Mathematics and Theoretical Computer Science at the Vienna University of Technology. In 1974 he obtained his PhD in mathematics at the University of Vienna (with a thesis on probability theory). In 1985 habilitation at the University if Linz with a thesis on recursion theory. In 1986/1987 visiting associate professor at the CIS department of the University of Delaware. Since 1987 full professor at the Vienna University of Technology. In 2001 guest researcher at the CNRS in Grenoble (rank: directeur de recherche) for three months. Member of the editorial board of Studia Logica, program co-chair of IJCAR in 2001. Research interests are computational proof theory and automated deduction. Books: The Resolution Calculus (1997), Automated Model Building (2004, with R. Caferra and N. Peltier), Methods of Cut-Elimination (2011, with M. Baaz).