Research Laboratory - Laboratory for Logic and Language

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.