What is the focus of your work?
I mostly work on automated reasoning and constraint solving. A variety of problems in computer science and beyond can be recast as constraint solving problems. This includes analyzing the functional correctness of computer hardware or software components, identifying security vulnerabilities in software, and optimizing program execution, among many others. The constraint solving problems generated in these applications are often computationally challenging because they require the exploration of an exponentially large space of solutions. In my group, we focus on the theoretical foundations and tool development for a groundbreaking and successful form of constraint solving called Satisfiability Modulo Theories, or SMT.
Tell us about the broad impact it has/could have.
In the last 10-15 years, SMT has become an enabling technology for several areas of computer science, often revolutionizing research there thanks to the reasoning power of SMT solvers. In collaboration to Professor Clark Barrett's group at Stanford University, we have been developing a leading SMT solver, called CVC4, which is used widely in academia and industry. Most recently, Amazon Web Services has started to use it to verify that its customers set up correct control access policies for their data on the Amazon cloud. Such policies can be quite difficult for customers to specify correctly, potentially resulting in unauthorized data access. AWS relies on CVC4 to discover errors in them or certify their correctness. The same technology is also used to improve the quality of other software services at AWS, resulting overall in millions of calls per day to our tool.
What excites you about the environment in CLAS?
I would say the large number of disciplines represented by the many departments and programs in the college, and the opportunities that this offers for interdisciplinary research and education. In the Computer Science department, we have exciting and fruitful collaborations with colleagues from several other departments in the college.
What are your hobbies and pursuits outside of work?
I am an avid reader of non-fiction. I am generally curious about how things work, which makes me interested in many topics: technology, of course, but also engineering, physics, economics, sustainable agriculture, linguistics, history, cinema, and more. I do not seek any kind of expertise in these areas. I simply enjoy learning about them to satisfy my curiosity. In the age of search engines, Wikipedia, and online publications of any sort, this activity easily ends up taking most of my free time.
Favorite things to do in Iowa City?
It must be urban hiking. My wife and I like walking and love the city's extensive trail system. In addition, sometimes we will drive to some random neighborhood and just walk around to discover the surroundings. We also enjoy more traditional hiking in the Coralville Lake area and love that it is just a short drive from home.
Professor Cesare Tinelli joined the Department of Computer Science in 1999. His work has focused on software verification and on automated reasoning, in particular in Satisfiability Modulo Theory (SMT), a field he helped establish through his research and service activities. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He led the development of the award winning Darwin theorem prover and leads the development of the Kind model checker. Together with Prof. Clark Barrett of Stanford University he also leads the development of the award winning and widely used CVC4 SMT solver. He also is involved in the development of StarExec, a cross community web-based service for the comparative evaluation of logic solvers.