Aaron Tomb recently gave an interview with the Machine Intelligence Research Institute (MIRI) about what Galois is doing on DARPA’s Crowd Sourced Formal Verification (CSFV) program to crowd-source the problem of software verification. Read the article here: http://intelligence.org/2014/05/29/aaron-tomb/

Galois is pleased to host the following tech talk. These talks are open to the interested public–please join us! (There is no need to pre-register for the talk.) Please note the unusual time for this talk. It is on Thursday at 11am. title: Formal Verification of Monad Transformers speaker: Brian Huffman time: Thursday, 30 August […]

Galois is pleased to host the following tech talk. These talks are open to the interested public–please join us! (There is no need to pre-register for the talk.) Please note the unusual time for this talk, it is on Thursday, 12 January 2012 title: On deadlock verification in micro-architectural models of communication fabrics. speaker: Julien […]

Galois is pleased to announce the following tech talk.These talks are open to the interested public.  speaker:Alexey GotsmanIMDEA Software Institute, Madrid, Spain time:23 August 2011, 10:30 A.M. location:Galois, Inc.421 SW 6th Ave.Ste 300Portland, OR 97007(3rd floor of the Commonwealth Building)  abstract:Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for […]

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 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

We have a new position paper on the use of EDSLs (LwDSLs) for verification and validation of unmanned vehicle avionics, written jointly with John van Enk of DornerWorks, recently presented at a mixed-criticality architecture conference. (Download) :: PDF

Lee Pike, Don Stewart, John Van EnkCPS Week 2009 Workshop on Mixed CriticalityRoadmap to Evolving UAV Certification

We outline a new approach to the verification and validation (V & V) of safety-critical avionics based on the use of executable lightweight domain specific languages – domain-specific languages hosted directly in an existing high-level programming language. We provide examples of LwDSLs used in industry today, and then we describe the advantages of LwDSLs in V & V. We argue the approach promises substantial automation and cost-reduction in V & V.

This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)

Abstract

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

 In 2014, Google Glass was released to the public to great fanfare. Just the previous year, in his 2013 TED Talk, Google co-founder Sergey Brin spoke about the human usability issues that Google Glass was designed to solve, and they sounded plausible enough. Who wants to be hunched over their phone all the time? Wouldn’t […]

In May 2016, the newly created Decentralized Autonomous Organization (DAO), an investor-directed venture capital fund built as a smart contract on the Ethereum blockchain, raised around $150 million worth of digital currency. Hopes were high. The fund was to be a fully transparent and decentralized organization, with investment decisions made collectively through member votes, and […]