Justifying LMC Proofs to Support Debugging
This recently begun project aims to provide necessary support for
debugging specifications using XMC. Since we use
a tabled logic programming system to implement
model checkers, the various lemmas used in a
proof (or disproof) have been memoized in the tables.
A Justifier reconstructs the proof from the tables,
to provide a user of the system with detailed information
of how a proof (or disproof) was reached.
The interesting questions here pertain to presentation:
how to select only significant parts of a proof,
how to navigate the proof structures, and
how to represent fixed point computations in the proof.
Contact: lmc@cs.sunysb.edu
Last modified: Tue Jun 30 14:00:00 DST 1998