BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20110313T020000 RDATE:20110313T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110808T162902Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110810T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110810T103000 DTSTAMP;VALUE=DATE-TIME:20110808T162902Z LAST-MODIFIED;VALUE=DATE-TIME:20110808T162902Z UID:http://calagator.org/events/1250461200 DESCRIPTION:Presented by Kristin Rozier \;\n \;\nFormal behavioral specifications written early in the system-design \;\nprocess and com municated across all design phases have been shown to \;\nincrease th e efficiency\, consistency\, and quality of the system under \;\ndev elopment. To prevent introducing design or verification errors\, it is&# 13\;\ncrucial to test specifications for satisfiability. Our focus here is on \;\nspecifications expressed in linear temporal logic (LTL). 3\;\n \;\nWe introduce a novel encoding of symbolic transition-based Buchi \;\nautomata and a novel\, ``sloppy\,'' transition encoding\, b oth of which \;\nresult in improved scalability. We also define nove l BDD variable \;\norders based on tree decomposition of formula pars e trees. We describe \;\nand extensively test a new multi-encoding ap proach utilizing these novel \;\nencoding techniques to create 30 enc oding variations. We show that our \;\nnovel encodings translate to s ignificant\, sometimes exponential\, \;\nimprovement over the current standard encoding for symbolic LTL \;\nsatisfiability checking. \ ;\n \;\nDetails can be found here: http://ti.arc.nasa.gov/profile/kyr ozier/.\n\nTags: galois\, tech talk\, formal methods\n\nImported from: h ttp://calagator.org/events/1250461200 URL:http://corp.galois.com/blog/2011/8/8/tech-talk-a-multi-encoding-appro ach-for-ltl-symbolic-satisfi.html SUMMARY:Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Sati sfiability Checking LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR