Van E. Kelly

AAAI Conference 1993 Conference Paper

KITSS: A Knowledge-Based Translation System for Test Scenarios

• Van E. Kelly

AAAI Conference 1987 Conference Paper

Inferring Formal Software Specifications from Episodic Descriptions

• Van E. Kelly

The WATSON automatic programming system computes formal behavior specifications for process-control software from informal "scenarios": traces of typical system operation. It first generalizes scenarios into stimulus-response rules, then modifies and augments these rules to repair inconsistency and incompleteness. It finally produces a formal specification for the class of computations which implement that scenario and which are also compatible with a set of "domain axioms". A particular automaton from that class is constructed as an executable prototype for the specification. WATSON’s inference engine combines theorem proving in a very weak temporal logic with faster and stronger, but approximate, model-based reasoning. The use of models and of closed-world reasoning over "snapshots" of an evolving knowledge base leads to an interesting special case of non-monotonic reasoning.

AAAI Conference 1982 Conference Paper

The CRITTER System: Analyzing Digital Circuits by Propagating Behaviors and Specifications

• Van E. Kelly

CRITTER is a system that reasons about digital hardware designs, using a a declarative representation that can represent components and signals at arbitrary levels of abstraction. CRITTER can derive the behaviors of a component’s outputs given the behaviors of the inputs. It can derive the specifications a component’s inputs must meet in order for some given specifications on the outputs to be met, and it can verify that a given signal behavior satisfies a given specification. By combining these operations, it evaluates both the correctness and the robustness of the overall design.