Galois is pleased to host the following tech talk.
These talks are open to the interested public. Please join us!
Please note that this talk is on Wednesday!
title:
A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking
speakers:
Kristin Rozier
time:
10 August 2011, Wednesday, 10:30 A.M.
location:
Galois, Inc.
421 SW 6th Ave
Ste 300
Portland, OR 97204
(3rd floor of the Commonwealth building)
abstract:
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/.
bio:
Kristin Yvonne Rozier is a Research Computer Scientist in the Robust
Software Engineering group at NASA Ames Research Center. Her primary
research interests include model checking, automata theory, mathematical
logic, automated reasoning, and algorithms. Currently, Kristin is
contributing research to the Airspace Systems Program, focusing on
automated techniques for formal verification of safety critical software
systems. Kristin has been at NASA since 2001. She earned a B.S. in 2000
and an M.S. in 2001 from The College of William and Mary, and is
currently a PhD candidate at Rice University under the advisement of
Moshe Y. Vardi. She has received the American Helicopter Society’s
Howard Hughes Award and the NASA Group Achievement Award.