Tech Talk: Orc in Haskell

The June 16th Galois Tech Talk will be delivered by Trevor Elliott, titled “Orc in Haskell.”

• Date: Tuesday, June 16th, 2009
• Time: 10:30am - 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: Concurrency is difficult to realize successfully. The Orc language tackles this problem by introducing explicit concurrency as part of its core. It presents a clean, and somewhat monadic, style of programming that should look familiar to Haskell users. I will give a quick introduction to the Orc language, using several examples to motivate its use. Following this introduction, a monadic Haskell embedding of the major features will be presented, bringing a type system to Orc.Bio: Trevor Elliott is a member of the technical staff at Galois, Inc.  His interests center around functional programming, and the effective use of type systems.Slides are available for download.Update: the source is now available on Hackage (though changed from the version presented at this talk).

---

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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Tech Talk: A Taste of DDT

The June 9th Galois Tech Talk will be delivered by Jim Grundy titled "A Taste of DDT."

• Date: Tuesday, June 9th, 2009
• Time: 10:30am - 12:00 noon
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: DDT is a partial implementation of the directed testing approach to test generation. The presentation will likely interest you if you are interested in how directed testing works, or what it is like to use in practice.This seminar presents a rational reconstruction of an experience of using DDT to test a rather rich FIFO/list module implemented in C. The module in question is about 1500 lines of code with a dozen or so entry points. The presentation walks through the user experience of writing and running a first naïve test harness for the module, finding and correcting issues in the code, up to a final declaration of victory.The presentation is rather long, about 1.5 hours, but takes the form of a gently paced walk through a user experience, and as such is rather less taxing on the concentration that you might expect for a talk of its duration.Bio: Jim Grundy is a research scientist with Intel Corporation.  His interests include functional programming, mechanized and interactive reasoning and their application to establishing the correctness of hardware and software systems.

---

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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

EDSLs for Unmanned Autonomous Verification and Validation

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.

Click to read more ...

Achronix and Signali: High-performance 128-bit AES cores for Speedster FGPAs

Achronix Semiconductor, maker of the world’s fastest FPGAs, today announced (.pdf) the availability of new, high-performance AES IP cores for its Speedster^TM 1.5 GHz family FPGAs.These high-performance 128-bit key size AES core are targeted at 10 Gbps, 40 Gbps, and 100 Gbps applications have been designed and built by Signali, a Galois spinoff focusing on custom cores targetting computationally intensive algorithms, fixed-function DSP and cryptographic applications. Signali uses their Quattro™ compiler suite to transform high-level descriptions of data-intensive functions, such as AES into high-performance RTL.Read the full story.

Click to read more ...

Engineering Large Projects in Haskell: A Decade of FP at Galois

Galois has been building systems in Haskell for the past decade. This talk describes some of what we’ve learned about in-the-large, commercial Haskell programming in that time. (Download slides :: .pdf).

• When and where we use Haskell
• Correctness, productivity, scalabilty, maintainability
• What language features we like: types, purity, types, abstractions, types, concurrency, types!
• The Haskell toolchain: FFI, HPC, Cabal, compiler, libraries, build systems, etc.
• Being a commercial entity in a largely open source community

This talk was presented Monday 20th April at λondon HUG.

Click to read more ...