iProver --- an instantiation-based theorem prover for first-order logic. New version iProver v0.8.1 (post CASC-J5, 2010) is released!!! Hard Reality Tool --- HRT is a tool for randomly extracting
hard and realistic theory problems (conjunctive constraints) from SMT problems with a non-trivial boolean structure.
GoRRiLA is another tool for randomly generating (i) linear arithmetic problems and (ii) propositional problems.
PhD opportunities:
If you are interested in any of the topics above and would like
to apply for a PhD at School of Computer Science please do not hesitate to contact me.
Students:
Ph.D. Christoph Sticksel (co-supervised with Renate Schmidt) graduated 2011, congratulations Christoph!!!
MSc. Ahmad Abu-Khazneh (graduated 2007)
PC member of: IJCAR'2012, LPAR-18 (2012), IWIL 2012,FTP'2011, LPAR-17, LPAR-16, IWIL'2010, LPAR'09, RTA'08, PAAR'08, LPAR'07
Invited talks: Collegium Logicum 2011, CADE-22 (09), ARW'09, IWIL'06
Teaching: