Reports and documents
From Automated Assistance for Formal Reasoning
This is a collection of links to documents pertaining to the design, definition, implementation, and application of the aartifact system.
[edit] Presentation slides
Provides background and motivation for a dedicated interface layer for machine verification systems. Also contains a detailed step-by-step illustration of how the simulated dynamic context grows as a formal argument is processed by the aartifact system, along with data on the growth rate of the dynamic context during processing of example arguments.
[edit] Drafts
- Machine Involvement in Formal Reasoning (PDF)
This text assembles much of the content found in the technical reports below. It describes the design of many components of the aartifact system. It also includes an extensive discussion of related work and the motivation behind the aartifact design.
[edit] Publications and technical reports
[edit] Definition, design, and implementation
- A User-friendly Interface for a Lightweight Verification System (PDF)
This report motivates and describes the design of the aartifact user interface. Appears in Proceedings of UITP'10: 9th International Workshop On User Interfaces for Theorem Provers.
- User-friendly Support for Common Concepts in a Lightweight Verifier (PDF)
This is a discussion paper on the topic of usability and formal verification systems. Appears in Proceedings of VERIFY-2010: The 6th International Verification Workshop.
- Ontology Support for a Lightweight Verification System (PDF)
This report discusses the implementation of the static context.
- Designing accessible lightweight formal verification systems (PDF)
This report describes the symbolic logical rules and associated inference and search algorithms in an early aartifact prototype. It also motivates a focus on user interface design in verification tools, and references several similar projects.
- Efficient Support for Common Relations in Lightweight Formal Reasoning Systems (PDF)
This report describes earlier work on the dynamic context implementation.
[edit] Applications
- Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches (PDF)
The aartifact system is applied in verifying the soundness of the NetSketch type system.
- Safe Compositional Network Sketches: Reasoning with Automated Assistance (PDF)
Describes how aartifact can be used to model individual modules within the NetSketch formalism.
- Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code (PDF)
This report describes our experience deploying an early prototype of aartifact in a classroom setting.