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.
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.
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.
Technical reports
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.
- 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.
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.
