Usability and Accessibility of Formal Modeling and Verification Software

Aartifact Lightweight Verification System and Related Frameworks

From 2008 until 2013, this research effort undertaken at Boston University investigated, prototyped, and evaluated (within the classroom and for domain-specific use cases) features and techniques that could improve the usability and accessibility of formal modeling and verification software tools and services. It included the development of variants of a verification system called Aartifact, focusing on the use of heuristic algorithms, fact databases, interactive interfaces, and browser compatibility. Related and/or interoperable frameworks for visualization of mathematical concepts and mathematical content management and presentation were also developed as part of this work and peripheral efforts.

Software Prototypes and Frameworks

Aartifact Verification System.
A Haskell implementation of a formal verification system that can leverage a database of formal facts and an ensemble of heuristic symbolic search algorithms to verify mathematical proofs assembled in a human-legible style and level of detail.
Aartifact Light Web-Based Verifier.
A browser-compatible lightweight variant of the Aartifact Verification System implemented using JavaScript.
Sheaf and Protoql.
Early versions of the Sheaf framework for web-based presentation of mathematical content and the Protoql visualization library were developed as part of this effort. This included the integration of the Aartifact Light interactive proof environment directly into the assignment sections of course notes written and presented using Sheaf, as well as the embedding of Protoql interactive visualizations into the same Sheaf course notes.

Publications and Reports

Towards Accessible Integration and Deployment of Formal Tools and Techniques. [ web, pdf ]
Andrei Lapets, Richard Skowyra, Azer Bestavros, and Assaf Kfoury
Proceedings of TOPI 2013: The 3rd Workshop on Developing Tools as Plug-ins. San Francisco, CA, USA. May 2013.
Accessible Integrated Formal Reasoning Environments in Classroom Instruction of Mathematics. [ web, pdf ]
Andrei Lapets
Proceedings of HCSS 2012: The High Confidence Software and Systems Conference. Annapolis, MD, USA. May 2012.
A User-friendly Interface for a Lightweight Verification System. [ web, pdf ]
Andrei Lapets and Assaf Kfoury
Electronic Notes in Theoretical Computer Science, 285(C):29-41, 2012.
Formal Verification of SLA Transformations. [ web, pdf ]
Vatche Ishakian, Andrei Lapets, Azer Bestavros, and Assaf Kfoury
Proceedings of CloudPerf 2011: IEEE International Workshop on Performance Aspects of Cloud and Service Virtualization. Washington, D.C., USA. July 2011.
User-friendly Support for Common Concepts in a Lightweight Verifier. [ web, pdf, report ]
Andrei Lapets
Proceedings of VERIFY-2010: The 6th International Verification Workshop. Edinburgh, UK. July 2010.
Ontology Support for a Lightweight Formal Verification System.
Andrei Lapets, Prakash Lalwani, and Assaf Kfoury
Technical Report BUCS-TR-2010-012, CS Dept., Boston University, May 2010.
Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code.
Andrei Lapets
Technical Report BUCS-TR-2009-032, CS Dept., Boston University, November 2009.

Acknowledgments

This effort benefitted from the support and cooperation of Boston University, including the Department of Computer Science, the Hariri Institute for Computing.

This work was partially supported by the National Science Foundation under Grants #0720604, #0735974, #0820138, #0952145, and #1012798. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.