Programming with Boolean Satisfaction
Michael Codish
Biografía:
Michael Codish completed his PhD at the Weizmann Institute of Science in Israel. He submitted his thesis the day his first daughter was born. Today she is going on 21. Since 1994 he is with the faculty of the Ben-Gurion University of the Negev in Israel. Before this position he enjoyed post-docs at universities in Pisa and in Leuven. He is a frequent research visitor in Madrid and in Melbourne.
Michael Codish is best known for his work applying abstract interpretation to the analysis of logic programs. Since the mid 90's he focussed on the analysis of termination of logic programs. He introduced a semantic definition for logic programs that makes termination an observable. Implementing that semantics as an interpreter and then abstracting the interpreter led to the termination analyzer called TerminWeb, which at the time (1995) was one of the first program analyzers that could be applied via a web interface.
In 2005 while visiting Melbourne University Codish and colleagues, Lagoon and Stuckey, pioneered the application of SAT solving techniques to a termination analysis problem (for term rewrite systems). Since 2005 Codish has applied SAT solving to a variety of termination and other types of problems. This is one of his main current interests.