[Busec] next group meeting Monday @ 1
reyzin at cs.bu.edu
Thu Oct 27 15:54:10 EDT 2011
We meet at the usual time 10/31 at 1pm in the usual place MCS 137 with the
usual (yummy) food.
Our speaker is BU's own Andrei Lapets. He wanted me to mention that he
is interested in having at least part of this talk be a bit more
interactive, maybe even involving some brainstorming about possible ways to
move the project forward that would serve the interests of the group.
User-friendly Interactive Formal Reasoning Assistance
Modern user-friendly interfaces, growing distributed storage and computing
resources, and lightweight verification techniques can help bring the
benefits of static analysis, automated search, and formal verification to
communities of end-users who are not experts in logic and formal systems.
Aartifact is an automated assistant for common high-level formal reasoning
tasks whose design is motivated by this hypothesis. Aartifact has two
components: (1) a database infrastructure allowing domain experts to
assemble collections of high-level formal concepts, structures, and
propositions governing certain application domains, and (2) a web-based
interactive interface for quickly assembling, analyzing, or verifying formal
arguments and models which utilize the contents of the database. We present
a few simple examples illustrating how such a system can provide easy,
instant access to existing formal tools and techniques that address safe
equational reasoning, construction of safe logical arguments, and state
space definition and analysis. We also discuss how the system could act as a
front-end for existing static analysis and state space search tools.
Finally, we solicit discussion and feedback on how the system's database
might be instantiated for particular domains by domain experts, and how it
may be evaluated by, or can better accommodate, particular communities of
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Busec