tag:calagator.org,2005:/events/searchCalagator: Events tagged with: formal methods2018-07-24T15:08:28-07:00tag:calagator.org,2005:Calagator::Event/12504557582008-09-21T15:12:32-07:002008-09-22T08:57:00-07:00FMCAD 2008 (Formal Methods in Computer Aided Design)Monday, November 17, 2008 at 8:15am through Thursday, November 20, 2008 at 3:45pm at Embassy Suites Portland--Downtownhttp://calagator.org/events/12504557582008-11-17T08:15:00-08:002008-11-20T15:45:00-08:00<div class="vevent">
<h1 class="summary">FMCAD 2008 (Formal Methods in Computer Aided Design)</h1>
<div class='date'><time class="dtstart dt-start" title="2008-11-17T08:15:00" datetime="2008-11-17T08:15:00">Monday, November 17, 2008 at 8:15am</time> through <time class="dtend dt-end" title="2008-11-20T15:45:00" datetime="2008-11-20T15:45:00">Thursday, November 20, 2008 at 3:45pm</time></div>
<div class="location vcard">
<a href='/venues/202390607' class='url'>
<span class='fn org'>Embassy Suites Portland--Downtown</span>
</a>
<div class="adr">
<div class="street-address">319 Sw Pine St</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=319%20Sw%20Pine%20St,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<h1>Important Dates</h1>
<p> Early Registration Deadline: October 14, 2008
Hotel Registration Deadline: October 18, 2008</p>
<h1>Conference Overview</h1>
<p> FMCAD 2008 is the eighth in a series of conferences on the theory
and application of formal methods in hardware and system design and
verification. In 2005, the bi-annual FMCAD and sister conference
CHARME decided to merge to form an annual conference with a unified
community. The resulting unified FMCAD provides a leading
international forum to researchers and practitioners in academia and
industry for presenting and discussing groundbreaking methods,
technologies, theoretical results, and tools for formally reasoning
about computing systems, as well as open challenges therein.</p>
<h1>Local Information</h1>
<p> The Conference will be held at the Embassy Suites (Downtown) in
Portland, Oregon. We have negotiated a special rate with the hotel
for conference attendees. Please book early to secure the reduced
rate. For details, please see the conference web page. A dinner
cruise on the Willamette River is planned.</p>
<h1>Technical Program</h1>
<p> The technical program is available at the conference web page. It
includes 2 invited keynotes, 4 invited tutorials, 24 regular papers,
4 short papers, and 2 panels.</p>
<p> Keynotes</p>
<hr>
<p> o Ken McMillan (Cadence): Interpolation -- Theory and Applications
o Carl Seger (Intel): Formal Methods and Physical Design: Match Made
in Heaven or Fools' Paradise?</p>
<p> Tutorials</p>
<hr>
<p> o Kevin Jones (Rambus): Analog and Mixed Signal Verification: The
State of the Art and some Open Problems
o Moshe Levinger (IBM): Building a Bridge: From Pre-Silicon
Verification to Post-Silicon Validation
o Byron Cook (Microsoft): Computing Bounds on Space and Time for
Hardware Compilation.
o David Hardin (Rockwell Collins): Considerations in the Design and
Verification of Microprocessors for Safety-Critical and
Security-Critical Applications.</p>
<p> Panels</p>
<hr>
<p> o High Level Design and ESL: Who Cares?
o The Future of Formal: Academic, IC, EDA, and Software Perspectives</p>
<h1>Sponsors</h1>
<pre><code> Sponsored by: IEEE CEDA
</code></pre>
<p> In cooperation with: ACM SIGDA
Financial support: Cadence, Galois, IBM, Intel, NEC, Synopsys</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://fmcad.org/2008">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/acm">acm</a>, <a class="p-category" href="/events/tag/fmcad">fmcad</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/hardware">hardware</a>, <a class="p-category" href="/events/tag/ieee">ieee</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250455758.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250455758/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Sunday, September 21, 2008 at 3:12pm</strong> and last updated <br /><strong>Monday, September 22, 2008 at 8:57am</strong>.
</div>
</div>
</div>
45.5221 -122.6741tag:calagator.org,2005:Calagator::Event/12504578872009-10-20T16:16:49-07:002009-10-20T16:16:49-07:00Galois Talk: How to choose between a screwdriver and a drillTuesday, October 27, 2009 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504578872009-10-27T10:30:00-07:002009-10-27T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois Talk: How to choose between a screwdriver and a drill</h1>
<div class='date'><time class="dtstart dt-start" title="2009-10-27T10:30:00" datetime="2009-10-27T10:30:00">Tuesday, October 27, 2009 from 10:30</time>–<time class="dtend dt-end" title="2009-10-27T11:30:00" datetime="2009-10-27T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>The next talk in the Galois Tech Seminar series:</p>
<ul>
<li>Date: Tuesday, October 27th, 2009</li>
<li>Title: How to choose between a screwdriver and a drill</li>
<li>Speaker: Tanya L. Crenshaw</li>
<li>Time: 10:30am - 11:30am</li>
<li>Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204</li>
</ul>
<p>For details (including an abstract and speaker bio), please see our
blog post: <a href="http://www.galois.com/blog/2009/10/20/crenshaw-simplex/">http://www.galois.com/blog/2009/10/20/crenshaw-simplex/</a></p>
<p>An RSVP is not required; but feel free to drop a line to
<a href="mailto:levent.erkok@galois.com">levent.erkok@galois.com</a> if you've any questions or comments.</p>
<p>Levent Erkok</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2009/10/20/crenshaw-simplex/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/simplex">simplex</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250457887.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250457887/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, October 20, 2009 at 4:16pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504582542010-01-29T15:01:27-08:002010-01-29T15:01:27-08:00Galois Tech Talk: "An Introduction to the Maude Formal Tool Environment"Tuesday, February 2, 2010 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504582542010-02-02T10:30:00-08:002010-02-02T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: "An Introduction to the Maude Formal Tool Environment"</h1>
<div class='date'><time class="dtstart dt-start" title="2010-02-02T10:30:00" datetime="2010-02-02T10:30:00">Tuesday, February 2, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-02-02T11:30:00" datetime="2010-02-02T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Hello,</p>
<p>The next Galois Tech Talk will be "An Introduction to the Maude Formal
Tool Environment", presented by Joe Hendrix on Tuesday, February 2nd,
at 10:30am.</p>
<p>For more details, please visit:
<a href="http://www.galois.com/blog/2010/01/29/tech-talk-an-introduction-to-the-maude-formal-tool-environment/">http://www.galois.com/blog/2010/01/29/tech-talk-an-introduction-to-the-maude-formal-tool-environment/</a></p>
<p>Hope to see you there!
-Iavor</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2010/01/29/tech-talk-an-introduction-to-the-maude-formal-tool-environment/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/functional programming">functional programming</a>, <a class="p-category" href="/events/tag/galois">galois</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250458254.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250458254/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Friday, January 29, 2010 at 3:01pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504587062010-05-21T14:45:58-07:002010-05-21T14:45:58-07:00Galois Tech Talk: The L4.verified ProjectMonday, May 24, 2010 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504587062010-05-24T10:30:00-07:002010-05-24T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: The L4.verified Project</h1>
<div class='date'><time class="dtstart dt-start" title="2010-05-24T10:30:00" datetime="2010-05-24T10:30:00">Monday, May 24, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-05-24T11:30:00" datetime="2010-05-24T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>The L4.verified Project
Presented by Dr. Gerwin Klein.</p>
<p>Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2010/05/21/tech-talk-the-l4-verified-project/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/functional programming">functional programming</a>, <a class="p-category" href="/events/tag/galois">galois</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250458706.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250458706/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Friday, May 21, 2010 at 2:45pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504587682010-06-11T15:28:16-07:002010-06-11T15:28:16-07:00Galois Tech Talk: Introducing Well-Founded RecursionTuesday, June 15, 2010 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504587682010-06-15T10:30:00-07:002010-06-15T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Introducing Well-Founded Recursion</h1>
<div class='date'><time class="dtstart dt-start" title="2010-06-15T10:30:00" datetime="2010-06-15T10:30:00">Tuesday, June 15, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-06-15T11:30:00" datetime="2010-06-15T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Introducing Well-Founded Recursion
Eric Mertens</p>
<p>Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2010/06/11/tech-talk-introducing-well-founded-recursion/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/functional programming">functional programming</a>, <a class="p-category" href="/events/tag/galois">galois</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250458768.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250458768/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Friday, June 11, 2010 at 3:28pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504594182010-11-02T11:03:05-07:002010-11-02T11:03:44-07:00Galois Tech Talk: Copilot: A Hard Real-Time Runtime MonitorTuesday, November 9, 2010 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504594182010-11-09T10:30:00-08:002010-11-09T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Copilot: A Hard Real-Time Runtime Monitor</h1>
<div class='date'><time class="dtstart dt-start" title="2010-11-09T10:30:00" datetime="2010-11-09T10:30:00">Tuesday, November 9, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-11-09T11:30:00" datetime="2010-11-09T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Lee Pike.</p>
<p>We address the problem of runtime monitoring for hard real-time programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2010/11/02/tech-talk-copilot-a-hard-real-time-runtime-monitor/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/real time">real time</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250459418.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250459418/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, November 2, 2010 at 11:03am</strong> and last updated <br /><strong>Tuesday, November 2, 2010 at 11:03am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504594592010-11-09T14:05:17-08:002010-11-09T14:05:17-08:00Galois Tech talk: Formal Methods Applied to Control SoftwareTuesday, November 16, 2010 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504594592010-11-16T10:30:00-08:002010-11-16T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech talk: Formal Methods Applied to Control Software</h1>
<div class='date'><time class="dtstart dt-start" title="2010-11-16T10:30:00" datetime="2010-11-16T10:30:00">Tuesday, November 16, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-11-16T11:30:00" datetime="2010-11-16T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>speaker: Alwyn Goodloe</p>
<p>Critical cyber-physical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the Frama-C tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://www.galois.com/blog/2010/11/09/tech-talk-formal-methods-applied-to-control-software/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/control systems">control systems</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250459459.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250459459/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, November 9, 2010 at 2:05pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504596502011-01-18T14:07:44-08:002011-01-18T14:07:44-08:00Galois tech talk: Program Inconsistency Detection using Weakest PreconditionsTuesday, January 25, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504596502011-01-25T10:30:00-08:002011-01-25T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois tech talk: Program Inconsistency Detection using Weakest Preconditions</h1>
<div class='date'><time class="dtstart dt-start" title="2011-01-25T10:30:00" datetime="2011-01-25T10:30:00">Tuesday, January 25, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-01-25T11:30:00" datetime="2011-01-25T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Aaron Tomb.</p>
<p> Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior --- often a collection of independent assertions sprinkled throughout the program.</p>
<p>Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus.</p>
<p>We have applied our analysis to a large body of widely-used open-source software, and found a number of bugs.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/1/18/tech-talk-program-inconsistency-detection-using-weakest-prec.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/debugging">debugging</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/static analysis">static analysis</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250459650.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250459650/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, January 18, 2011 at 2:07pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504597212011-02-03T11:09:05-08:002011-02-07T10:45:33-08:00Galois Tech talk: The Strategy Challenge in Computer AlgebraMonday, February 7, 2011 from 4:30-5:30pm at Galois, Inchttp://calagator.org/events/12504597212011-02-07T16:30:00-08:002011-02-07T17:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech talk: The Strategy Challenge in Computer Algebra</h1>
<div class='date'><time class="dtstart dt-start" title="2011-02-07T16:30:00" datetime="2011-02-07T16:30:00">Monday, February 7, 2011 from 4:30</time>–<time class="dtend dt-end" title="2011-02-07T17:30:00" datetime="2011-02-07T17:30:00">5:30pm</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Grant Passmore.</p>
<p>In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: user-specifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different.</p>
<p>In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worst-case doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one?</p>
<p>The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification tool-chains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions).</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/2/3/tech-talk-the-strategy-challenge-in-computer-algebra.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/algebra">algebra</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250459721.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250459721/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, February 3, 2011 at 11:09am</strong> and last updated <br /><strong>Monday, February 7, 2011 at 10:45am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504604432011-04-06T16:00:25-07:002011-04-06T16:00:25-07:00Galois Tech Talk: The OpenTheory Standard Theory LibraryTuesday, April 12, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504604432011-04-12T10:30:00-07:002011-04-12T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: The OpenTheory Standard Theory Library</h1>
<div class='date'><time class="dtstart dt-start" title="2011-04-12T10:30:00" datetime="2011-04-12T10:30:00">Tuesday, April 12, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-04-12T11:30:00" datetime="2011-04-12T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Joe Hurd.</p>
<p>Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is cross-prover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/4/6/tech-talk-the-opentheory-standard-theory-library.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/opentheory">opentheory</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250460443.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250460443/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Wednesday, April 6, 2011 at 4pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504607982011-07-05T10:48:42-07:002011-07-05T10:48:42-07:00Galois tech talk: Parallel K-induction based Model CheckingTuesday, July 12, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504607982011-07-12T10:30:00-07:002011-07-12T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois tech talk: Parallel K-induction based Model Checking</h1>
<div class='date'><time class="dtstart dt-start" title="2011-07-12T10:30:00" datetime="2011-07-12T10:30:00">Tuesday, July 12, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-07-12T11:30:00" datetime="2011-07-12T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Temesghen Kahsai.</p>
<p>We give an overview of a parallel k-induction-based model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. A first level of parallelism is introduced in the k-induction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the k-induction loop as soon as they are produced and used to strengthen the induction hypothesis.</p>
<p>This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property -- valid or invalid -- is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties.</p>
<p>We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/7/5/tech-talk-parallel-k-induction-based-model-checking.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/model checking">model checking</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250460798.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250460798/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, July 5, 2011 at 10:48am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504612002011-08-08T09:29:02-07:002011-08-08T09:29:02-07:00Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Satisfiability CheckingWednesday, August 10, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504612002011-08-10T10:30:00-07:002011-08-10T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking</h1>
<div class='date'><time class="dtstart dt-start" title="2011-08-10T10:30:00" datetime="2011-08-10T10:30:00">Wednesday, August 10, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-08-10T11:30:00" datetime="2011-08-10T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Kristin Rozier</p>
<p>Formal behavioral specifications written early in the system-design
process and communicated across all design phases have been shown to
increase the efficiency, consistency, and quality of the system under
development. To prevent introducing design or verification errors, it is
crucial to test specifications for satisfiability. Our focus here is on
specifications expressed in linear temporal logic (LTL).</p>
<p>We introduce a novel encoding of symbolic transition-based Buchi
automata and a novel, ``sloppy,'' transition encoding, both of which
result in improved scalability. We also define novel BDD variable
orders based on tree decomposition of formula parse trees. We describe
and extensively test a new multi-encoding approach utilizing these novel
encoding techniques to create 30 encoding variations. We show that our
novel encodings translate to significant, sometimes exponential,
improvement over the current standard encoding for symbolic LTL
satisfiability checking.</p>
<p>Details can be found here: <a href="http://ti.arc.nasa.gov/profile/kyrozier/">http://ti.arc.nasa.gov/profile/kyrozier/</a>.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/8/8/tech-talk-a-multi-encoding-approach-for-ltl-symbolic-satisfi.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461200.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461200/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Monday, August 8, 2011 at 9:29am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504612332011-08-19T15:18:26-07:002011-08-22T07:29:33-07:00Tech Talk: Modular verification of preemptive OS kernelsTuesday, August 23, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504612332011-08-23T10:30:00-07:002011-08-23T11:30:00-07:00<div class="vevent">
<h1 class="summary">Tech Talk: Modular verification of preemptive OS kernels</h1>
<div class='date'><time class="dtstart dt-start" title="2011-08-23T10:30:00" datetime="2011-08-23T10:30:00">Tuesday, August 23, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-08-23T11:30:00" datetime="2011-08-23T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Alexey Gotsman</p>
<p>Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK).</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2011/8/19/tech-talk-modular-verification-of-preemptive-os-kernels.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461233.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461233/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Friday, August 19, 2011 at 3:18pm</strong> and last updated <br /><strong>Monday, August 22, 2011 at 7:29am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504617952012-01-03T10:19:17-08:002012-01-03T10:19:17-08:00Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic FrameworkTuesday, January 10, 2012 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504617952012-01-10T10:30:00-08:002012-01-10T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework</h1>
<div class='date'><time class="dtstart dt-start" title="2012-01-10T10:30:00" datetime="2012-01-10T10:30:00">Tuesday, January 10, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-01-10T11:30:00" datetime="2012-01-10T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by David Lazar</p>
<p>Formal semantics is notoriously hard. The K semantic framework (<a href="http://k-framework.org/">http://k-framework.org/</a>) is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K.
The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-week-formalizing-haskell-98-in.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/haskell">haskell</a>, <a class="p-category" href="/events/tag/semantics">semantics</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461795.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461795/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, January 3, 2012 at 10:19am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504618002012-01-04T13:38:43-08:002012-01-04T13:38:43-08:00Galois Tech Talk (2 of 3 next week!): Model-based Code Generation and Debugging of Concurrent ProgramsWednesday, January 11, 2012 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504618002012-01-11T10:30:00-08:002012-01-11T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk (2 of 3 next week!): Model-based Code Generation and Debugging of Concurrent Programs</h1>
<div class='date'><time class="dtstart dt-start" title="2012-01-11T10:30:00" datetime="2012-01-11T10:30:00">Wednesday, January 11, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-01-11T11:30:00" datetime="2012-01-11T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Borzoo Bonakdarpour.</p>
<p>Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.</p>
<p>The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2012/1/4/galois-tech-talk-2-of-3-next-week-model-based-code-generatio.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/concurrency">concurrency</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461800.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461800/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Wednesday, January 4, 2012 at 1:38pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504618082012-01-05T17:24:27-08:002012-01-05T17:24:27-08:00Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.Thursday, January 12, 2012 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504618082012-01-12T10:30:00-08:002012-01-12T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.</h1>
<div class='date'><time class="dtstart dt-start" title="2012-01-12T10:30:00" datetime="2012-01-12T10:30:00">Thursday, January 12, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-01-12T11:30:00" datetime="2012-01-12T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Julien Schmaltz.</p>
<p>Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2012/1/5/galois-tech-talk-33-next-week-on-deadlock-verification-in-mi.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/hardware">hardware</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a>, <a class="p-category" href="/events/tag/verification">verification</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461808.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461808/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, January 5, 2012 at 5:24pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504619162012-01-31T17:57:30-08:002012-01-31T17:57:30-08:00Galois Tech Talk: Efficient Implementation of Property Directed ReachabilityMonday, February 6, 2012 from 10-11am at Galois, Inchttp://calagator.org/events/12504619162012-02-06T10:00:00-08:002012-02-06T11:00:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Efficient Implementation of Property Directed Reachability</h1>
<div class='date'><time class="dtstart dt-start" title="2012-02-06T10:00:00" datetime="2012-02-06T10:00:00">Monday, February 6, 2012 from 10</time>–<time class="dtend dt-end" title="2012-02-06T11:00:00" datetime="2012-02-06T11:00:00">11am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Alan Mishchenko.</p>
<p>Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2012/1/31/tech-talk-efficient-implementation-of-property-directed-reac.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/model checking">model checking</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461916.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461916/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, January 31, 2012 at 5:57pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504627802012-08-24T10:05:27-07:002012-08-24T10:05:27-07:00Galois Tech Talk: Formal Verification of Monad Transformers Thursday, August 30, 2012 from 11am-noon at Galois, Inchttp://calagator.org/events/12504627802012-08-30T11:00:00-07:002012-08-30T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Formal Verification of Monad Transformers </h1>
<div class='date'><time class="dtstart dt-start" title="2012-08-30T11:00:00" datetime="2012-08-30T11:00:00">Thursday, August 30, 2012 from 11am</time>–<time class="dtend dt-end" title="2012-08-30T12:00:00" datetime="2012-08-30T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Brian Huffman.</p>
<p>We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2012/8/24/tech-talk-formal-verification-of-monad-transformers.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/Isabelle">Isabelle</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/functional programming">functional programming</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/haskell">haskell</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250462780.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250462780/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Friday, August 24, 2012 at 10:05am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504629422012-10-09T09:58:35-07:002012-10-09T09:58:35-07:00Galois Tech Talk: Towards a Formally Verified Component PlatformTuesday, October 16, 2012 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504629422012-10-16T10:30:00-07:002012-10-16T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Towards a Formally Verified Component Platform</h1>
<div class='date'><time class="dtstart dt-start" title="2012-10-16T10:30:00" datetime="2012-10-16T10:30:00">Tuesday, October 16, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-10-16T11:30:00" datetime="2012-10-16T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Matthew Fernandez.</p>
<p>In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2012/10/9/tech-talk-towards-a-formally-verified-component-platform.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/OS design">OS design</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/kernels">kernels</a>, <a class="p-category" href="/events/tag/l4">l4</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250462942.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250462942/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, October 9, 2012 at 9:58am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504635282013-02-06T10:01:29-08:002013-02-06T10:01:29-08:00Galois Tech Talk: Automatic Function Annotations for Hoare LogicTuesday, February 12, 2013 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504635282013-02-12T10:30:00-08:002013-02-12T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Automatic Function Annotations for Hoare Logic</h1>
<div class='date'><time class="dtstart dt-start" title="2013-02-12T10:30:00" datetime="2013-02-12T10:30:00">Tuesday, February 12, 2013 from 10:30</time>–<time class="dtend dt-end" title="2013-02-12T11:30:00" datetime="2013-02-12T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Daniel Matichuk.</p>
<p>Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2013/2/6/tech-talk-automatic-function-annotations-for-hoare-logic.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250463528.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250463528/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Wednesday, February 6, 2013 at 10:01am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504637492013-02-28T18:09:56-08:002013-02-28T18:09:56-08:00Galois Tech Talk: Parametricity, Quotient types, and Theorem transferTuesday, March 5, 2013 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504637492013-03-05T10:30:00-08:002013-03-05T11:30:00-08:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Parametricity, Quotient types, and Theorem transfer</h1>
<div class='date'><time class="dtstart dt-start" title="2013-03-05T10:30:00" datetime="2013-03-05T10:30:00">Tuesday, March 5, 2013 from 10:30</time>–<time class="dtend dt-end" title="2013-03-05T11:30:00" datetime="2013-03-05T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Brian Huffman.</p>
<p>A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadler-style "free theorems" about a polymorphic function from its type; e.g. rev :: [a] -> [a] must satisfy map f (rev xs) = rev (map f xs).</p>
<p>In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using types-as-binary-relations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://corp.galois.com/blog/2013/2/28/tech-talk-parametricity-quotient-types-and-theorem-transfer.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250463749.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250463749/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, February 28, 2013 at 6:09pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504643792013-06-06T18:06:56-07:002013-06-06T18:06:56-07:00Galois Tech Talk: Non-interference and Binary Correctness of seL4Friday, June 14, 2013 from 11am-noon at Galois, Inchttp://calagator.org/events/12504643792013-06-14T11:00:00-07:002013-06-14T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Non-interference and Binary Correctness of seL4</h1>
<div class='date'><time class="dtstart dt-start" title="2013-06-14T11:00:00" datetime="2013-06-14T11:00:00">Friday, June 14, 2013 from 11am</time>–<time class="dtend dt-end" title="2013-06-14T12:00:00" datetime="2013-06-14T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Gerwin Klein and Thomas Sewell.</p>
<p>This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.</p>
<p>The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.</p>
<p>The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2013/6/6/tech-talk-non-interference-and-binary-correctness-of-sel4.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/kernels">kernels</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250464379.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250464379/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, June 6, 2013 at 6:06pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504705412016-07-07T08:41:07-07:002016-07-07T08:41:07-07:00Galois Tech Talk: Hoare Monitor Programming Revisited : Safe and Optimized ConcurrencyTuesday, July 12, 2016 from 11am-noon at Galois, Inchttp://calagator.org/events/12504705412016-07-12T11:00:00-07:002016-07-12T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Hoare Monitor Programming Revisited : Safe and Optimized Concurrency</h1>
<div class='date'><time class="dtstart dt-start" title="2016-07-12T11:00:00" datetime="2016-07-12T11:00:00">Tuesday, July 12, 2016 from 11am</time>–<time class="dtend dt-end" title="2016-07-12T12:00:00" datetime="2016-07-12T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>abstract:</p>
<p>Hoare monitors, invented by Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, and how it is possible to improve runtime efficiency and parallelism of Tower-generated C programs by releasing some constraints on the Hoare monitor model. Finally, some test results on SMACCMPilot, a high-assurance autopilot, will be presented.</p>
<p>bio:</p>
<p>Georges-Axel Jaloyan is a CS student at École Normale Supérieure in Paris. He is interning at Galois as part of his Master’s degree. He is interested in embedded systems security and safety-critical systems. He interned previously at NASA Langley Safety Critical Avionics Systems Branch.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://galois.com/blog/2016/07/tech-talk-hoare-monitor-programming-revisited-safe-optimized-concurrency/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/Galois tech talk">Galois tech talk</a>, <a class="p-category" href="/events/tag/concurrency">concurrency</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250470541.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250470541/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, July 7, 2016 at 8:41am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504740362018-07-24T15:08:28-07:002018-07-24T15:08:28-07:00Galois Tech Talk: The Lean Theorem Prover: Past, Present and FutureFriday, August 3, 2018 from 11am-noon at Galois Inchttp://calagator.org/events/12504740362018-08-03T11:00:00-07:002018-08-03T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: The Lean Theorem Prover: Past, Present and Future</h1>
<div class='date'><time class="dtstart dt-start" title="2018-08-03T11:00:00" datetime="2018-08-03T11:00:00">Friday, August 3, 2018 from 11am</time>–<time class="dtend dt-end" title="2018-08-03T12:00:00" datetime="2018-08-03T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202394717' class='url'>
<span class='fn org'>Galois Inc</span>
</a>
<div class="adr">
<div class="street-address">421 Sw 6th Ave Ste 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20Sw%206th%20Ave%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Abstract:
Lean is an interactive theorem prover and functional programming language. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean has parallel compilation and checking of proofs, and provides a server mode that supports a continuous compilation and rich user interaction in editing environments such as Visual Studio Code, Monaco, Emacs, and Vim. In the first part of this talk, we provide a short introduction to Lean, its applications, and its metaprogramming framework. We also describe how this framework extends Lean’s object language with an API to many of Lean’s internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is efficient, and that it provides a convenient and flexible way of writing not only metaprograms and small-scale interactive tactics, but also more substantial kinds of automation. In the second part, we describe our plans for the system, and what we are currently working on.</p>
<p>More information about Lean can be found at <a href="http://leanprover.github.io">http://leanprover.github.io</a>. The interactive book “Theorem Proving in Lean” is the standard reference for Lean. The book is available in PDF and HTML formats. In the HTML version, all examples and exercises can be executed in the reader’s web browser.</p>
<p>Bio:
I’m a Principal Researcher in the RiSE group at Microsoft Research. I joined Microsoft in 2006, before that I was a Computer Scientist at SRI International. I obtained my PhD at PUC-Rio in 2000. My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I’m the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is an open source theorem prover and programming language. Sebastian Ullrich and I are currently developing the next version (Lean 4). Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. Z3 has been open sourced (under the MIT license) in the beginning of 2015. I received the Haifa Verification Conference Award in 2010. In 2014, the TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) has given an award for “The most influential tool paper in the first 20 years of TACAS” to the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science. In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN. In 2017, the International Conference on Automated Deduction (CADE) presented the Skolem Award for my paper “Efficient E-Matching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field. In 2018, the ETAPS conference has given the test of time award to the Z3 paper: Z3: An Efficient SMT Solver. You can see more about me at <a href="https://leodemoura.github.io/about.html">https://leodemoura.github.io/about.html</a></p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://galois.com/blog/2018/07/the-lean-theorem-prover-past-present-and-future/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/computer science">computer science</a>, <a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/lean">lean</a>, <a class="p-category" href="/events/tag/theorem proving">theorem proving</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250474036.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250474036/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, July 24, 2018 at 3:08pm</strong>.
</div>
</div>
</div>
45.5208 -122.6779