Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">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 p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-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-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 u-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>