|
Change #10307
2011-08-08
09:29:02
|
create
Calagator::Event
1250461200
Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking
Roll back
| description |
nil |
→ |
Presented by Kristin Rozier
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).
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.
Details can be found here: http://ti.arc.nasa.gov/profile/kyrozier/. |
| end_time |
nil |
→ |
2011-08-10 11:30:00 -0700 |
| id |
nil |
→ |
1250461200 |
| start_time |
nil |
→ |
2011-08-10 10:30:00 -0700 |
| title |
nil |
→ |
Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking |
| url |
nil |
→ |
http://corp.galois.com/blog/2011/8/8/tech-talk-a-multi-encoding-approach-for-ltl-symbolic-satisfi.html |
| venue_id |
nil |
→ |
202390439 |
|