POPL02:Lazy Abstraction

Today I read this paper again, and find that I have not capture its major ideas before.

Actually, It first unfold the control flow of the program to construct a tree that can reach the error position. This graph's each vertex is labeled with its own set of predicates and the reachable states formula expressed in these predicates. Its edge is labeled with the basic block of the program.

Then it backtrack and compute weakest precondition at each edge, until it find a node whose intersection of reachable state and precondition formula is empty. This will discover a new predicate by analyzing the unsat proof of this intersection .

Third, it constructs new abstract model from this pivot state to reach more errors again.

For each node reached, if it is also reached before, and the old node's label formula cover the new reached node's formula, then this node does not need to be explored any more.

CAV11:HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection

What is important is the solver on strings.

CAV11:Interpolation-Based Software Verification with Wolverine

This paper is not interesting, but the tool is open source, that is the point.

TACAS11:Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models

This paper propose some very simple memory models for TSO and PSO, and then, I think it is the most important idea, find out whether there is some behavior on these models that can't occur in normal SC model.

FMCAD11:Effective Word-Level Interpolation for Software Verification

It proposes a layered approach to generate word level interpolant for BV.

The traditional approach include two DPLL solver, one for the Boolean skeleton on the formula, the other for the conjunction of BV clauses. When a satisfying assignment is generated by the Bool solver, it is passed to the BV solver to verify it consistency.

This paper's approach inserts some layer between this two solver. These layers are over-approximation of the BV solver. They check for easier cases that can generate interpolants. For example, EUF.

FMCAD07:Lifting Propositional Interpolants to the Word-Level

This paper lift the resolution tree of the SAT instance that generated from an EUF formula.

In the analysis, it not only need the resolution tree, but also the corresponding equality predicates that introduced in encoding EUF equality into CNF, and also the clause structure of this encoding.

So I can not use it to infer word level structure for a purely bit level CNF generated from complementary synthesis.

VMCAI11:SAT-Based Model Checking Without Unrolling

This approach contains two nested loop,

1. in the major loop, it iteratively constructs a list of formulas F0....Fk, in which Fk means the over-approximation of the states set reachable in k steps.

2. in the minor loop, it iteratively refines the F0...Fk, such that they form an inductive path that leads to the property P to be verified.

DAC11:Re-Synthesis for Cost-Efficient Circuit-Level Timing Speculation

This paper reduce the number of paths that need "Timing Speculation" by retiming to improve timing character.

And then it use ILP to share pading buffers between different paths.

MICRO03:Razor: A Low-Power Pipeline Based on Circuit-Level Timing Speculation

Dynamic voltage scaling is widely used to reduce the power consumption, but it need to guarentee that all critical paths can run correctly.This may seem too conservative becasue too long path only account for a very small percent of all paths.

So this paper propose to use a shadow register to sample the critical path a little bit later than the real register, and then compare them. If the result is not the same, then a circuit is used to roll back the correct state.

One major overhead of "Timing Speculation" is the need to pad the short paths, to prevent them from making the comparator to think that a too long path has cause a timing error.

DAC11:Abstraction-Based Performance Analysis of NoCs

It infers the traffic pattern for each channel in a NOC by analyzing the simulation trace generated by typical benchmarks.

This traffic pattern include the burst transition number, transition rate and bound.

And then it generate a regulator for each channel that represent this pattern and insert them into the correspoding channel, and constraint that they all hold in verification.

In this way, the traffic pattern that we interest in will be forced to hold.

This approach can also be extended to multiple channels, for example, to constrain that we dont allow five source to flood the sink at the same time, be we allow one of them to send.

Inferring Assertion for Complementary Synthesis" is accepted by ICCAD'1

My paper "Inferring Assertion for Complementary Synthesis" has just been accepted by ICCAD'11.

TACAS11: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

Very interesting paper that combine AC(ssociativity and commutativity) operators with Shostak approach.

Generally, there are two approaches for theory combinations, nelson-oppen and Shostak.

The former one just pass equalities between T-solvers, so it is relativly easy to combine AC with it.

But for Shostak, it need to computer canonical form, which is not possible for AC.

TACAS11: Transition Invariants and Transition Predicate Abstraction for Program Termination

Very interesting.
Normal invaraints and abstraction are for states, while this paper apply them to transitions.
But I think the disjunctive well foundness is a very well known result.
I dont understand why this paper published on TACAS 11 again, these topic are well discussed before 2006.

CAV11: Verification of Certifying Computations

Instead of directly verifying a program, this paper tries to verify the checker of a particular program.

This checker is actually an over-approximation of the behavior of the original program.

CAV11: Existential Quantification as Incremental SAT

It use ALLSAT approach to perform existential quatification. And use increamental SAT to reduce the run time overhead.

But I think the major innovation is to use sorting network to find out the shortest prime clause. This is bettern than my approach in VMCAI05: Minimizing Counterexample with Unit Core Extraction and Incremental SAT, which reduce the size of a block clause by iteratively remove those literal not in the support set of a proof.

CAV11: Temporal property verification as a program analysis task

It is a very interesting paper. Given a transition system and a temporal logc property, generate a program that search for the proof or counterexample of this property. and then use existing program analysis tools to determine that whether this program terminate with some answer.

All the methods that boost the speed, such as abstraction refinement, will be automatically performed by the program analysis tools.