Research Laboratory - Laboratory for Logic and Language

updated: 02.06.2021

Automated theorem proving and computer-aided verification have been topics of research since the earliest days of computers. Attempting to prove correctness of programs and similarly verification of circuits face many difficulties. The general problems are unsolvable, many restrictions that are solvable are intractable, and those that are fast enough often require human intervention.


Nonetheless, many practical applications of mathematical logic to computer science have burgeoned over the last decades, not only in the domains of verification of software and hardware, but also in artificial intelligence and programming languages. Some of these efforts have attained sufficient maturity to have been packaged in commercial products, most notably the "model checking" technique for verification of protocols and circuits. The overall potential future impact of formal methods based on logic is enormous.


Members of the lab also engage in research on the semantics of natural language.


Location: 441 Checkpoint


The lab is supervised by Prof. Nachum Dershowitz, Prof. Arnon Avron, and Prof. Alexander Rabinovich.

Tel Aviv University makes every effort to respect copyright. If you own copyright to the content contained
here and / or the use of such content is in your opinion infringing, Contact us as soon as possible >>