Enhancing theorem prover interfaces with program slice information

DOI10.1016/J.ENTCS.2006.09.019MaRDI QIDQ2867933zbMATH OpenOpenAlexFDO

Authors Louise A. Dennis

Publication date 20 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.09.019

zbMATH Keywords

verificationprogram slicingproof-directed debugging

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1870455
• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• Proof-directed debugging
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Functional design and implementation of graphical user interfaces for theorem provers

Cites work

• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Program Slicing
• Proof-directed debugging
• Source-Based Trace Exploration
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings

Describes a project that uses

Uses Software

• Lambda-Clam
• Hat
• Proof General
• Isar
• IsaPlanner
• Isabelle/HOL

This page was built for publication: Enhancing theorem prover interfaces with program slice information

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2867933)