Lecturers

MPB-Torino2011.10.4Maria Paola Bonacina (Università degli Studi di Verona, Italy)

Maria Paola Bonacina is a Professor of Computer Science at the Università degli Studi di Verona, on sabbatical at SRI International. Earlier she was on the faculty of the Department of Computer Science of the University of Iowa. Her research area is artificial intelligence and computational logic, where she works in automated reasoning, including theorem proving, model building, decision procedures for satisfiability, reasoning for analysis, verification, synthesis of systems, strategy analysis, distributed deduction, and rewriting. She is the President of the Board of Trustees of the Conference in Automated Deduction (CADE). Maria Paola did her postdoc at INRIA Lorraine and at the Argonne National Laboratory; received a PhD from the State University of New York at Stony Brook, and a Doctorate and a Laurea from the Università degli Studi di Milano.

supratik3Supratik Chakraborty (IIT Bombay, India)

Supratik Chakraborty is currently Bajaj Group Chair Professor in the Department of Computer Science and Engineering at Indian Institute of Technology (IIT) Bombay, India.  He is also a principal investigator in the Center for Formal Design and Verification of Software at IIT Bombay.  He received a B.Tech. (Honours) in Computer Science and Engineering from IIT Kharagpur, and an M.S. and Ph.D. in Electrical Engineering (Computer Systems) from Stanford University.  From 1998 to 1999, he served as a Member of Research Staff at Fujitsu Laboratories of America.
Supratik’s current research interests include formal methods, with an emphasis on scalable algorithmic techniques for formally analyzing hardware, software and biological systems.  He also works on approximate techniques for sampling and counting with rigorous approximation guarantees.  Besides several conference and journal papers, he has authored a book chapter on analyzing heap manipulating programs using automata techniques.  Another book on algorithms for automata on infinite words is currently under preparation. Supratik serves on the Technical Advisory Board of Microsoft Research India, and on the Council of Indian Association for Research in Computing Science (IARCS).

dejanDejan Jovanović (SRI International, USA)

Dejan Jovanović is a computer scientist in the Computer Science Laboratory at SRI International. His research interests are automated reasoning, satisfiability, and model-checking. He is involved in development of Yices2 and CVC4 SMT solvers. He received his Ph.D. degree in computer science from New York University.

jarvisaloMatti Järvisalo (University of Helsinki, Finland)

Matti Järvisalo is academy research fellow and adjunct professor at the Department of Computer Science, University of Helsinki, Finland, where he leads the Constraint Reasoning and Optimization group. His research record lists over 60 refereed publications with a main focus on theoretical and algorithmic aspects of Boolean satisfiability (SAT) and optimization, and applications of SAT-based techniques in solving various hard search and optimization problems in AI. He has received several best paper award recognitions, and SAT-based systems arising from his research have reached top positions at multiple solver competition (including MaxSAT Evaluation 2015 and the first ICCMA argumentation solver competition). He has served as program chair for the International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) and is current member of the steering committee of the SAT conference series.

marius_smallMarius Lindauer (University of Freiburg, Germany)

Marius Lindauer is a postdoctoral research fellow in the Machine Learning for Automated Algorithm Design (ML4AAD) group at the University of Freiburg (Germany). He works on algorithm configuration and selection using cutting-edge techniques from machine learning and optimization to improve the performance of arbitrary algorithms, including SAT and MIP solvers, but also machine learning algorithms. Marius Lindauer received his PhD at the University of Potsdam, working in the Potassco Group, and is a co-founder of the international research group on COnfiguration and SElection of ALgorithms (COSEAL).

lonsing-bw-portraitFlorian Lonsing (TU Vienna, Austria)

Florian Lonsing is a post-doctoral researcher in the Knowledge-Based Systems Group (KBS) at Vienna University of Technology, Austria, which he joined in 2012. His position is part of the Austrian-wide RiSE/SHiNE research project funded by the Austrian Science Fund (FWF). Florian Lonsing studied computer science at Johannes Kepler University (JKU), Linz, Austria (PhD 2012) and was a research and teaching assistant at the Institute for Formal Models and Verification at JKU from 2008 to 2012. His current research activities focus on decision procedures for quantified Boolean formulas (QBF) and related theoretical and practical aspects, e.g., approaches to automated testing and debugging of solvers, incremental solving, and experimental evaluation. He has been developing the state of the art QBF solver DepQBF, which achieved top rankings in several QBF solver competitions.

Nuno LopesNuno P. Lopes (Microsoft Research Cambridge, UK)

Nuno Lopes is a researcher at MSR Cambridge.  He holds a PhD from the University of Lisbon, and has previously interned at MSR Redmond, Apple’s compiler team, Max Planck Institute (MPI-SWS), and the Institute for Systems and Robotics Lisbon. Nuno’s research interests include software verification, compilers, and mixing the two.

JakobCSAILOkt09Jakob Nordström (KTH Royal Institute of Technology, Sweden)

Jakob Nordström received his Master of Science in Computer Science and Mathematics at Stockholm University in 2001, and his PhD in Computer Science at KTH Royal Institute of Technology in 2008. During the academic years 2008-09 and 2009-10, he was a postdoctoral researcher at the Massachusetts Institute of Technology (MIT). Since 2011 he is working at the School of Computer Science and Communication at KTH, where he became an Associate Professor and received his Docent degree (habilitation) in 2015.
In 2006 he received the best student paper award at 38th ACM Symposium on Theory of Computing (STOC ’06), and his PhD thesis received the Ackermann Award 2009 for “outstanding dissertations in Logic in Computer Science” from the European Association for Computer Science Logic. His research is funded by a Starting Independent Researcher Grant from the European Research Council (2011) and by a Breakthrough Research Grant from the Swedish Research Council (2012).
In 1997-1998, Jakob Nordström served as a military interpreter at the Swedish Armed Forces Language Institute (Försvarets tolkskola), graduating as the best student of the 1998 class. In parallel with his studies and later his research, he has worked as a Russian interpreter, engaged among others for His Majesty the King of Sweden and the Swedish Prime Minister. He also has a Diploma in Choir Conducting with extended Music Theory from the Tallinn Music Upper Secondary School, Estonia. During the period 1994-1999, he was the artistic director of Collegium Vocale Stockholm, a vocal ensemble performing mainly Renaissance and Baroque music.

ajr-2014Andrew Reynolds (University of Iowa, USA)

Andrew Reynolds is a research scientist at the University of Iowa and an active developer of the Satisfiability Modulo Theories (SMT) solver CVC4. His received his doctorate at the University of Iowa under the supervision of Cesare Tinelli, and did a postdoc at Ecole Polytechnique Federale de Lausanne (EPFL) in Switzerland. His research interests are in various aspects of SMT, including decision procedures, proofs, and quantifiers. For the latter, he has developed a variety of techniques for quantifiers in SMT, including conflict-based instantiation, techniques for automating induction and function synthesis, and finite model finding.

jpms05João Marques Silva (University of Lisbon, Portugal)

João Marques-Silva holds a PhD degree from the University of Michigan, Ann Arbor, USA, in 1995, and the Habiliation degree in Computer Science from the Technical University of Lisbon, Portugal, in 2004. Currently, he is Professor of Computer Science, Faculty of Science, University of Lisbon. He has also been affiliated with University College Dublin, Ireland, University of Southampton, United Kingdom, and Instituto Superior Tecnico, Lisbon, Portugal. His research interests includ decision and function procedures, analysis of over-constrained systems, and applications in artificial intelligence, formal methods and software engineering. He received the 2009 CAV award for fundamental contributions to SAT solvers.

Laurent-SimonLaurent Simon (Bordeaux Computer Science Laboratory (Labri) and Bordeaux Institute of Technology, France)

Laurent Simon is one of the authors of Glucose, an award winning SAT solver designed on the top of Minisat. He is one of the organizers of the SAT competitions from 2002 to 2009. He was the co-chair of SAT 2011 and is the local chair of SAT 2016 (in Bordeaux).
Laurent Simon holds a Professor position at the LaBRi, University of Bordeaux – Bordeaux INP.

cw2Christoph Weidenbach (Max-Planck-Institut für Informatik, Germany)

Christoph Weidenbach is Senior Researcher and Group Leader at the Max Planck Institute for Informatics. He holds a PhD from Saarland University (1996), and received his Habilitation from the same university in 2000. Further stages of his career include:
1991-1999: Researcher at the Max Planck Institute for Informatics
Since 1994: Head of the SPASS theorem prover/workbench team
1999-2005: IT Manager, GM Powertrain Europe
Since 2005: Senior Researcher, Independent Group Leader, Max Planck Institute for Informatics
Since 2007: Adjunct Professor, Saarland University
2012: Foundation of the Startup L4B

thwiesThomas Wies (New York University, USA)

Thomas Wies is an Assistant Professor at New York University and a member of the Analysis of Computer Systems Group in the Courant Institute of Mathematical Sciences. He received his doctorate in Computer Science from the University of Freiburg, Germany (2009). Before joining NYU, he held post-doctoral positions at École Polytechnique Fédérale de Lausanne and at the Institute of Science and Technology Austria. His research focuses on formal methods, programming languages, and automated reasoning. He has received an NSF CAREER Award, a Microsoft European PhD Fellowship, and an OOPSLA Best Paper Award.