Well-structured pushdown systems (WSPDSs) extend pushdown systems withwell-quasi-ordered (possibly infinitely many) states and stack alphabet. As an expressive model for concurrent recursive computations, WSPDSs are believed to "be close the border of undecidability"[11]. Most of the decidability results are known only on subclasses. In this paper, we investigate the decidability of the termination and boundedness problems for WSPDSs using two algorithms: One is an extension of the reduced reachability tree technique proposed by Leroux et. al in [11]. The other is based on Post*-automata technique which has been successfully applied in the model checking of pushdown systems. The complexity of both are Hyper-Ackermannian for bounded WSPDSs. We implement both algorithms and make experiments on a large number of randomly generated WSPDSs. The results illustrate thatthe Post*-automata based algorithm sometimes behaves an order of magnitude faster.

Binary code analysis has attracted much attention. The difficulty lies in constructing a Control Flow Graph (CFG), which is dynamically generated and modified, such as mutations. Typical examples are handling dynamic jump instructions, in which destinations may be directly modified by rewriting loaded instructions on memory. In this paper, we describe a PhD project proposal on a hybrid approach that combines static analysis and dynamic testing to construct CFG from binary code. Our aim is to minimize false targets produced when processing indirect jumps during CFG construction. To evaluate the potential of our approach, we preliminarily compare results between our method and Jakstab, a state-of-the-art tool in this field.

SAT and SMT (SAT modulo theory) solvers aim to find a satisfiable instance of given constraints. SAT solver accepts a boolean constraints in a conjunctive normal form (CNF), such as, and if a CNF is satisfiable, returns an instance, such as. SMT solver accepts constraints described in background theory, such as arithmetic. Part 1 is devoted to explain the textbook concepts and usage of SAT and SMT solvers. For their usage, we investigate how to encode problems into CNF. Examples are taken from puzzles. Although puzzles are problems on bounded domains, there is certain hierarchy of difficulties, corresponding to the logical hierarchy of problems. Our examples are SUDOKU [2], Logic pictures [3], and Slither link [4] 1, 2, which correspond to descriptions in CNF, general propositional logic, and higher order logic, respectively. As conversion techniques to efficient CNFs, a popular Tseitin conversion and two special techniques (for the latter two, respectively) are introduced. If time allows, we will overview on de-facto-standard algorithm designs for SAT solvers, i.e., non-chronological back tracking with implication graphs, conflict driven learning and reset, and two watched literals [1].

This paper proposes a counterexample-guided narrowing approach, which mutually refines analyses and testing if (possibly spurious) counterexamples are found. A prototype tool CANAT for checking roundoff errors between floating point and fixed point numbers is reported with preliminary experiments.

Pushdown systems are well understood as abstract models of programs with (recursive) procedures. Reps et al. recently extended pushdown systems into weighted pushdown systems, which serve as a generalized framework for solving certain kinds of meet-over-all-path problems in program analysis. In this paper, we extend weighted pushdown systems to conditional weighted pushdown systems, by further specifying conditions under which a pushdown transition rule can be applied, and show that model checking problems on conditional weighted pushdown systems can be reduced to those on weighted pushdown systems.

This paper proposes a framework for statically analyzing overflow and roundoff errors of C programs. First, a new range representation, "extended affine interval", is proposed to estimate overflow and roundoff errors. Second, the overflow and roundoff error analysis problem is encoded as a weighted model checking problem. To avoid widening, currently we focus on programs with bounded loops, which typically appear in encoder/decoder reference algorithms. Last, we implement the proposed framework as a static analysis tool CANA. Experimental results on small programs show that the extended affine interval is much more precise than classical interval.

flow analyses are reduced to the problem of finding a fixed point in a certain transition system, and such fixed point is commonly computed through an iterative procedure that repeats tracing until convergence.

In this paper we propose a new method for deriving a practical linear-time algorithm from the specification of a maximum-weightsum problem: From the elements of a data structure x, find a subset which satisfies a certain property p and whose weightsum is maximum. Previously proposed methods for automatically generating linear-time algorithms are theoretically appealing, but the algorithms generated are hardly useful in practice due to a huge constant factor for space and time. The key points of our approach are to express the property p by a recursive boolean function over the structure x rather than a usual logical predicate and to apply program transformation techniques to reduce the constant factor. We present an optimization theorem, give a calculational strategy for applying the theorem, and demonstrate the effectiveness of our approach through several nontrivial examples which would be difficult to deal with when using the methods previously available.