A month or so ago, I gave talks at SRI and NASA Ames on 11+ Years of Formal Methods at Galois (pdf). Though I haven't been around the whole time, it was fun to reminisce on the projects I've helped with and to highlight my colleagues' work!
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.
Galois, Inc. | Thursday, July 14, 2011 at 12:54PM | in Events, Formal Methods, Functional Programming, Tech Talks 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.
On May 10 Joe Hurd gave a guest lecture at Portland State University, as part of Bart Massey's Computer Science course on Combinatorial Games. The topic of the guest lecture was "Formally Verified Endgame Tables", and Joe showed how Formal Methods can be used to prove that endgame tables used by computer chess programs are correct with respect to the laws of chess. The slides of the guest lecture are available for download.
Galois, Inc. | Tuesday, January 18, 2011 at 2:58PM | in Domain Specific Languages, Formal Methods, Functional Programming Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers -- extensions to SAT solvers with support for variables of non-boolean type -- offer powerful automation for solving a variety of assurance problems in software. We use them, for example, in Cryptol, to prove the equivalence (or otherwise) of algorithm implementations.
For a while now, Galois has been interested in connecting automated solvers to our programming language of choice, Haskell, to make it possible to prove automatically some properties of our functions (rather than just testing, e.g. with QuickCheck). We've pushed two efforts out this week, as previews of what we're thinking in this space:
Both are embedded DSLs for representing propositions to an SMT solver via Haskell functions and values. They take different approaches (a compiler from Haskell to the SMT-LIB format, versus an interpreter for the Yices SMT solver). SBV is the more mature package, while yices-painless emphasizes a type-preserving translation from a minimal core language. SBV was built by Levent Erkok, yices-painless by Don Stewart. Documentation for the design of yices-painless is available, as is documentation on SBV.
Both are ready for experimentation and feedback, and we welcome your comments.