University of Artois Jean Perrin Faculty of Sciences
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.
School of Computing, National University of Singapore.
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.
TCS Research, Pune, India
Scaling up SAT+SMT to Industry Problems
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.
University of California, Berkeley
UCLID5- Integrating Modeling, Verification, Synthesis, and Learning
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.
Validating optimizations of concurrent C/C++ programs.
Soham Chakraborty is an Assistant Professor at the Department of Computer Science and Engineering, IIT Delhi. He has obtained his PhD from the Max Planck Institute for Software Systems (MPI-SWS), Germany in 2019 and MS from the Department of Computer Science and Engineering, IIT Kharagpur in 2008. He has worked in various industrial research positions for 5 years before starting PhD. He works in the area of Programming Languages and Software Engineering. His specific research interests lie in relaxed memory concurrency, compiler correctness, and related topics.