Events

Sept. 9, 2008
Reading Group: An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, and Gert-Martin Greuel. CAV 2008.

Sept. 23, 2008:
Clark Barrett: Bit-vector arithmetic in SMT.

Sept. 30, 2008:
Reading group: Bounded Verification of Voting Software. Greg Dennis, Kuat Yessenov, and Daniel Jackson. VSTTE 2008.

Oct. 7, 2008:
Dejan Jovanović

Oct. 14, 2008:
Uri Klein: Synthesis of Software from Property Specifications.

Oct. 15, 2008: [NOTE: Wednesday meeting]
Sumit Gulwani (Microsoft Research): SPEED: Statically Estimating Symbolic Computational Complexity of Programs.

Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project at Microsoft Research attempts to address these limitations by static estimation of symbolic computational complexity of programs. The SPEED project builds over recent advances in static program analysis, which has traditionally been used for checking correctness as opposed to measuring performance.

Computing symbolic complexity bounds is a challenging problem since such bounds for even simple sequential programs are usually disjunctive, non-linear, and involve numerical properties of heaps. Sometimes even proving termination is hard (Remember halting problem is undecidable!), and computing bounds ought to be a harder problem. In this talk, I will present some algorithmic techniques used in SPEED for statically estimating the worst-case symbolic computational complexity of procedures in terms of their scalar inputs and user-defined quantitative functions of input data-structures (such as length of a list, or height of a tree). SPEED attempts to generate complexity bounds that are usually precise not only in terms of the computational complexity, but also in terms of the constant factors.

Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.

Oct. 21 and Oct. 28, 2008:
Reading group: A type system equivalent to a model checker. Mayur Naik and Jens Palsberg. TOPLAS Vol. 30 No. 5, 2008.

Nov. 4, 2008:
Chris Conway: The Use and Abuse of CVC for Static Analysis.

Nov. 11, 2008:
Christian Urban (TU Munich): Nominal Techniques in the Theorem Prover Isabelle or, How Not to be Intimidated by the Variable Convention.

If researchers in programming languages want to formalise and check their work in a theorem prover, they need to deal with binders, renaming of bound variables, capture-avoiding substitution, etc. This is very often a major problem in formal proofs. In informal proofs one often assumes a variable convention and thus side-steps all these problems. In the talk I will show how strong induction principles can be derived that have the variable convention already built-in. However, I will also show that this convention is in general an unsound reasoning principle and requires restrictions in order to be safe. The aim of this work is to provide all proving technology necessary for reasoning conveniently about programming languages.

Nov. 18, 2008:
Werner Damm (U. Oldenburg): Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space.

Nov. 25, 2008: No meeting

Dec. 2, 2008:
Yeting Ge: Complete instantiation for quantified SMT formulas.

Quantifier reasoning in Satisfiability Modulo Theories is a long-standing challenge. The practical method employed in modern SMT solvers is to instantiate quantified formulas based on heuristics. One major problem of this instantiation-based approach is incompleteness. For some fragments, e.g. the array property fragment by Aaron et al, it is possible to have a complete instantiation. In this paper, we push forward complete instantiation method by identifying fragments in many-sorted first order logic. When quantifiers range over uninterpreted domain, we define a fragment we call sufficiently stratified. When quantifiers are over interpreted domain, we propose a more restricted fragment we call essentially ground fragment. We then discuss conditions under which an unsorted formula could be converted into a many-sorted one. One drawback of complete instantiation is that the number of useless instantiations is usually huge. We propose a heuristic to pick the most likely instantiation first.

Dec. 9, 2008:
Tim King: BVUTVPI

Dec. 11, 2008: [NOTE: Thursday meeting, 12:00 PM - 1:00 PM]
Satish Chandra & Manu Sridharan (IBM Research): Symbolic Analysis for Java

Bug-finding tools that are based on approximate analysis often report false positives. Burned enough by false positives, a skeptical programmer wants to see convincing evidence that a bug report is indeed feasible. Symbolic analysis can often help produce such evidence in the form of a concrete test case that can reproduce a feasible bug. In this talk, we will describe our recent work on symbolic analysis of Java programs. Our main technical contribution is in the handling of procedure calls during symbolic analysis. We present new techniques to make symbolic analysis work effectively on realistic Java applications, without requiring hand-written specifications of procedures, and without inlining procedure calls away. We will present our preliminary experience with building a bug validator based on symbolic analysis, and discuss some open issues.