SMTLIB initiative

SMT-LIB is an international initiative aimed at facilitating research and development in Satisfiability Modulo Theories. Since its inception, the initiative has pursued these aims by focusing on the following concrete goals: provide standard rigorous descriptions of background theories used in SMT systems; (ii) develop and promote common input and output languages for SMT solvers; (iii) establish and make available to the research community a large library of benchmarks for SMT solvers. This talk will give an overview of SMT-LIB and its standards, and present some of the resources it provides.

Cesare Tinelli, University of Iowa, Iowa City, USA and David Cok, Grammatech.

Cesare Tinelli is an associate professor of Computer Science at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, software verification, foundations of programming languages, and applications of logic in computer science.
His research has been funded by the US National Science Foundation, the US Air Force Office of Scientific Research, and Intel Corp., and has appeared in more than 40 refereed publications, including articles in such journal as Artificial Intelligence, Information and Computation, the Journal of the ACM, Logical Methods in Computer Science, and Theoretical Computer Science.
He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers. He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, and a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community. He has given invited talks at such conferences as CAV, HVC, TABLEAUX, VERIFY, and WoLLIC. He is an associate editor of the Journal of Automated Reasoning. He founded the SMT workshop series and has served in the program committee of numerous automated reasoning conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He was the PC chair of FroCoS'11.

David Cok is a researcher and project leader in static analysis, software development, computational science and digital imaging. He is currently Associate Vice President for Technology at GrammaTech, Inc., a company that has been researching and creating static analysis tools since 1988. At GrammaTech, he is building on his experience in internal and commercial software development and research accomplishments in static analysis and software verification and has led the proposal and execution of a number of research contracts. He has also been a major contributor to the collaborative academic research tools jSMTLIB, JML, OpenJML, and Esc/Java2. His particular interests are the usability and application of static analysis and verification technology for industrial-scale software development. Prior to GrammaTech, Cok was a Research Fellow in the Kodak Research Laboratory and held several technical leadership positions at Kodak; he worked in digital imaging and applications of machine learning and automated reasoning at Kodak since the early days of digital photography. He earned a Ph.D. in Physics from Harvard University.