Tech Talk: A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking

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.

Tech talk video: Parallel K-Induction Based Model Checking

We are pleased to announce the availability of a new tech talk video: "Parallel K-Induction Based Model Checking", presented by Temesghen Kahsai. More details about the talk are available on the announcement page.

For more videos of our technical seminars, please visit our Vimeo channel.

Galois is Hiring!

Do you want to lead the development of the next generation of embedded systems that transform how we interact with the physical world? Do you want to make secure cloud computing a reality? Can you help us develop and exploit secure, ubiquitous networked devices?

Galois has a position open for a senior computer scientist in our Portland office.  This individual will support existing research programs and internal research and development efforts and provide technical leadership in the development of new capabilities and business opportunities.  Such leadership may include development of new R&D efforts and expansion of existing efforts.  The candidate should be an experienced and recognized researcher in the field capable of envisioning, designing and leading new R&D efforts and large, complex programs.

Click here for more information. 

Tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:Combining Denotational and Operational Semantics for Scalable Proof Development

speakers:Adam Foltzer

time:Tuesday, 19 July 2011, 10:30am

location:

Galois Inc.

421 SW 6th Ave. Suite 300,

Portland, OR, USA

(3rd floor of the Commonwealth building)

abstract:Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.

This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.

This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.

bio: Adam Foltzer is an Intern at Galois, Inc. and a Master's student at Indiana University studying programming languages.

Tech talk: Parallel K-induction based Model Checking

Galois is pleased to host the following tech talk.
These talks are open to the interested public. Please join us!

title:
Parallel K-induction based Model Checking

speakers:
Temesghen Kahsai

time:
Tuesday, 12 July 2011, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:
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.

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.

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.

bio:
Temesghen Kahsai is a postdoc research scholar at the University of Iowa. He recevied a BSc and an MSc in Computer Science from the University of Udine (Italy) and a Ph.D. in Computer Science from Swansea University (Wales). His research interests include formal specification languages, software verification, specification-based testing and interactive theorem proving. Currently, he is working on SMT-based model checking for synchrouns systems. His publications and other information can be found at www.cs.uiowa.edu/~tkahsaiazene