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

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

Abstract: Formally verifying security properties and the functional correctness of systems involves comprehensive analyses of system compatibility and interoperability. Many conventional approaches require trusted systems in order to assure properties of transmitted data that are difficult to authenticate, or the undesirable exposure of additional data for the purpose of verification. We overcome this limitation by […]

Abstract: The exponential rise in data has spurred significant interest in developing personalized machine models for a seemingly infinite range of applications. However, in the case of safety critical systems such as autonomous medical systems, classical algorithms have failed due to complications spanning from limited data to the requirement that systems be explainable and verifiably […]

The slides for this presentation can be found here. Abstract: Porting operating systems is expensive; it costs time and money and (particularly) the attention of senior developers. Furthermore, with the end of Moore’s Law, portability is becoming more important again. Against this background, recent advances in program synthesis and the increasing availability of formal specifications for machine architectures offer an […]

Abstract: Many software systems employ parsing techniques to map sequential input to structured output. Often, a parser is the system component that consumes data from an untrusted source. Because parsers mediate between the outside world and application internals, they are good targets for formal verification; parsers that come with strong correctness guarantees are likely to […]