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

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

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title: The OpenTheory Standard Theory Library   speaker: Joe Hurd   time: Tuesday, 12 April 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300,Portland, OR, USA(3rd floor of the Commonwealth building)   abstract:Interactive […]

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   Please note the unusual time slot for this talk: it is on Monday, 7 February 2011, at 4:30pm (changed from 1:30pm due to flight delays).   title: The Strategy Challenge in Computer Algebra   presenter: Grant […]

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title:  Verifying seL4-based Systems   presenter: Simon Winwood   time: Tuesday, 01 February 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)   abstract:   In […]

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

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title: Program Inconsistency Detection using Weakest Preconditions   presenter: Aaron Tomb   time: Tuesday, 25 January 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)   abstract:  Many tools […]

NASA has awarded Galois, Inc. a Small Business Innovation Research award to conduct research into the application of formal verification to machine learning systems. From the abstract: Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are […]

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.

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

title:

Introduction to Logic Synthesis (slides, video)

speaker:

Alan Mishchenko, University of California, Berkeley

time:

10:30am, Friday 08 October 2010

location:

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

abstract:

The lecture describes the problems solved by logic synthesis. It presents functional representations and typical computations applied to Boolean networks, such as traversal, windowing, cut computation, simulation, Boolean reasoning. Presented next are And-Inverter Graphs (AIGs) that are increasingly used as a unifying representation for all problems. The lecture is finished by an overview of AIG-based solutions in synthesis, technology mapping, and formal verification.

bio:

Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998.  Currently, Alan is an Associate Researcher at University of California, Berkeley.  His research interests are in developing computationally efficient methods for logic synthesis and verification.