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 AveSte 300Portland, OR 97204(3rd floor of the Commonwealth building)  […]

Read More

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 […]

Read More

ZUC in Cryptol

ZUC is a stream cipher that is proposed for inclusion in the “4G” mobile standard named LTE (Long Term Evolution), the future of secure GSM. The proposal is actually comprised several different algorithms: A stream cipher named ZUC, LTEencryption algorithm (128-EEA3), based on ZUC, LTEintegrity algorithm (128-EIA3), which is a hash function using ZUC as […]

Read More

Formally Verified Chess Endgames

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 […]

Read More

Merging SMT solvers and programming languages

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 […]

Read More

Tech talk: Formal Methods Applied to Control Software

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

title:
Formal Methods Applied to Control Software
speaker:
Alwyn Goodloe
time:
10:30am, Tuesday, 16 November 2010
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Critical cyber-physical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the Frama-C tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers.
bio:
Alwyn Goodloe obtained his B.Sc. in Computer Science from Old Dominion University in 1985 and an M.Sc. in Mathematics from George Mason University in 1992. He worked for fourteen years in the software industry as a software engineer, database administrator, Unix system administrator, and technologist. In 1999, he returned to graduate school to study at the University of Pennsylvania, where he obtained a Ph.D. in Computer and Information Science in 2008. At Penn he conducted research in the area of computer and network security. He is currently a research scientist at the National Institute of Aerospace in Hampton, Virginia. At NIA his research focus has been formal methods applied to high-reliable systems such as avionics.
Read More

Tech Talk: Copilot: A Hard Real-Time Runtime Monitor

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

title:
Copilot: A Hard Real-Time Runtime Monitor (slides, video)
speaker:
Lee Pike
time:
10:30am, Tuesday, 9 November 2010
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
We address the problem of runtime monitoring for hard real-time programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos.
bio:
Lee Pike has worked in Research & Development at Galois, Inc. since 2005. His primary area of research is dependable embedded systems, including both safety-critical and security-critical systems. Previously, he was a research scientist with the NASA Langley Formal Methods Group. He has a Ph.D in Computer Science from Indiana University. He has a Best Paper award from Formal Methods in Computer-Aided Design (FMCAD’2007), and service includes being on the program committees of FMCAD and Interactive Theorem Proving. His publications and other information can be found at http://www.cs.indiana.edu/~lepike.
Read More

Cryptol Course: High-assurance Cryptographic Development Using the Cryptol Workbench

Galois is offering a four‐day Cryptol course for those interested in exploring the capabilities of the Cryptol workbench.The course is highly participatory: we will work on a series of exercises for each new topic, using the Cryptol toolset interactively. Prospective participants should have experience writing programs and some knowledge of cryptography. Those who complete the course will have the skills necessary to develop high‐assurance, high‐performance cryptographic algorithms in Cryptol. A tentative outline and further information can be found in the course flyer. Interested parties should contact Dr. Sally Browning via e-mail at sally@galois.com, or call her at (503) 808 7151.

Read More

Tech Talk: Databases are Categories 2: Refinements and Extensions.

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 an unusual day and time, Friday, at 3:30pm.

title:
Databases are Categories 2: Refinements and Extensions. (slides,video)
speaker:
David Spivak
time:
3:30pm, Friday, 22 October 2010
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
About five months ago I gave a talk here at Galois called “Databases are categories.” The basic idea was that a database schema can be represented as a category C and its states can be represented as functors C–>Set. In this talk I’ll refine that notion a bit, explaining that schemas are better represented as sketches. I’ll also show how, within this model one can: deal with incomplete data; incorporate typing and calculated fields; and perform queries, define views, and migrate data between disparate schemas. That is, I’ll try to show that the categorical approach handles everything one might hope it would. Finally, I’ll discuss a linguistic version of categories, called “ologs,” and show how they may help to democratize information storage.
bio:
I received my PhD in mathematics from UC Berkeley in 2007; my thesis was in Algebraic Topology. For the next three years I was a post doc in the math department at the University of Oregon. During this time my focus moved toward using category theory to understand information and communication. This past summer (2010) I began a post doc in the math department at MIT. My main interest at the moment is in using category theory to bridge the gap between disparate academic fields, and to generally enhance our ability to record, process, and communicate information.
Read More

Monitoring Distributed Real-Time Systems: A Survey and Future Directions

Monitoring Distributed Real-Time Systems: A Survey and Future DirectionsAlwyn Goodloe (NIA) and Lee Pike (Galois, Inc), NASA Langley Research Center, 2010.

Runtime monitors have been proposed as a means to increase the reliability of safety-critical systems. In particular, we explore runtime monitors for distributed hard real-time systems, such as fault-tolerant data buses and control systems for avionics and spacecraft. This class of systems has had little attention from the monitoring community. We motivate the need for monitors by discussing examples of avionic systems failure. We then describe work in the field of runtime monitoring. We present potential monitoring architectures for distributed real-time systems, and then we discuss how those architectures might be used to monitor properties of real-time distributed systems.

Read More