previous day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 86E: Fairness and Liveness
Location: FH, Seminarraum 101B
Fairness for Infinite-State Systems
SPEAKER: Heidy Khlaaf

ABSTRACT. In this paper we introduce the first known tool for symbolically proving fair-CTL properties of (infinite-state) integer programs. Our solution is based on a reduction to existing techniques for fairness-free CTL model checking. The key idea is to use prophecy variables in the reduction for the purpose of symbolically partitioning fair from unfair executions.

Reducing Deadlock and Livelock Freedom to Termination

ABSTRACT. In this paper we introduce a general method for proving deadlock and livelock freedom of concurrent programs with shared memory. Our goal in this work is to support programs which use locks stored in mutable data structures. The key to our technique is the observation that dependencies between locks can be abstracted using recursion and non-determinism in a sequential logic program such that termination of the abstraction implies deadlock and livelock freedom of the original program.

Specifying and verifying liveness properties of QLOCK in CafeOBJ
SPEAKER: unknown

ABSTRACT. We provide an innovative development of algebraic specifications and proof scores in CafeOBJ of QLOCK's safety and liveness properties. The particular interest of the development is two-fold: Firstly, it extends base specifications in order-sorted and rewriting logics to a meta-level, which requires behavioral logic, thus using the three logics together to achieve the proofs. Secondly, we use a search predicate and covering state patterns that allow us to prove the validity of a property over all possible one step transitions, by which safety and liveness properties in the base and meta level can be proven.

10:15-10:45Coffee Break
10:45-13:00 Session 90AH: SAT Encodings and Semantic Labelling
Location: FH, Seminarraum 101B
Automating Elementary Interpretations
SPEAKER: Harald Zankl

ABSTRACT. We report on an implementation of elementary interpretations for automatic termination proofs.

A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
SPEAKER: Haruhiko Sato

ABSTRACT. We present a general approach to encode termination in the dependency pair framework as a satisfiability problem, and include encodings of dependency graph and reduction pair processors. We use our encodings to increase the power of the completion tool Maxcomp.

Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling
SPEAKER: Alexander Bau

ABSTRACT. We SAT-encode constraints for termination orders based on semantic labelling, argument filters, and recursive path orders, within the dependency pairs framework.

We specify constraints in a high-level Haskell-like language, and translate to SAT fully automatically by the CO4 compiler. That way, constraints can be combined easily.

This allows to write a single constraint for: find a model, and a sequence of ordering constraints for the labelled system, such that at least one original rule can be removed completely.

As an application, we produce a termination proof, verified by CeTA, for TRS/Aprove/JFP\_Ex31.

A Solution to Endrullis-08 and Similar Problems
SPEAKER: Alfons Geser

ABSTRACT. We prove the termination of the string rewriting system Endrullis-08, the termination of infinitely many related systems, and even the termination of their union, an infinite string rewriting system.

SPEAKER: Everyone
13:00-14:30Lunch Break
14:30-16:00 Session 96AI: Term Rewriting Revisited
Location: FH, Seminarraum 101B
On the derivational complexity of Kachinuki orderings

ABSTRACT. For string rewriting systems compatible with the standard Kachinuki ordering it is known that their derivational complexity is primitive recursively bounded. However, in case the definition of Kachinuki orderings comprises a possibly different lexicographic status for different letters, the standard upper bound proof method by monotone interpretations fails, and primitive recursive complexity bounds are an open problem, to the best of our knowledge. In this talk, such an upper bound result is shown by examining worst case rewriting strategies.

Kurth's Criterion H Revisited
SPEAKER: Alfons Geser

ABSTRACT. Criterion H is one of the criteria for termination of string rewriting that Winfried Kurth implemented in his thesis. Criterion H can be slightly improved. The improved version can be translated into a termination proof by Semantic Labelling.

Another Proof for the Recursive Path Ordering

ABSTRACT. Yet another proof of well-foundedness of the recursive path ordering is provided.

16:00-16:30Coffee Break
16:30-18:00 Session 99AH: Discussion and Business Meeting
Location: FH, Seminarraum 101B
Discussion and Business Meeting
SPEAKER: Everyone