Invited talks
ICTAC will have 4 invited talks.
Formal Verification of a Geometry Algorithm:
A Quest for Abstract Views and Symmetry in Coq Proofs
Yves Bertot (Inria Sophia Antipolis - Méditerranée, FR) [DBLP]
This work is an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm, questions of symmetry appear and this exposition attempts to give an account of how these symmetries can be handled. All this work relies on formal developments made with Coq and the mathematical components library.
What Is Knowledge Representation and Reasoning?
Tommie Meyer (University of Cape Town, ZA) [DBLP]
Artificial Intelligence (AI) is receiving lots of attention at the moment, with all kinds of wild speculation in the media about its potential benefits. The excitement is mostly about recent successes in the subarea of AI known as Machine Learning. The current hype is reminiscent of the scenario about 20 years ago when logic-based AI, and more specifically, the subarea known as Knowledge Representation, had everyone in a state of euphoria about the future of AI.
My focus in this talk is on Knowledge Representation. I first provide an overview of the field as a whole, followed up by a more detailed presentation about some of the successful Knowledge Representation techniques and tools. The presentation is augmented with a discussion on the strengths and limitations of the Knowledge Representation approach to AI. Finally, I offer some thoughts on the recently revitalised suggestion that a combination of Knowledge Representation and Machine Learning techniques can lead to further advances in AI.
Finding Rare Concurrent Programming Bugs:
An Automatic, Symbolic, Randomized, and Parallelizable Approach
Gennaro Parlato (University of Southampton, UK) [DBLP]
Developing correct, scalable and efficient concurrent programs is a complex and difficult task, due to the large number of possible concurrent executions that need to be taken into account. Modern multi-core processors with weak memory models and lock-free algorithms make this task even more difficult, as they introduce additional executions that confound the developers' reasoning. Because of these complex interactions, concurrent programs often contain bugs that are difficult to find, reproduce, and fix. Stress testing is known to be very ineffective in detecting rare concurrency bugs as all possible executions of the programs have to be explored explicitly. Consequently, testing by itself is often inadequate for concurrent programs and needs to be complemented by automated analysis tools that enable detection of bugs in a systematic and symbolic way.
In the first part of the talk, I provide an overview of Lazy-CSeq, a symbolic method based on Bounded Model Checking (BMC) and Sequentialization. Lazy-CSeq first translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as backends for the sequential verification problem. This translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight SAT/SMT formulae, and is thus very effective in practice.
In the second part of the talk, I present Swarm-CSeq, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea is to generate a set of simpler program instances, each capturing a reduced set of the original program’s interleavings. These instances can then be verified independently in parallel. Our approach is parametrizable and allows us to fine-tune the nondeterminism and randomness used for the analysis. In our experiments, by using parallel analysis, we show that this approach is able, even with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.
From Logic to Automata by Derivation
Peter Thiemann (Universität Freiburg, DE) [DBLP]
Vardi and Wolper popularized the automata-theoretic approach to automatic program verification. Their key observations are transformations from various logics to finite omega-automata. However, these transformations are constructed by sheer insight.
We show how these transformations from formulae of various temporal logics into suitable alternating finite automata can be understood in terms of derivatives. The key of these transformations is the adaptation of Antimirov's notion of linear factors to the respective logics. We further show that the tableaux-based satisfaction check for LTL can also be explained with derivatives.
(Based on joint work Martin Sulzmann.)