Profile

Cover photo
Galois, Inc.
160 followers|90,710 views
AboutPostsPhotosYouTube

Stream

Galois, Inc.

Shared publicly  - 
 
Join us this week for a tech talk.

Isaac Potoczny-Jones's talk, "E3DB – Tozny’s End-to-End Encrypted Database", will be at 11am on Wednesday. Details here: https://galois.com/blog/2016/12/tech-talk-e3db-toznys-end-end-encrypted-database/
abstract: Project E3DB is a tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. We are providing a command-line client for you to play with and a Java SDK to prototype with. Over the next few weeks, we’ll be getting feedback from you, adding features, and making it …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us next week for a tech talk.

Georges-Axel Jaloyan's talk, "Hoare Monitor Programming Revisited : Safe and Optimized Concurrency", will be at 11am on Tuesday. Details here: https://galois.com/blog/2016/07/tech-talk-hoare-monitor-programming-revisited-safe-optimized-concurrency/
abstract: Hoare monitors, invented by Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, and …
2
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us for two tech talks this week.

The first talk is on Thursday, March 24th, at 1:30PM by Kristin Yvonne Rozier, "Design-Time Formal Verification for Full-Scale Automated Air Traffic Control": http://galois.com/blog/2016/03/tech-talk-design-time-formal-verification-for-full-scale-automated-air-traffic-control/

The second talk is on Friday, March 25th, at 10:30AM by Eric Rozier, "Adversarial Machine Learning, Privacy, and Cybersecurity in the Age of Data Science": http://galois.com/blog/2016/03/tech-talk-adversarial-machine-learning-privacy-and-cybersecurity-in-the-age-of-data-science/
abstract: We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us Tuesday, December 8th, at 11am for a talk by R. Andrew Goodwin, "Individual and Group Decision-making in Open Environments from an Ecological Point of View"

Details on the talk here: http://galois.com/blog/2015/12/tech-talk-individual-and-group-decision-making-in-open-environments-from-an-ecological-point-of-view/
abstract: Animal movement is driven by responses to both social and non-social factors of the environment. Research across species shows that animals do not make decisions based solely on present information, e.g., at time t, but on an integrated assessment of information over recent time, e.g., t-1, t-2, etc. This raises the conundrum of how …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us on Wednesday, August 12th, at 11am for a talk by Robby, "Evidence-based Trust of Symbolic Execution-based Verification"

Details on the talk here:
http://galois.com/blog/2015/08/tech-talk-evidence-based-trust-symbolic-execution-based-verification/
abstract: Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us next week, July 27th at 11am, for a talk by Josh Benaloh, "A Brief History of Verifiable Elections".

Details on the talk here:
http://galois.com/blog/2015/07/tech-talk-brief-history-verifiable-elections/
abstract: Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us next week for a tech talk.

Charles Consel's talk, "Internet of Things: From Small- to Large-Scale Orchestration", will be at 11am on Tuesday the 30th.

Details here: https://galois.com/blog/2016/08/tech-talk-internet-things-small-large-scale-orchestration/
abstract: The domain of Internet of Things (IoT) is rapidly expanding beyond research and becoming a major industrial market with such stakeholders as major manufacturers of chips and connected objects, and fast-growing operators of low-power wide-area networks. Importantly, this emerging domain is driven by applications that leverage the infrastructure to provide users with innovative, high-value …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us for a tech talk this week.

June Andronick's talk, "Interrupts in OS code: let’s reason about them. Yes, this means concurrency", will be at 11am on Wednesday. Details here: 
https://galois.com/blog/2016/05/tech-talk-interrupts-in-os-code-lets-reason-about-them-yes-this-means-concurrency/
abstract: Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us Friday, March 18th, at 10:30am for a talk by James Caldwell, "Toward Extracting Monadic Programs from Proofs"

Details on the talk here: http://galois.com/blog/2016/03/tech-talk-toward-extracting-monadic-programs-from-proofs/
abstract: The Curry-Howard Isomorphism motivates the well known proofs-as-programs interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a -> (a -> M b) -> …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us Wednesday, November 11th, at 11am for a talk by Chris Casinghino, "Designing a practical dependently typed language"

Details on the talk here: http://galois.com/blog/2015/11/tech-talk-designing-a-practical-dependently-typed-language/
abstract: The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In …
1
Add a comment...

Galois, Inc.

Shared publicly  - 
 
Join us tomorrow, July 30th at 2pm, for a talk by Alex Summers, "Viper: Verification Infrastructure for Permission-based Reasoning".

Details on the talk here:
http://galois.com/blog/2015/07/tech-talk-viper-verification-infrastructure-permission-based-reasoning/
abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from …
1
Add a comment...
Story
Tagline
Advancing computer science: developing software to solve your hardest problems.
Introduction
Galois specializes in the research and development of new technologies that solve the most difficult problems in computer science. We are passionate about the trustworthiness of critical systems, and work to ensure that the systems you depend on work as intended, and only as intended. Our team works closely with clients to achieve a balance between the privacy/cost/speed challenges involved in making systems more trustworthy.

We care deeply about real-world use of our R&D efforts and work diligently to transition them into use. Many of our researchers joined Galois from academia and elsewhere in pursuit of more impact. Our clients, like those listed at the bottom of the page, derive value working with us as trusted advisors, and hold us to high standards for the actual production of algorithms and code that embody our work together.

Galois is a privately held U.S.-owned and -operated company established in 1999 in Portland, Oregon. We were founded on core principles that are central to how we function. We believe that we can and should derive joy from our work, be authentic and trustworthy in all of our interactions, and cherish the opportunity to develop and steward new technology.
Contact Information
Contact info
Phone
503.626.6616
Email
Fax
503.350.0833
Address
421 SW 6th Avenue, Suite 300 Portland, OR 97204