LMS/BCS-FACS Evening Seminars

In association with the British Computer Society Formal Aspects of Computing Science BCS-FACS the LMS hosts an annual evening seminar on aspects of the computer science-mathematics interface. These events are free to anyone who wishes to attend, and have attracted high quality speakers.

The 2017 LMS/BCS-FACS Seminar will be held on 2nd November at 6:00pm at De Morgan House.  Professor Erika Ábrahám of RWTH Aachen University will give a talk titled Symbolic Computation Techniques in SMT Solving.

Abstract:The satisfiability problem is the problem of deciding whether a logical formula is satisfiable. For first order arithmetic theories, in the early 20th century some novel solutions in form of decision procedures were developed in the area of Mathematical Logic. With the advent of powerful computer architectures, a new research line of Symbolic Computation started to develop practically feasible implementations of such decision procedures.

Independently, for checking the satisfiability of propositional logic formulas, around 1960 a new technology called SAT solving started its career. Despite the fact that the problem is NP complete, SAT solvers showed to be very efficient when employed by formal methods for verification. Motivated by this success, the power of SAT solving for Boolean problems had been extended to cover also different theories. Nowadays, fast SAT-modulo-theories (SMT) solvers are available also for arithmetic problems. These sophisticated tools are continuously gaining importance, as they are at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas.

Due to their different roots, Symbolic Computation and SMT solving tackle the satisfiability problem differently, offering potential for combining their strengths. This talk will provide a general introduction to SMT solving and decision procedures for non-linear arithmetic, and show on the example of the Cylindrical Algebraic Decomposition method how algebraic decision procedures, rooted in Symbolic Computation, can be adopted in the SMT solving context to synthesise beautiful novel techniques for solving arithmetic problems.

A poster is available.

If you wish to attend, please email lmscomputerscience@lms.ac.uk.

Previous Seminars

2016

Professor Muffy Calder - Probabilistic Formal Analysis of Software Usage Styles in the Wild

2015

Professor Roland Backhouse - The Mathematics of Programme Construction

2014

Professor Joel Ouaknine - Decision Problems for Linear Recurrecnce Sequences

2013

Professor Philippa Gardner - Views: Compositional Reasoning for Computer Programs

2012

Professor Jack Copeland - The Mathematical Objection: Turing, Gödel and Penrose on the Mind

2011

Professor Andrew Ireland - Reasoned Modelling: Towards Decision Support for System Designers.

2010

Professor Peter O’Hearn - Reasoning about Programmes Using a Scientific Method

2009

Professor Mike Gordon, FRS – Forward with Hoare.

2008

Professor John Tucker – The Equations of Computer Science