The PhD student seminars are intended to be informal and relaxed without the "polish" of the official seminars. The seminars can discuss for example recent results (your own or from an article) or survey some interesting topic. The intended audience is primarily PhD students, but everyone is welcome. Contact Stephan Gocht if you want to give a seminar or receive email announcements about upcoming seminars.
More information about practical details are available in Swedish. There is also a page with previous seminars.
See also the page with the TCS groups official seminars.
02 Oct 2017 at 13:15 in room 4523, Lindstedtsvägen 5
A Tradeoff Between Length and Width in Resolution
This talk will consist of a 45 minute overview of the content of the title paper, which was written by Neil Thapen. This will include a description of the results and formulas examined, as well as a sketch of the proof. Time and interest permitting, I will follow this with up to another hour of more thorough exposition of the proofs and discussion of open questions.
Paper abstract: We describe a family of CNF formulas in n variables, with small initial width, which have polynomial length resolution refutations. By a result of Ben-Sasson and Wigderson it follows that they must also have narrow resolution refutations, of width O(sqrt(n logn)). We show that, for our formulas, this decrease in width comes at the expense of an increase in size, and any such narrow refutations must have exponential length.
06 Apr 2017 at 13:15 in room 4532, Lindstedtsvägen 5
Slicing with Relational Verification, a Precise Program Analysis Technique
(Stephan Gocht, Karlsruhe Institute of Technology)
Slicing is a program analysis technique, which removes statements from a program, preserving a subset of its behavior. To produce minimal slices it is necessary to consider the semantics of the program. Existing semantic approaches use established software verification techniques like symbolic execution, verification condition generation (VCG), term rewriting or abstract interpretation.
I will present a new method based on relational verification to automatically produce precise slices. The advantage of the used relational verification approach is that it is based on coupling invariants instead of functional loop invariants to handle loops. As evaluation with our prototype shows, this is beneficial as coupling invariants for slicing can be found automatically and fast.
05 Apr 2017 at 13:15 in room 4532, Lindstedtsvägen 5
Auto-Tabling for Subproblem Presolving in MiniZinc
(Jip J. Dekker, Uppsala University)
A well-known and powerful constraint model reformulation is to compute the solutions to a model part, say a custom constraint predicate, and tabulate them within an extensional constraint that replaces that model part. Despite the possibility of achieving higher solving performance, this tabling reformulation is often not tried, because it is tedious to perform; further, if successful, it obfuscates the original model. In order to encourage modellers to try tabling, we extend the MiniZinc toolchain to perform the automatic tabling of suitably annotated predicate definitions, without requiring any changes to solvers, thereby eliminating both the tedium and the obfuscation. Our experiments show that automated tabling yields the same tables as manual tabling, and that tabling is beneficial for solvers of several solving technologies.