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.

We are pleased to announce the availability of a new Galois tech talk video: “Databases are Categories 2: Refinements and Extensions”, presented by David Spivak. More details about the talk are available on the announcement page.

Databases are Categories 2: Refinements and Extensions from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

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.

We are pleased to announce the availability of a new Galois tech talk video: “Fides: Remote Anomaly-Based Cheat Detection Using Client Emulation”, presented by Wu-chang Feng. More details about the talk are available on the announcement page.

Fides: Remote Anomaly-Based Cheat Detection Using Client Emulation from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

We are pleased to announce the availability of a new Galois tech talk video: “Application of Computer Algebra Techniques in Verification of Galois Field Multipliers: Potential + Challenges”, presented by Priyank Kalla . More details about the talk are available on the announcement page.

Verification of Galois Field Multipliers from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

We are pleased to announce the availability of a new Galois tech talk video: “Introduction to Logic Synthesis”, presented by Alan Mishchenko. More details about the talk are available on the announcement page.

Introduction to Logic Synthesis from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

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.

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

title:

Fides: Remote Anomaly-Based Cheat Detection Using Client Emulation (slides, video)

speaker:

Prof. Wu-chang Feng

time:

10:30am, Tuesday 19 October 2010

location:

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

abstract:

As a result of physically owning the client machine, cheaters in online games currently have the upper-hand when it comes to avoiding detection. To address this problem and turn the table on cheaters, this paper presents Fides, an anomaly-based cheat detection approach that remotely validates game execution. With Fides, a server-side Controller specifies how and when a client-side Auditor measures the game. To accurately validate measurements, the Controller partially emulates the client and collaborates with the server. This paper examines a range of cheat methods and initial measurements that counter them, showing that a Fides prototype is able to efficiently detect several existing cheats, including one state-of-the-art cheat that is advertised as undetectable.

bio:

Wu-chang Feng is currently an Associate Professor in the Intel Systems and Networking Laboratory at Portland State University where he leads a research group in networking and security. Wu-chang received his B.S. in 1992 from Penn State University and his M.S.E. and Ph.D. degrees in 1994 and 1999 from the University of Michigan. He was awarded the IEEE Communications Society 2003 William R. Bennett prize as well as one of four prizes recognizing the Best IBM Research Papers in Computer Science, Electrical Engineering and Math published in 2002.

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

title:

Application of Computer Algebra Techniques in Verification of Galois Field Multipliers: Potential + Challenges

speaker:

Priyank Kalla

time:

10:30am, Tuesday 12 October 2010

location:

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

abstract:

Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others.My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the word-length (k) in such multipliers can be very large: typically, k = 256. Due to such large word-lengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome.

bio:

Priyank Kalla recieved the Bachelors degree in Electronics engineering from Sardar Patel University in India in 1993; and Masters and PhD from University of Massachusetts Amherst in 1998 and 2002, respectively. Since 2002, he is a faculty member in the ECE Dept. at the Univ. of Utah. His research interests are in the general areas of Logic Synthesis and Design Verification. Over the past few years, he has been investigating the use of computer algebra techniques over finite integer rings (Z/mZ) and finite fields (GF(2^m)) for optimization and verification of arithmetic datapaths. He is a recepient of the NSF CAREER award and the ACM TODAES 2009 best paper award. For more information, visit http://www.ece.utah.edu/~kalla

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.