Invited Presenters

Daniel Le Berre

University of Artois Jean Perrin Faculty of Sciences

Brief Bio

Daniel Le Berre conducts research in the field of artificial intelligence and is particularly interested in the design and evaluation of algorithms for inference and decision-making. He is also passionate about software engineering, which he teaches at the University of Artois. Mobilizing the two facets of his job as a teacher-researcher, Daniel Le Berre studies the practical resolution of problems specific to software engineering. It uses Boolean constraint-based approaches to address dependency management, software product lines, and automatic hotfix summarization.Some of his contributions are Sat4j, which offers a set of reasoning tools in Boolean variables for the Java language, which also integrates consortium ObjectWeb (now OW2), which promotes the development of free middleware, and has emerged as one of the software flagship consortium. All applications based on Eclipse benefit from the integration of the software of Daniel Le Berre.

Mate Soos

School of Computing, National University of Singapore.

Brief Bio

Mate Soos obtained his MsC in BUTE, Hungary, in IT Security and wrote his PhD in INRIA, Grenoble on Privacy-preserving RFIDs. During this time he has started writing the SAT solver CryptoMiniSat that has since won many awards, most recently it ranked the first in the 2016 and 2015 incremental SAT solving competitions. Mate has worked in the IT security industry for many years while maintaining and building (i) CyrptoMiniSat, a SAT solver, (ii) STP, an SMT solver, and (iii) ApproxMC, Approximate Model Counter, all of which are extensively used in both industry and academia.

R Venkatesh

TCS Research, Pune, India

Scaling up SAT+SMT to Industry Problems

Brief Bio

R. Venkatesh is a chief scientist with TCS Research and heads its Verification and Validation Program. He has been with TCS for more than 25 years primarily in the areas of software development, formal methods and verification. During this tenure he has lead several tool development projects including TCS ECA a static analysis tool that is sold commercially by TCS. Other tools include MasterCraft and more recently a formal specification notation EDT.

Sanjit A. Seshia

University of California, Berkeley

UCLID5- Integrating Modeling, Verification, Synthesis, and Learning

Brief Bio

Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, and the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award. He is a Fellow of the IEEE.

© 2019 SAT+SMT School