Symbolic Computation Techniques in SMT Solving

When: 2nd Nov 2017, 18:00 - 2nd Nov 2017, 21:00
Where: The London Mathematical Society De Morgan House, 57-58 Russell Square, London, WC1B 4HS
Town/City: London
Organiser: BCS FACS (Formal Aspects of Computing Science) Specialist Group
Price: Free
Further Information: Further Information

Joint event with the London Mathematical Society

Prof. Erika AbrahamSpeaker: Prof. Erika Abraham, University of Aachen

Details:

The satisfiability problem is the problem of deciding whether a logical formula is satisfiable. For firstorder 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.

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

S
M
T
W
T
F
S
1
3
4
6
8
9
10
11
12
13
14
17
18
19
20
21
22
25
26
27
28