Ir
ina and Markus attended SPIN symposium that took place in Malaga, Spain, where they gave a tutorial on Software Model Checking for Mobile Security.
Tag Archives: talk
Founding the Foundry Lecture series welcome Prof. Moshe Vardi (Rice University)
Professor Moshe Vardi from Rice University, Texas, will give a talk on The Automated-Reasoning Revolution: From Theory to Practice and Back Wednesday 27th June, 12-1pm, Computational Foundry Seminar Room (Talbot 909).
Abstract:
For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk I will review this amazing development and show how automated reasoning is now an industrial reality.
I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks. Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more. While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees.
Amir Tabatabai and Rahele Jalali visiting
Amir Tabatabai and Rahele Jalali, both PhD students at the Institute of Mathematics of the Czech Academy of Sciences under the supervision of Pavel Pudlak, are visiting Swansea University 13 Nov – 6 Dec 2017.
Amir will give a talk on Computational Flows in Arithmetic on 16 November.
More information: A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among
them. In this talk we will explain the basics of the theory of computational
flows and how they make a sound and complete interpretation for bounded
theories of arithmetic. This property helps us to decompose a first order
arithmetical proof to a sequence of computational reductions by which we can
extract the computational content of the low complexity statements in some
bounded theories of arithmetic such as 
Arno Pauly joining our department
We would like to welcome Arno Pauly, who has recently joined the computer science department here in Swansea. Today he is going to give a talk on Noncomputability in analysis as a part of our Computational Foundry Seminar Series.
More information: Many theorems in analysis state the existence of a certain object depending on some parameter. Each such theorem has an associated computational task: Compute the object from the parameter. From the viewpoint of a constructivist, these tasks are intricately linked to the meaningful truth of the theorems. From a pragmatic perspective, the applicability of a theorem to fields like physics or economics is tied to the solvability of the associated computational task.
Louis Warren visiting
Louis Warren, a PhD student from the University of Canterbury (NZ), is on secondment at Swansea University for a month as a part of the CORCON project. He has given a talk on Classifying the Drinker Paradox and its Dual.