Kedar Namjoshi -- Publications

I've arranged my publications below by topic (some papers appear under multiple topics). The journal and conference articles are usually covered by the publisher's copyright -- they are made available here for convenient access.

Verification Theory
The first paper describes a proof rule for showing equivalence of two programs up to hiding of irrelevant information (stuttering bisimulation). It greatly simplifies the earlier formulations, and is especially well-suited for automated theorem proving (see Pete Manolios' web page for extensions and applications of this idea). The second paper shows how model checkers can be thought of as deductive proof generators. Both failure and success proofs have a number of interesting applications. The third paper fills a gap in proof generation: how to lift a generated proof for an abstraction of a concrete system back to the concrete domain.

A Simple Characterization of Stuttering Bisimulation (.ps)

Certifying Model Checkers (.ps)
Lifting Temporal Proofs Through Abstractions (.ps)

Program Abstraction
A very useful state space reduction technique is to compute an abstraction of the program that preserves just enough information to decide the status of the correctness property. Abstractions are often defined by hand and then proved correct. The first paper adopts this approach; the second paper presents an algorithm to automatically compute predicate abstractions. This algorithm is currently being implemented and tried out on a number of hardware and software examples. The resulting tool, AUTOABS, is described in the third paper. The fourth paper describes how to lift automatically generated proofs from abstract to concrete domains. The fifth paper describes an application of an automated abstraction algorithm to the analysis of "shape" properties of a program heap, such as reachability and circularity.

Linking Theorem Proving and Model Checking with Well Founded Bisimulation (.ps)

Syntactic Program Transformations for Automatic Abstraction (.ps)

AUTOABS: Syntax Directed Program Abstraction (.ps)

Lifting Temporal Proofs Through Abstractions (.ps)
Shape Analysis Through Predicate Abstraction and Model Checking (.ps)

Compositional Reasoning
Most programs are too big (textually or in terms of their state space) to reason about as a single unit. Compositional reasoning attempts to alleviate this problem by reducing reasoning about a composition to reasoning about individual components. This is also closely connected to modular reasoning: for example, using properties established earlier about library functions in reasoning about programs that use the library. The papers below deal both with theoretical issues (when are compositional reasoning rules sound and complete for arbitrary temporal properties?) and practical ones (how to utilise the structural properties of timing diagrams in order to facilitate such reasoning?).

On the Completeness of Compositional Reasoning (.ps)

Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams (.ps)

Visual Specifications for Modular Reasoning about Asynchronous Systems (.ps)

Best Paper Award

Branching Time Compositional Reasoning

Model Checking for Infinite-State Parameterized Systems
The systems considered here are programs with an unbounded number of instances of a small, finite number of process types. The question is whether such a program satisfies an property for all instances . Examples of such programs abound: for example, one may ask whether a distributed mutual exclusion protocol ensures mutual exclusion for all instances? While this question is undecidable in general, the papers below show decidability for important special cases: token rings, synchronous broadcast protocols, and some kinds of broadcast cache-coherence protocols.

Reasoning about Rings (POPL 95) (.ps)

Automatic Verification of Parameterized Synchronous Systems (.ps)

Verification of a Parameterized Bus Arbitration Protocol (.ps)

On Model Checking for Nondeterministic Infinite State Systems (.ps)

Analysis of Timing Diagrams
Timing diagrams appear in almost every hardware manual, but these are informal descriptions which can not be used as formal specifications. In these papers, my co-authors and I provide a formal syntax for timing diagrams, and a semantics in terms of automata. Surprisingly, while the automaton for a timing diagram property can be exponential in the diagram size, the automaton for the negated property is linear! This fortunate occurrence gives rise to efficient, linear time, model checking algorithms. Furthermore, timing diagrams have a decompositional (conjunctive) structure which can be exploited to create heuristics for decomposing a diagram into assume-guarantee pairs for compositional reasoning. These simple heuristics work surprisingly well in practice.

Efficient Decompositional Model Checking for Regular Timing Diagrams (.ps)

Model Checking Synchronous Timing Diagrams (.ps)

RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams (.ps)

Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams (.ps)

Visual Specifications for Modular Reasoning about Asynchronous Systems (.ps)

Best Paper Award

Applications
I have worked on some applications where program semantics and verification questions appear in surprising ways. The first is the problem of detecting conflicts in telecommunications features (e.g., call-waiting); the second tackles the question of whether circular combinational circuits are well defined.

Feature Specification and Automated Conflict Detection (.ps)

Efficient Analysis of Cyclic Definitions (.ps)

Dissertation
For those who're curious about my dissertation, here's a link to it.

Drafts
Compositional Reasoning for Asynchronous Systems (.ps)
(draft, with Nina Amla, E. Allen Emerson, and Richard Trefler)