Galois, Inc. is pleased to announce the immediate release of the Haskell Lightweight Virtual Machine (or HaLVM), version 1.0. The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” Internally, Galois has used this system in several projects with much success, and we […]

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

title:

The Rubinius Virtual Machine

speaker:

Brian Ford

time:

10:30am, Tuesday, 30 November 2010

location:

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

abstract:

Ruby is a highly dynamic, strongly-typed programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it well-suited for embedded domain-specific languages. Ruby was popularized by the Ruby on Rails web development framework.The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk-80 virtual machine described in the Blue book (“Smalltalk-80: the language and its implementation” by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and just-in-time (JIT) compilers. Rubinius currently features a stack-oriented opcode virtual machine, generational garbage collector, and LLVM-based JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby.We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius.

bio:

Brian Ford began contributing to the Rubinius project in December 2006 shortly after the creator, Evan Phoenix, announced the project. He is presently employed by Engine Yard, Inc to work full-time on Rubinius. Brian is keenly interested in languages of all kinds, from mathematics and various programming languages to Spanish and Japanese. He has primarily used C/C++, Tcl, Python, and Ruby in Geographic Information Systems, physical security systems monitoring and web application development. He has a B.Sc. in Mathematics from Portland State University.

We are pleased to announce the availability of a new Galois tech talk video: “Copilot: A Hard Real-Time Runtime Monitor”, presented by Lee Pike. More details about the talk are available on the announcement page.

Copilot: A Hard Real-Time Runtime Monitor 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:

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.

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.

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.