<div class="gmail_quote"><br></div><div class="gmail_quote">Hi, Everyone,</div><div class="gmail_quote"><br></div><div class="gmail_quote">We meet at the usual time 10/31 at 1pm in the usual place MCS 137 with the usual (yummy) food.</div>

<div class="gmail_quote"><br></div><div class="gmail_quote">Our speaker is BU&#39;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.</div>

<div class="gmail_quote"><br></div><div class="gmail_quote">Abstract</div><div class="gmail_quote"><br>
User-friendly Interactive Formal Reasoning Assistance<br>
<br>
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&#39;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 potential end-users.<br>


<br><br></div>