Show simple item record

dc.contributor.authorLapets, Andreien_US
dc.date.accessioned2012-05-21T18:59:35Z
dc.date.available2012-05-21T18:59:35Z
dc.date.issued2010-05-14
dc.identifier.citationLapets, Andrei. "User-friendly Support for Common Concepts in a Lightweight Verifier", Technical Report BUCS-TR-2010-010, Computer Science Department, Boston University, May 14, 2010. [Available from: http://hdl.handle.net/2144/3789]
dc.identifier.urihttps://hdl.handle.net/2144/3789
dc.description.abstractMachine verification of formal arguments can only increase our confidence in the correctness of those arguments, but the costs of employing machine verification still outweigh the benefits for some common kinds of formal reasoning activities. As a result, usability is becoming increasingly important in the design of formal verification tools. We describe the "aartifact" lightweight verification system, designed for processing formal arguments involving basic, ubiquitous mathematical concepts. The system is a prototype for investigating potential techniques for improving the usability of formal verification systems. It leverages techniques drawn both from existing work and from our own efforts. In addition to a parser for a familiar concrete syntax and a mechanism for automated syntax lookup, the system integrates (1) a basic logical inference algorithm, (2) a database of propositions governing common mathematical concepts, and (3) a data structure that computes congruence closures of expressions involving relations found in this database. Together, these components allow the system to better accommodate the expectations of users interested in verifying formal arguments involving algebraic and logical manipulations of numbers, sets, vectors, and related operators and predicates. We demonstrate the reasonable performance of this system on typical formal arguments and briefly discuss how the system's design contributed to its usability in two case studies.en_US
dc.language.isoen_US
dc.publisherCS Department, Boston Universityen_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2010-010
dc.titleUser-friendly Support for Common Concepts in a Lightweight Verifieren_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record