The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
The proof assistant Isabelle/HOL owes much of its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on external automatic theorem provers for its proof search, and the counterexample generator Nitpick is based on a finite model finder, which performs a reduction to propositional satisfiability (SAT). This talk will describe how these tools work and how they help make Isabelle users more productive.