Abstract:

Habit is a high-level programming language, originally based on Haskell, that was designed to meet the needs of high assurance, very low-level software development. The most recent version of the language report was completed in 2010, and an initial working prototype implementation was developed by the HASP group at PSU. However, there has not been a lot of externally visible news about the language or its implementation since then. In this talk, I will provide an introduction to the goals of Habit (no previous experience is assumed), and an update on the status of its current implementation as we continue to edge towards a broader public release. In particular, this talk will discuss the challenges of meeting the performance requirements for typical systems software; the benefits of programming in a source language with high-level functional abstractions and expressive types; and the role that whole-program optimization can play in bridging between these two worlds.

Bio:

Mark Jones is a professor in the Department of Computer Science at Portland State University in Portland, Oregon. His primary research focus is on the use of advanced programming language technologies that support the construction and certification of secure and reliable software systems.

Abstract: Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this work, we present RustBelt, the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem. In the talk, I will first review some of the essential features of Rust, and then explain some of the key ideas behind the RustBelt verification.

Bio: Derek Dreyer is a professor of computer science at the Max Planck Institute for Software Systems (MPI-SWS), and recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award. His research runs the gamut from the type theory of high-level functional languages, down to the verification of compilers and low-level concurrent programs under relaxed memory models. He is currently leading the RustBelt project, which focuses on building the first formal foundations for the Rust programming language. He also knows a thing or two about Scotch whisky.

Abstract: Recent progress in AI and machine learning is stimulating interest in applying AI in high stakes applications such as self-driving cars, surgical robots, and autonomous weapons systems. These applications require high levels of software assurance and resilience, but virtually all AI research has focused on raw performance without paying attention to questions of robustness and resilience.

In this talk, I will survey AI research that aims to create robust systems. I will consider both robustness to “known unknowns” and robustness to “unknown unknowns” — that is, to unmodeled aspects of the environment.

One technology that is relevant to creating robust AI systems is anomaly detection. In the second part of the talk, I will survey the work at Oregon State on anomaly detection. I’ll discuss our recent research on applying anomaly detection to problems of fraud detection and equipment diagnosis and discuss methods for explaining anomaly alarms to an analyst and incorporating analyst feedback into the anomaly detection process.

Bio: Dr. Tom Dietterich (AB Oberlin College 1977; MS University of Illinois 1979; PhD Stanford University 1984) is Professor Emeritus and Director of Intelligent Systems Research in the School of Electrical Engineering and Computer Science at Oregon State University, where he joined the faculty in 1985. Dietterich has devoted his career to machine learning and artificial intelligence. He has authored more than 180 publications and two books. His research is motivated by challenging real world problems ranging from personal information management, to drug design, to sustainability, and most recently to problems in safe and robust artificial intelligence. Dietterich has also devoted many years of service to the research community. He is Past President of the Association for the Advancement of Artificial Intelligence, and he previously served as President of AAAI (2014-16) and as the founding president of the International Machine Learning Society (2001-08). Other major roles include Executive Editor of the journal Machine Learning (1992-98), co-founder of the Journal for Machine Learning Research (2000), and program chair of AAAI 1990 and NIPS 2000. He is currently the moderator for machine learning on arXiv. Dietterich is a Fellow of the ACM, AAAS, and AAAI.

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 how it is possible to improve runtime efficiency and parallelism of Tower-generated C programs by releasing some constraints on the Hoare monitor model. Finally, some test results on SMACCMPilot, a high-assurance autopilot, will be presented.

bio:

Georges-Axel Jaloyan is a CS student at École Normale Supérieure in Paris. He is interning at Galois as part of his Master’s degree. He is interested in embedded systems security and safety-critical systems. He interned previously at NASA Langley Safety Critical Avionics Systems Branch.

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) -> M b) does not contain enough information to allow many proofs to go through. For lists, an implicit assumption on the function of type ( a -> M b) is that the input of type a is an element of the list of type M b. We developed an new typeclass of epsilon-monads to be able to strengthen the function type. Epsilon-monads are monads that support a membership predicate. Epsilon-monads enabled the development of a bind-induction proof rule which allows the extraction of monadic programs using the bind operator. Also, epsilon monads allow for extensional specifications of monadic programs. We used the Coq theorem prover to formalize the definitions and to prove many properties of the formalization. This is joint work with Hadi Shafe’i.

bio:

James Caldwell is Professor and Head of the Computer Science Department at the University of Wyoming. He earned his PhD from Cornell in the Nuprl group advised by Robert Constable. Before moving to the University of Wyoming in 1998, he was a researcher in the formal methods group at the NASA Langley Research center. He moved to NASA from the Electric Corporate R&D center in Schenectady, NY where he was first exposed to formal verification. He has MS and BS degrees in computer science from SUNY Albany. Before coming to computer science he studied painting and sculpture at the School of the Museum of Fine Arts, Boston.

(from the Meetup description):

Welcome to Portland Haskell Office Hours! Bring your projects, or just your excitement for learning.

We will still be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

--

About Haskell Office Hours:

Show up with a project you'd like to share or a problem that you're stuck on, and we'll learn together in small, supportive groups! An "Office Hours" meetup is an opportunity for people of all skill levels to come together, learn, and have fun. Our goal is to focus on inclusion and active participation through teaching and mentorship.

The meetup is hosted at Galois, which uses Haskell extensively in industry, and is well-attended by Galwegians who are eager to share their excitement for Haskell and functional programming. This group is very new, so you still have an opportunity to shape how we do things. If the schedule doesn't work for you, or if we can do anything to help you feel more safe and welcome, let us know!

abstract:

CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent.

There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and an axiomatic semantics (a separation logic for C). The most important properties — soundness and completeness results, subject reduction and progress, correctness of the type checker — have all been proved. All definitions and proofs have been fully formalized in Coq, without any axioms and on top of a non-trivial support library.

The CH2O project has two abstract C-like languages. A significant subset of C called “CH2O abstract C” is translated into a simplified language called “CH2O core C”. This translation is written in Coq and implicitly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C.

The executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standalone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does not yet support I/O (nor the exit function), a small hack allows the CH2O interpreter to still explore programs that call printf.

The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert and CH2O are that the CH2O semantics has explicit typing judgments for everything, and that CH2O applies to any ISO compliant compiler.

bio:

I have a master degree in mathematics (my thesis was about conformal supergravity), and a PhD in computer science, both from the University of Amsterdam. I also worked as a system administrator at the University of Utrecht.

Currently I’m an assistant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using interactive theorem provers, but recently I have been getting interested in practical program verification, where interactive proof is used when automation doesn’t cut it.

At the moment I am an alternate member of WG14, and I won a price in the IOCCC twice. And my favorite project is the CakeML/verified-HOL Light project.

abstract: In this talk, I’ll give an introduction to differential privacy with an emphasis on its relationship to machine learning, and its usefulness outside of privacy. Along the way, I’ll give a taste for the mathematical tools that can be used to achieve differential privacy. My thesis is that anyone who cares about data should care about the tools that the differential privacy literature offers.

bio: Katrina Ligett is an assistant professor of computer science and economics at Caltech. Before joining Caltech in 2011, she did postdoctoral work at Cornell, and she received her PhD in computer science from Carnegie Mellon in 2009. Her primary research interests are in mathematical foundations for data privacy, and in game theory. She has received an NSF Career Award, a Microsoft Research Faculty Fellowship, a Google Faculty Research Award, and an Okawa Foundation Research Grant.

abstract: We present four calculi for gradual typing: $\lambda\B$, based on the blame calculus of Wadler and Findler~(2009); $\lambda\C$, based on the coercion calculus of Henglein~(1994); and $\lambda\T$ and $\lambda\W$, based on the threesome calculi with and without blame of Siek and Wadler~(2010). We define translations from $\lambda\B$ to $\lambda\C$, from $\lambda\C$ to $\lambda\T$, and from $\lambda\T$ to $\lambda\W$. We show each of the translations is fully abstract —far stronger correctness results than have previously appeared.

bio: Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 60, with more than 18,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O’Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.

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

abstract: At this year’s WWDC, Apple announced Swift, a new programming language for iOS and OS X development. In this talk, I’d like to give a brief overview of the language, focussing on its ‘functional features’. I’ll try to demonstrate that there are exciting new possibilities for applying functional programming technology to a new platform — like writing an app that computes Fibonacci numbers without using a for-loop.

bio: Wouter Swierstra is a lecturer at the University of Utrecht. He has recently written a book, Functional Programming in Swift, together with Chris Eidhof and Florian Kugler.

abstract: Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit, called Termite-2. Termite-2 is the first tool to combine the power of automation with the flexibility of conventional development. It is also the first practical synthesis tool based on abstraction refinement. Finally, it is the first synthesis tool to support automated debugging of input specifications. I will explain the main principles behind the tool and give a brief demo of its capabilities.

bio: Leonid Ryzhyk is a postdoctoral fellow at the University of Toronto and a researcher at NICTA. He received his PhD from the University of New South Wales in 2010.

abstract: C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational semantics of C, the same operational semantics compiled by the proved-correct CompCert verified optimizing C compiler. Both of those proofs are machine-checked in Coq, an interactive proof assistant. This talk will present the basics of VST, followed by an example proof of a C program.

bio: Josiah (Joey) Dodds is an intern at Galois for the summer, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton, where he has been verifying information-flow properties and C programs in Coq.

Abstract: Records in Haskell are notoriously difficult to compose; many solutions have been proposed. Vinyl lies in the space of library-level approaches, and addresses polymorphism, extensibility, effects and strictness. I describe how Vinyl approaches record families over arbitrary key spaces using a Tarski universe construction, as well as a method for immersing each field of a record in a chosen effect modality. Moreover, I give a characterization of records as sheaves of types, which provides a clear motivation for the safety of subtyping and coercion of records, and a path toward records with non-trivial topologies on their key spaces. Lastly, I describe an interpretation of Vinyl-style records into Type Theory as finite products over containers, leading to many possible and interesting extensions, such as compositional universes of polymorphic variants, as well as inductive and coinductive types.

Bio: I'm an amateur type theorist who studied Historical Linguistics during my undergraduate at UC Berkeley, specializing in Ancient Greek, Sumerian, Akkadian and Anglo-Saxon. I'm particularly interested in type-theoretic syntax and semantics for natural language, and am presently exploring the use of multi-modal combinatory categorial grammar for interpreting the hyperbaton-rich syntax of ancient Indo-European languages. In addition to my interest in linguistics, I have become obsessed with extensionality, realizability and PER semantics for Martin-Löf Type Theory, and am currently trying to come up with an extension to Observational Type Theory which internalizes further extensional concepts, such as union, intersection, image and PER types whilst retaining decidability of type checking.

abstract: Sunroof is an embedded Haskell Domain Specific Language (DSL) that compiles to JavaScript. Blank Canvas is an embedded Haskell DSL that provides direct access to the HTML5 JavaScript Canvas. Both DSLs superficially provide the same capabilities, but make different trade-offs in the DSL design space. Sunroof uses monadic reification to enable bindings in the DSL to be translated into bindings in JavaScript, while blank canvas has every binding make a round trip from Haskell, to JavaScript, back to Haskell. In this talk, we will present the specifics of both DSLs, using examples, then use both DSLs to outline the difference choices available when designing and implementing embedded DSLs in Haskell.

bio: Andrew (Andy) Gill was born and educated in Scotland, and has spent his professional career in the United States, working both in industry, and academia. Andy received his Ph.D. from the University of Glasgow in 1996, then spent three years in industry as a compiler developer, and a year in academia as a principal project scientist. He co-founded Galois in 2000, a technology transfer company that used language technologies to create trustworthiness in critical systems. In 2008, he joined the University of Kansas, and in 2014 he was a recipient of the NSF CAREER Award.

Andy believes that functional languages like Haskell are a great medium for expressing algorithms and solving problems. Since returning to academia, he has targeted the application areas of telemetry and signal processing, specializing in generating high performance circuits from specifications. His research interests include optimization, language design, debugging, and dependability. The long-term goal of his research is to offer engineers and practitioners the opportunity to write clear and high-level executable specifications that can realistically be compiled into efficient implementations.

(from the Meetup page, please RSVP there!)

Our inaugural meeting will be a full-fledged office hours session! Bring your projects, or just your excitement for learning.

We will also be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

speaker: Joachim Breitner

abstract: We will take you on a guided tour through the memory of a running Haskell program and get to peek at the raw bytes of Haskell values. We’ll see how uniformity allows for polymorphic functions and data structures, where the garbage collector finds the information it needs and learn to predict how large certain values tend to become. With the help of a visualization tool (ghc-vis) we will also see laziness and sharing at work, and reveal the mystery of how Haskell fits infinite data structures into a finite amount of memory.

bio: Joachim Breitner is a PhD student at the Karlsruhe Institute of Technology, Germany, where he works on the semantics of lazy functional programming language and on interactive theorem provers. He maintains the Haskell packages for Debian and Ubuntu and contributes to GHC. When he is AFK, he enjoys board games, swing dancing, softball and paragliding.

Small presentation on the Meetup idea and values at 5:45pm by Tyler Zika.

Socializing, forming Master Mind groups, coding, and brainstorming from 6-7pm. Bring your laptop if you want to show what you are working on or you'd like some help.

Another small presentation. Topic and speaker TBA for remainder of Meetup.

RSVP on meetup.com site. Please and thank you.

Happy Coding!

Formal Verification of Cyber-Physical Systems

speaker: Pavithra Prabhakar

abstract: Cyber-Physical Systems (CPS) refer to systems in which control, computation and communication converge to achieve complex functionalities. The ubiquitous deployment of cyber-physical systems in safety critical applications including aeronautics, automotive, medical devices and industrial process control, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The talk will focus on an important feature of cyber-physical systems, namely, the mixed discrete-continuous behaviors manifesting as a result of the interaction of a network of embedded processors with the physical world. Hybrid Automata are a popular formalism for modeling systems exhibiting both discrete and continuous behaviors. We discuss formal approaches for the verification of hybrid automata. More precisely, scalable approaches based on approximations, including predicate abstraction, counter-example guided abstraction refinement and bounded error approximations, will be discussed in the context of safety and stability analysis. We will present applications of the techniques on hybrid automata models.

bio: Pavithra Prabhakar is on the faculty at the IMDEA Software Institute in Madrid, Spain, since 2011. Previously, she obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India. She spent the year between 2011-2012 at the California Institute of Technology as a CMI (Center for Mathematics of Information) fellow. Her main research interest is in Formal Analysis of Cyber-Physical Systems, more precisely, hybrid systems, with focus on both theoretical and practical aspects.

Correct-By-Construction Control Synthesis in Model-Based Design of Autonomous Systems

speaker: Ufuk Topcu

abstract: How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional "design+verify" approach to "specify+synthesize" in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that operate in adversarial environments. They combine ideas from control theory with those from computer science, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. The expressivity of the resulting design methodology enables us to formally investigate a number of emerging issues in autonomous, networked systems. I conclude my talk with a brief overview of several such issues from my ongoing projects: (i) compositional synthesis for the so-called fractionated systems; (ii) effects of perception imperfections on protocol synthesis; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctness; and (iv) human-embedded autonomy.

bio: Ufuk Topcu is a Research Assistant Professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California, Berkeley and was a Postdoctoral Scholar at the California Institute of Technology until 2012. His research is on the analysis, design, and verification of autonomous, networked systems.

RSVP on the meetup.com site. Please and thank you!

Be at the door by 5:30pm.

Message me on Skype: tylerzika if you are running behind so we can buzz you in.

Small presentation on the meetup idea and values at 5:45pm by Tyler Zika.

Socialize, forming Master Mind groups, coding, and brainstorming from 6-7pm.

Another small presentation. Topic and speaker TBA for remainder of meetup.

Happy Coding!

abstract: What if you want to store encrypted files on an untrusted Cloud Server in such a way that Server does not even know if you are editing the same file today as you were yesterday, or anything else about your usage patterns other than total amount of traffic to the Server? Clearly, no matter how strong of an encryption you use, access pattern is revealed: Cloud Server can simply track where on the hard drive you read/write from – clearly encryption does not hide that information. One naive solution to prevent revealing access pattern to the Server is to simply read all your data back from the Server and re-write your entire data back to Server in its entirety for each read/write. This works, but it is clearly impractical. Oblivious Random Access Memory (ORAM) is an algorithm that allows you to completely hide arbitrary access pattern in an efficient manner. In this talk, I will describe Oblivious RAM from the ground up, starting from my own Ph.D. thesis work on this topic (STOC 1990, MIT Ph.D. 1992) which showed the first efficient ORAM. The Journal Version of this work gained over 450 references according to Google Scholar [Ostrovsky-Goldreich JACM 1996] and ORAM became an important area of research in Cryptography in the last 5 years. I will describe surprising connections of ORAM to (1) tamper-proof embedded systems, (2) Software Protection (3) Secure Multi-Party and Secure Two Party Computation as well as (4) ways to securely compile programs with loops, “goto” statements, recursion, etc. into Garbled programs without “unrolling” the execution path, yet not revealing anything about the execution path. I will also compare and contrast ORAM to Single-Server Private Information Retrieval (Single-server PIR), which I co-invented with Kushilevitz in 1997, and explain important differences of these two models. The talk will be self-contained and accessible to the general audience.

Speaker bio: Rafail Ostrovsky is a Professor of Computer Science and Professor of Mathematics at UCLA and co-founder of Stealth Software Technologies, Inc. He has over 200 papers published in refereed journals and conferences and has 11 U.S. Patents issued. In 2013, Dr. Ostrovsky was inducted as an IACR (International Association of Cryptologic Research) Fellow. He currently serves as Vice-Chair of the IEEE Technical Committee on Mathematical Foundations of Computing and has served on 38 international conference Program Committees including serving as a PC chair of FOCS 2011. He is a member of the Editorial Board of JACM, the Editorial Board of Algorithmica; and the Editorial Board of Journal of Cryptology; he serves on the Editorial and Advisory Board of the International Journal of Information and Computer Security and is a member of the steering committee of the international symposium of Security in Communication Networks (SCN). He is a recipient of multiple academic awards and honors and has google h-index factor of 55. At UCLA, Prof. Ostrovsky heads security and cryptography multi-disciplinary Research Center (http://www.cs.ucla.edu/security/) at Henry Samueli School of Engineering and Applied Science.

Presented by Morgan Miller.

Cryptographic tools have become more powerful in the last three decades. With that power has come complexity. To use or even understand most security tools you need a thorough understanding of mathematics which makes them inaccessible to the general public. The discipline of usability has been growing as well in the past three decades. There have been few but promising overlaps in usability and security which may provide vital tools for managing our digital selves, upholding the principal of privacy, and preserving freedom of speech.

Presented by John Launchbury.

In secure computation, one or more parties collaborate to compute a result while keeping all the inputs private. That is, no-one can gain knowledge about the inputs from the other parties, except what can be determined from the output of the computation. Methods of secure computation include fully homomorphic encryption (where one party owns the input data and the other party performs the whole computation), and secure multiparty computation (where multiple parties collaborate in the computation itself). The underlying methods are still exceedingly costly in time, space, and communication requirements, but there are also many other practical problems to be solved before secure computation can be usable. For programmers, the algorithm construction is often nonintuitive; for compiler writers, the machine assumptions are very different from usual; and for application designers, the application information flow has to match the security architecture. In this talk we will highlight these challenges, and indicate promising research directions.

This event is free, but please RSVP on Eventbrite (will be linked above)

Event Description

Introducing TA3M Drink and Draw! We are planning a fun hands-on meetup. You will get to work with a team to discuss privacy, security, anti-surveillance, and anti-censorship topics and communicate your ideas through doodling! Each discussion group will work together to create a hand-drawn poster related to TA3M topics. This is a time to network with other individuals interested in these topics, and provides a fun way to express your ideas and concerns. We will do our very best to make sure beverages of all sorts (alcoholic and not) are available to get those creative juices flowing.

After the Drink and Draw session, we invite attendees to join us for social time at a nearby bar/restaurant.

Have a preference about what you want to learn? Want to lead a group in teaching a method? Email us a [email protected] and we'll add you to the agenda.

What is it?

This is the Techno-Activism 3rd Monday event for Portland, Oregon! Read more about techno-activism 3rd mondays.

Who should come?

Anyone interested in techno-activism. We invite coders, geeks, artists, and anyone else. No technical experience required.

Who's hosting?

The Privly Foundation organizes the event. Galois is generously providing space for the event.

Code of Conduct

Please review our code of conduct before attending the event to ensure a safe and welcoming time for all.

PDXTech4Good

If you're interested in this event, you might also be interested in the PDXTech4Good meetup.

presented by: Ashe Dryden

abstract: It's been scientifically proven that more diverse communities and workplaces create better products and the solutions to difficult problems are more complete and diverse themselves. Companies are struggling to find adequate talent. So why do we see so few women, people of color, and LGBTQ people at our events and on the about pages of our websites? Even more curiously, why do 60% of women leave the tech industry within 10 years? Why are fewer women choosing to pursue computer science and related degrees than ever before? Why have stories of active discouragement, dismissal, harassment, or worse become regular news?

In this talk we’ll examine the causes behind the lack of diversity in our communities, events, and workplaces. We’ll discuss what we can do as community members, event organizers, and co-workers to not only combat this problem, but to encourage positive change by contributing to an atmosphere of inclusivity.

bio: Ashe Dryden is an indie ruby developer living in Madison, WI. She's been involved with the web in some form or another over the course of the past 12 years. Ashe is an outspoken educator for diversity, inclusiveness, and empathy. She's currently writing a book on increasing diversity within companies, as well as working on a video series and site to serve as a resource to people who want to get involved. When she isn't discussing technology or it’s intersection with culture, she's cycling, tweeting, playing board games, debating the social implications of Star Trek episodes, being that awkward girl at the party, and waiting for her next burrito fix.

Small unmanned aircraft---more often called drones---are set to make a big impact on agriculture. You already know about military drones operating overseas, and perhaps you've even seen recreational drones starring in youtube videos, but as the FAA begins permitting commercial use of unmanned aircraft in 2015, you'll see drones replacing all sorts of roles that used to require a manned aircraft, and taking on new roles made possible by their low cost, versatility, and safety.

Chris Anderson will speak about the upcoming role of drones in agriculture, a field Chris says "is a big data problem without the big data." Chris will describe how farmers can will drones to curb plant disease, conserve water, and reduce pesticide and fertilizer use. He'll discuss the challenges ahead to integrate air vehicle systems with sensors, specialized cameras, and data processing.

Presented by Alex Groce.

One of the most effective ways to test complex language implementations, file systems, and other critical systems software is random test generation. This talk will cover a number of recent results that show how---despite the importance of hand-tooled random test generators for complex testing targets--- there are methods that can be easily applied in almost any setting to greatly improve the effectiveness of random testing. Surprisingly, giving up on potentially finding any bug with every test makes it possible to find more bugs over all. The practical problem of finding distinct bugs in a large set of randomly generated tests, where the frequency of some bugs may be orders of magnitude higher than other bugs, is also open to non ad-hoc methods.

Academic papers often describe typed calculi, but it is rare to find one in a production compiler. Indeed, I think the Glasgow Haskell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly statically-typed intermediate language, informally called "Core", or (when writing academic papers) the more respectable-sounding "System FC".

As real compilers go, GHC's Core language is tiny: it is a slight extension of System F, with letrec, data types, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core, namely typed (but erasable) coercions that witness type equalities, which turn Core into a particular kind of proof-carrying code. This single addition has opened the door to a range of source-language extensions, such as GADTs and type families.

In this talk I'll describe Core, and how it has affected GHC's development over the last two decades, concentrating particularly on recent developments, coercions, evidence, and type families. To test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a non-terminating rewrite system with non-left-linear rules.

Presented by Jesse Hallett.

Take control of your hardware by installing an open build of Android. Get root access and extend the life of your device. Learn about what is involved in installing a third-party OS on your phone or tablet.

Presented by Pat Hickey.

At Galois, we're building critical flight control software using new software methods for embedded systems programming. We will show how we used new domain-specific languages which permit low-level hardware manipulation while still providing guarantees of type and memory safety. The flagship application for these new languages is called SMACCMPilot, a clean slate design of quadcopter flight control software built on open-source hardware. This talk will introduce our new software methods and show how we built SMACCMPilot to be high assurance without sacrificing programmer productivity.

Presented by Neil Sculthorpe.

In Haskell, there are many data types that would form monads were it not for the presence of type-class constraints on the operations on that data type. This is a frustrating problem in practice, because there is a considerable amount of support and infrastructure for monads that these data types cannot use. This talk will demonstrate that a monadic computation can be restructured into a normal form such that the standard monad class can be used. The technique is not specific to monads --- it can also be applied to other structures, such as applicative functors. One significant use case for this technique is Domain Specific Languages, where it is often desirable to compile a deep embedding of a computation to some other language, which requires restricting the types that can appear in that computation.

Presented by Gerwin Klein and Thomas Sewell.

This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.

The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.

The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.

Five students in PSU’s Electrical and Computer Engineering Senior Capstone sequence want to show you what they’ve created: an inexpensive computer vision system for a quadcopter running on a Raspberry Pi board. One might be surprised how simple it is to code a decent object tracking algorithm using open-source software, and how difficult it is to keep a quadcopter from crashing into the wall in the debug stage. This talk should appeal to the RC hobbyist, the embedded systems programmer, and anyone interested in the art of computer vision. The presentation will include video footage of what these students have accomplished and how they pulled it off.

Presented by Joe FitzPatrick.

Generally, there is a very low barrier to entry when it comes to software or network-based attacks due to the fact that actual costs are minimal and most resources are readily available. This does mean that it's generally much easier to attack the software of a system than the hardware, but unfortunately that also leads to overconfidence in, as well as misplaced trust in hardware.

There is a clear 'hierarchy of attacks' in the hardware world. There are costs, often significant, involved in acquiring your hardware 'target' which might be damaged or destroyed in the process. There are a number of useful tools that cost anywhere from a few dollars to a few million dollars. I'll give a couple examples of what's possible within budgets of $100, $10,000, and $1,000,000. I'll point out how many capabilities are much more accessible than most assume, and how vulnerable to sub-$100 attacks most of our 'secure' hardware really is.

Presented by Andrew Farmer.

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks, leaving the programmer to do them by hand. This talk introduces HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT, demonstrate its use on examples, and seek input for further development and case studies.

Presented by Erlend Hamberg.

An important problem in genetics is phylogenetic inference: Coming up with good hypotheses for the evolutionary relationship between species – usually represented as a “family tree”. As the amount of molecular data (e.g. DNA sequences) quickly grows, efficient algorithms become increasingly important to analyze this data. A maximum-likelihood approach with models for nucleotide evolution allows us to use all the sequence data, but is a computationally expensive approach. The number of possible trees also grows rapidly as we include more species. It is therefore necessary to use heuristic search methods to find good hypotheses for the “true” tree. Evolutionary algorithms (EA) is a class of such search/optimization algorithms that has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecular data.

Presented by Brian Huffman.

A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadler-style "free theorems" about a polymorphic function from its type; e.g. rev :: [a] -> [a] must satisfy map f (rev xs) = rev (map f xs).

In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using types-as-binary-relations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types.

Presented by Daniel Matichuk.

Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.

Come join the Portland Drone Enthusiast community for our monthly meeting. If you like Drones, UAVs, or UAS then this is the group for you. We'll have some great guest speakers and the retreat to a local brewpub for continued discussion!

• Mike Hutt, UAS Program Manager, USGS National UAS Project Office Mike will join us remotely to talk about how the US Geological Society is using UAS to support their missions. The UAS office currently flies the Raven, Global Hawk and T-Hawk to operate their missions.

• Pat Hickey, Mavelous Developer Pat will speak about running ArduPilot and ArduCopter on the new PX4 hardware, and the advantages and challenges the new architecture brings with it.

Presented by Becky Straus.

Abstract: Efforts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) have attracted widespread attention and criticism, and rightly so. But Washington, D.C. is far from the only place that officials are making decisions that impact the privacy and free speech rights. State and local officials are jumping into the fray as well, passing laws or creating policies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up with emerging technologies. This presentation will survey several areas where state and local officials in Oregon have recently been active, including reviewing policies on automated license plate recognition, surveillance cameras, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.

Presented by Matthew Fernandez.

In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.

Presented by Brian Huffman.

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.

Presented by Larry Diehl.

Many advanced branches of mathematics involve structures that abstract over well known specific instances, e.g. abstract algebraic structures, equivalence relations, various orders, category theoretic structures, etc. In typed functional programming (e.g. with type classes in Haskell), encoding such structures amounts to enforcing the definition of elements and operations for a particular structure instance on one hand, and being able to use said elements and operations in generic definitions on the other hand. With Dependently Typed Programming (DTP) we can go one step further and define propositions/properties for abstract structures, and subsequently require proofs in particular instances.

This talk will tell the story of how examples of particular instances inspire an abstract definition (including its propositional properties), how to then instantiate the original concrete examples in the new abstract definition, and finally create further abstract definitions that depend on previously defined ones. Emphasis will be given on how easily concrete proofs can be used as evidence for abstract propositions, and how proofs about abstract structures parameterized by other abstract structures may reuse their proofs (similar to the more common concept of reusing operations in subsequent abstract definitions). The talk will use Agda as its demonstration language, but proofs will mostly be in the form of equational reasoning that should look familiar to the non-expert.

Presented by Iulian Neamtiu.

The relative novelty and rapid evolution pace of the Android ecosystem (platform, vendor-installed apps and third-party apps) means both the platform and apps receive little scrutiny. Hence there is a need for tools that assess, monitor and verify all components of the Android ecosystem. This lack of tools and scrutiny is particularly problematic when combined with the open nature of Google Play, the main app distribution channel.

In the first part of this talk we will focus on multi-layer profiling of Android apps using ProfileDroid, a tool and framework we developed at UC Riverside. ProfileDroid is useful for a variety of Android app analyses, from performance to usability to security. ProfileDroid monitors and correlates the behavior of an app at four layers: (a) static, or app specification (b) user interaction, (c) operating system, and (d) network layer. Using ProfileDroid on 27 free and paid Android apps, we have revealed: (a) discrepancies between the app specification and app execution, (b) free versions of apps could end up costing more than their paid counterparts, due to an order of magnitude increase in traffic, (c) most network traffic is not encrypted, (d) apps communicate with many more sources than users might expect.

In the second part of the talk we will present results from our long-term permission evolution study of the Android ecosystem---platform and 237 apps---over three years. We found that the platform has increased the number of dangerous permissions and does not move towards finer-grained permissions, and that app developers do not follow the principle of least privilege. We will also briefly discuss our efforts with static information flow tracking for Android apps, as well as building a log-and-replay system for Android.

Presented by Sergio Antoy from Portland State University.

In this talk, I will introduce narrowing, the characterizing feature of functional logic programming, from the programmer's viepoint. Narrowing promotes non-determinism and it enables computing with incomplete or unknown information. After a short and informal presentation of Curry, the leading functional logic language, I will discuss a few examples showing that narrowing and its associated non-determinism support programming at a very high level of abstraction.

Presented by Chris Andrew, Kayla Seliner, Mark Craig, and Trang Nguyen.

On October 7, 2008, the flight control system of Qantas flight 72 malfunctioned without warning. The failure caused the aircraft to violently pitch down with an acceleration of -0.8g, pitching passengers and crew into the roof of the cabin resulting in many injuries. In the investigation that followed, the malfunction was attributed to a software problem in the Air Data Inertial Reference Unit. These units are utilized on all modern passenger jets, but are proprietary devices not open to public scrutiny.

This capstone project develops an open source Air Data Inertial Reference Unit using four redundant Arduino boards each with a microcontroller, 3D gyroscope and accelerometer. Faults are injected into the system through software and outputs are monitored over serial ports allowing the user to test effectiveness of fault-tolerant algorithms to mask fail silent and byzantine faults in the sensors. Failures in ADIRU systems are usually complex in nature and arise under very anomalous circumstances suggesting that fault-tolerant system design could benefit from the diverse testing and evaluation that can occur in an open source community. This project demonstrates the low entry-cost to building a fault-tolerant system for open-source design and experimentation.

Presented by Charles Parker

A basic problem in computer science is binary classification, in which an algorithm applies a binary label to data based on the presence or absence of some phenomenon. Problems of this type abound in areas as diverse as computational biology, multimedia indexing, and anomaly detection. Evaluating the performance of a binary labeling algorithm is itself a complex task, often based on a domain-dependent notion of the relative cost of "false positives" versus "false negatives". As these costs are often not available to researchers or engineers, a number of methods are used to provide a cost-independent analysis of performance. In this talk, I will examine a number of these methods both theoretically and experimentally. The presented results suggest a set of best practices for evaluating binary classification algorithms, while questioning whether a cost-independent analysis is even possible.

Presented by Alan Mishchenko.

Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Presented by Julien Schmaltz.

Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.

Presented by Borzoo Bonakdarpour.

Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.

The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.

Presented by David Lazar

Formal semantics is notoriously hard. The K semantic framework (http://k-framework.org/) is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K. The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.

Presented by Nate Foster.

The languages used to program networks today lack modern features. Programming them is a complicated task, and outages and infiltrations are frequent. We believe it is time to develop NETWORK PROGRAMMING LANGUAGES with the following essential features:

• High-level abstractions that give programmers direct control over the network, allowing them to specify what they want the network to do without worrying about how to implement it.

• Compositional constructs that facilitate modular reasoning about programs.

• Portability, allowing programs written for one platform to be used with different devices.

• Rigorous semantic foundations that precisely document the meaning of the language and provide a basis for building formal verification tools.

The Frenetic language addresses these challenges in the context of OpenFlow networks. It combines a streaming declarative query sub-language and a functional reactive sub-language that, together, provide many of the features listed above. Our implementation handles many low-level packet-processing details and keeps traffic in the "fast path" whenever possible.

Presented by Eric Migicovsky.

Hardware is hard. At least that's what people always say. Building a hardware startup requires a broad base of technical knowledge, from electronics and manufacturing experience to aesthetic and interface design. But Eric Migicovsky chose to start a hardware company after graduating from engineering because he wanted to see something he designed become a physical reality.

inPulse is a $150 hackable Bluetooth smartwatch. It connects to your smartphone and displays notifications like incoming emails, calls, and calendar alerts right on your wrist. After launching an SDK, 3rd party developers have started to create apps for inPulse.

In his talk, Eric will share some honest stories and anecdotes from various stages of product development. He'll also talk about the costs, timeframes and failure modes of hardware startups.

Presented by Dylan McNamee.

This talk is an introduction to the MILS (Multiple Independent Layers of Security) architecture, motivated by the challenge of enforcing various kinds of security policies. I'll describe the goals of policy enforcement, traditional means of implementing security enforcement mechanisms, and the emerging MILS architecture for enforcing policies with high assurance.

Presented by Kevin Butler

The complexity of modern operating systems makes securing them a challenging problem. However, changes in the computing model, such as the rise of cloud computing and smarter peripherals, have presented opportunities to reconsider system architectures, as we move from traditional "stove-pipe" computing to distributed systems. In particular, we can build trustworthy components that act to provide security in complex systems.

This talk discusses how new disk architectures may be exploited to aid the protection of systems by acting as policy decision and enforcement points. We prototype disks that enforce data immutability at the block level on critical system data, preventing malicious code from inserting itself into system configuration and boot files. We then examine how storage may be used to ensure the integrity state of hosts prior to allowing access to data, and how such a design improves the security of portable storage devices. Using continual measurements of system state, we show through formal reasoning that such a device enforces guarantees that data is read and written while the host is in a good state. Finally, we discuss some recent initiatives to assure the identity of the host and identify future directions for exploring the interface between storage and operating system security.

Presented by Alexey Gotsman

Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK).

Presented by Sebastian Niller and Nis N. Wegmann

1

title: Translation of Functionally Embedded Domain-specific Languages With Static Type Preservation by using Witnesses

abstract: Static type preservation automatically guarantees type-correctness of an embedded domain-specific language (eDSL) by tying its type system to that of the host-language. Not only does this obviate the need for a custom type checker, it also preserves type-correctness during code transformations and optimizations, and simplifies and increases the efficiency of interpreters. When implementing a translator from a source DSL with type preservation to a target DSL, the commonly chosen approach requires the incorporation of extensions in the source DSL specific to the target DSL, which, in cases where multiple back-ends are required, obfuscates the source DSL and decreases the overall modularity. We show that by using witnesses, a technique which facilitates the construction of type-level proofs, we can effectively cope with this issue and implement translators without extending the source DSL.

We have applied our approach on Copilot, a Haskell-embedded domain specific language for runtime monitoring of hard real-time distributed systems, and used it for implementing two back-ends targeting the Haskell-embedded languages Atom and SBV. Our approach restrains to the Haskell 2010 Standard except for existentially and universally quantified types.

2

title: From High-Level Languages to Monitoring Fault-Tolerant Hardware: Case-Studies of Runtime Verification Using Copilot

abstract: Failures of hard real-time systems can be caused by systematic faults in software and hardware, as well as by random hardware faults, and faults due to wear out of hardware components. Even if monitoring software is proven to comply to its specification, there is no guarantee that failing underlying hardware does not affect the monitors themselves. An application of distributed Copilot monitors to a redundant airspeed measurement system is presented. We show the use of monitors enables the system to withstand benign and Byzantine hardware and software faults.

The second part of the talk presents current work using Copilot to monitor the MAVLink protocol in flight of a sub-scale model of an Edge 540T aircraft.

Presented by Kristin Rozier

Formal behavioral specifications written early in the system-design process and communicated across all design phases have been shown to increase the efficiency, consistency, and quality of the system under development. To prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. Our focus here is on specifications expressed in linear temporal logic (LTL).

We introduce a novel encoding of symbolic transition-based Buchi automata and a novel, ``sloppy,'' transition encoding, both of which result in improved scalability. We also define novel BDD variable orders based on tree decomposition of formula parse trees. We describe and extensively test a new multi-encoding approach utilizing these novel encoding techniques to create 30 encoding variations. We show that our novel encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking.

Details can be found here: http://ti.arc.nasa.gov/profile/kyrozier/.

Presented by Adam Foltzer.

Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.

This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.

This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.

Presented by Temesghen Kahsai.

We give an overview of a parallel k-induction-based model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. A first level of parallelism is introduced in the k-induction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the k-induction loop as soon as they are produced and used to strengthen the induction hypothesis.

This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property -- valid or invalid -- is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties.

We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties.

"Cfengine is an automation framework for system administration or IT Management. It began in 1993 and, after significant research and evaluation, it was completely rewritten in 2007. Today it is the most advanced automation framework, supporting all common platforms, and designed with security in mind, from the ground up."

Aleksey Tsalolikhin, aleksey at verticalsysadmin.com, made us an outstanding offer to introduce us to Cfengine version 3 the weekend following this year's USENIX conference.

Afterward, feel free to join us for lunch!

Presented by Nicholas Begley, Dave Dung Anh, James Heilinger, Alec Rasmussen, and Mark Theuson.

It's a bird! It's a plane! No, it's an open-source autonomous quad-copter. In collaboration with the Portland State University Electrical and Computer Engineering Dept., Galois mentored a Spring semester Senior Capstone Project to build an ArduCopter. The ArduCopter is based on the Arduino open-source hardware platform, and includes infrared sensors (collision avoidance), sonar and barometer (altitude hold), GPS (location), magnetometer (direction), and gyro (stabilization). This talk will include a description of the ArduCopter and it's operation, including the trials and tribulations of building and testing one. Of course, the talk will include cool videos.

Presented by Chad Scherrer.

Sampling from a large discrete distribution is a common problem in statistics. In this talk, we'll consider a real-world situation where the properties of the distribution cause common approaches to break down, and we'll arrive at a Haskell-based solution that fixes the problem.

Presented by Jim Snow.

RNA Networks is a software company focused on providing the next generation storage cache solution that addresses performance deficiencies and the rising cost of storage for virtual environments. Our software solution utilizes compute resources (DRAM and flash) as a distributed clustered cache moving 'active' data off of the storage tier and into the compute tier translating to significant performance gains with no additional investment in hardware resources. RNA's MVX technology is based on a distributed shared memory core that leverages RDMA fabrics and allows for a unified and flexible namespace that can scale proportionally to meet any performance or capacity need.

In this presentation we'll discuss the core architecture and how this can be leveraged to both reduce the cost of high end storage and meet high performance storage objectives.

Presented by Joe Hurd.

Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is cross-prover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.

Presented by Philip Weaver.

Janrain offers user management services that include single sign-on, social login, and profile storage. We have recently begun using Haskell extensively to implement our products, and would like to share what the experience has been like.

In this talk we will give a technical demonstration of Capture, whose backend is written in Haskell, discuss some of the implementation details of Capture, and look at some of the joys and pitfalls that we experienced.

Presented by Rachel Lanigan.

Engineers Without Borders USA is a fast-growing national non-profit impacting developing communities around the world. EWB provides an opportunity for engineering students and professionals to use their skills to develop sustainable, appropriate technologies for specific applications, to help meet the basic needs of people. Our programs typically start with a focus on providing water and sanitation, but often move into other areas depending on the needs of the people. There is a role for everyone at EWB, from engineers to public health professionals. Rachel will give a background on EWB, our local chapter, and how to get involved.

Presented by Johan Tibell.

The most commonly used map (dictionary) data type in Haskell is implemented using a size balanced tree. While size balanced trees provide good asymptotic performance, their real world performance is not stellar, especially when used with keys which are expensive to compare, such as strings.

In this talk we will look at two different map implementations that use hashing to achieve better real world performance. The implementations have different performance characteristics: one provides very fast look-ups while the other trades better insert performance for somewhat slower look-ups. I will describe the design of these data structures and show some early benchmark results.

Presented by Grant Passmore.

In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: user-specifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different.

In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worst-case doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one?

The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification tool-chains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions).

Presented by Simon Winwood.

In 2009 the NICTA L4.verified project completed the machine-checked correctness proof of the seL4 microkernel. The natural next step is then to use this verified kernel to construct verified systems.

In this talk I give an overview of the ongoing work into systems verification in the Trustworthy Embedded Systems project. In particular, I will focus on the use of access control results to reason about the properties of systems in the presence of large untrusted components, such as a Linux kernel.

Presented by Aaron Tomb.

Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior --- often a collection of independent assertions sprinkled throughout the program.

Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus.

We have applied our analysis to a large body of widely-used open-source software, and found a number of bugs.

Presented by Rebekah Leslie.

The existing implementation of DDT uses a depth-first search algorithm to drive the exploration of new paths for testing. This algorithm provides full coverage of the program under test, but is limited by the fact that the number of paths increases exponentially with the size of the program. By employing the control-flow graph information of the program under test, we can direct the testing process towards program paths that contain unvisited points and therefore obtain full branch coverage in a smaller number of tests than would be required by the original depth-first search algorithm. We will present two uses of control-flow graph information in DDT. The first use is a refinement of depth-first search where control-flow graph information is used to prune the search space to eliminate unnecessary tests. The second use is in the context of a prioritized work-queue that forms the basis for a variety of sophisticated search algorithms that exploit different heuristics.

Presented by Brian Ford

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.

speaker: Alwyn Goodloe

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.

Presented by Lee Pike.

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.

presenter: David Spivak

About five months ago I gave a talk here at Galois called “Databases are categories.” The basic idea was that a database schema can be represented as a category C and its states can be represented as functors C–>Set. In this talk I’ll refine that notion a bit, explaining that schemas are better represented as sketches. I’ll also show how, within this model one can: deal with incomplete data; incorporate typing and calculated fields; and perform queries, define views, and migrate data between disparate schemas. That is, I’ll try to show that the categorical approach handles everything one might hope it would. Finally, I’ll discuss a linguistic version of categories, called “ologs,” and show how they may help to democratize information storage.

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

title:

Fides: Remote Anomaly-Based Cheat Detection Using Client Emulation

speaker:

Prof. Wu-chang Feng

time:

10:30am, Tuesday 19 October 2010

location:

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

abstract: As a result of physically owning the client machine, cheaters in online games currently have the upper-hand when it comes to avoiding detection. To address this problem and turn the table on cheaters, this paper presents Fides, an anomaly-based cheat detection approach that remotely validates game execution. With Fides, a server-side Controller specifies how and when a client-side Auditor measures the game. To accurately validate measurements, the Controller partially emulates the client and collaborates with the server. This paper examines a range of cheat methods and initial measurements that counter them, showing that a Fides prototype is able to efficiently detect several existing cheats, including one state-of-the-art cheat that is advertised as undetectable.

bio: Wu-chang Feng is currently an Associate Professor in the Intel Systems and Networking Laboratory at Portland State University where he leads a research group in networking and security. Wu-chang received his B.S. in 1992 from Penn State University and his M.S.E. and Ph.D. degrees in 1994 and 1999 from the University of Michigan. He was awarded the IEEE Communications Society 2003 William R. Bennett prize as well as one of four prizes recognizing the Best IBM Research Papers in Computer Science, Electrical Engineering and Math published in 2002.

Presented by Priyank Kalla.

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.

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

Please note the nonstandard day/time!

title:

Introduction to Logic Synthesis

speaker:

Alan Mishchenko, University of California, Berkeley 

time:

10:30am, Friday 08 October 2010

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

abstract:

The lecture describes the problems solved by logic synthesis. It presents functional representations and typical computations applied to Boolean networks, such as traversal, windowing, cut computation, simulation, Boolean reasoning. Presented next are And-Inverter Graphs (AIGs) that are increasingly used as a unifying representation for all problems. The lecture is finished by an overview of AIG-based solutions in synthesis, technology mapping, and formal verification. 

bio:

Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998.  Currently, Alan is an Associate Researcher at University of California, Berkeley.  His research interests are in developing computationally efficient methods for logic synthesis and verification. 

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

title:

Enabling Portable Build Systems

speaker:

Rogan Creswick, Galois, Inc.

time:

10:30am, Tuesday 05 October 2010

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

abstract:

Modern computing–and high-performance computing in particular–utilizes a variety of hardware and software platforms. These differences make it difficult to develop build systems that are robust to platform changes. Our goal is to investigate the design of portable build systems that are simple yet sufficiently robust with respect to environmental changes so that software can be easily distributed and built on, and for, myriad systems. We will discuss the current state of build tools and present options for iteratively improving the reliability and utility of existing build tools while laying the groundwork for more sophisticated and flexible build systems in the future. 

bio:

Rogan Creswick joined Galois in January of 2010, bringing expertise in programming by demonstration and natural language processing. He also harbors a love for tool development that is backed by years of academic research in usability and software engineering at Oregon State University. His work in those areas improved techniques for fault location, detection, and assertion propagation in end-user programming languages. 

abcBridge: Functional interfaces for AIGs and SAT solving

Edward Z. Yang

SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.

This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.

Computers As We Don’t Know Them Christof Teuscher, PhD

Since the beginning of modern computer science some sixty years ago, we are building computers in pretty much the same way. Silicon transistor electronics serves as a physical device, the von Neumann architecture provides a computer design model, while the abstract Turing machine concept supports the theoretical foundations. However, in recent years, unimagined computing devices have seen the light because of advances in synthetic biology, nanotechnology, material science, and neuroscience. Many of these novel devices share the following characteristics: (1) they are made up from massive numbers of simple, stochastic components which (2) are embedded in 2D or 3D space in some disordered way. A grand challenge in consists in developing computing paradigms, design methodologies, formal frameworks, architectures, and tools that allow to reliably compute and efficiently solve problems with such devices. In this talk, I will outline my visionary and long-term research efforts to address the grand challenge of building, organizing, and programming future computing machines. First, I will review exemplary future and emerging computing devices and highlight the particular challenges that arise for performing computations them. I will then delineate potential solutions on how these challenges might be addressed. Self-assembled nano-scale cellular automata (CAs) and random boolean networks (RBNs) will serve as a simple showcase. I will also present the efforts underway to self-assemble massive-scale nanowire-based interconnect fabrics for spatial computers and what the challenges are in terms of computations and communication in such a non-classical system.

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

title:

Industrial Strength Distributed Explicit Model Checking

presenter:

John Erickson

time:

10:30am,  August 3rd, 2010

location:

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

Abstract:

We present PReach, an industrial strength distributed explicit state model checker based on Murphi. The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murphi specification language. PReach is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murphi front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. This talk describes the PReach implementation including the various features that are necessary for the large models we target. We have used PReach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. PReach has been released to the public under an open source BSD license.

bio:

John Erickson is a Design Engineer at Intel Hillsboro.  He graduated with his PhD in Computer Science from The University of Texas at Austin in 2008.  Currently he is working on the validation of uncore components in a 50+ core processor using a variety of formal and dynamic techniques. Past research interests include theorem proving with a focus on lemma generation and generalization in the context of induction. 

Requirements and Performance of Data Intensive, Irregular Applications

Dr. John Feo

Many fundamental science, national security, and business applications need to process large volumes of irregular, unstructured data. Data collection and analysis is rapidly changing the way the scientific, national security, and economic communities operate. There are worldwide operational deployments of instruments to detect the proliferation of weapons of mass destruction, monitor terrorist cells, and track the movement of illicit goods and services. In the next 15 years 30% of battle-space defense forces will be autonomous with each advanced robotic device carrying dozens of sophisticated sensors collecting, processing, analyzing and transmitting large amounts of data. American economic competitiveness will depend increasingly on the timely analysis of many Petabytes of data collected in diverse computing clouds charting the social and economic behavior of consumers.

Unlike traditional scientific applications based on linear algebra routines, data analytic applications comprise large, integer-based graph computations with irregular data access patterns, low computation to memory access ratios, and high levels of fine grain parallelism that pass data and synchronize frequently. Traditional architectures optimized to run large-scale floating point intensive simulations are inadequate, and more suitable high-end architectures such as the Cray XMT are needed. In this talk I will discuss the programming language, tools, and system requirements for data analytic applications. I will survey the research at PNNL’s Center for Adaptive Supercomputer Software as regards graph analytics. In particular, I will present several key graph algorithms we have developed with an emphasis on structure, use of special hardware features, performance, and scalability.

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

title:

Towards a High-Assurance Runtime System: Certified Garbage Collection 

presenter:

Andrew Tolmach 

time:

10:30am, Tuesday, 29 June 2010.

location:

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

abstract:

It seems obvious that the reliability of critical software can be improved by using high-level, memory-safe languages (Haskell, ML, Java, C#, etc.). But most existing implementations of these languages rely on large, complex run-time systems coded in C. Using such an RTS leads to a large "credibility gap" at the heart of the assurance argument for the overall system. To fill this gap, we are working to build a new high-assurance run-time system (HARTS), using an approach grounded in machine-assisted verification, with an initial focus on providing certifiably correct garbage collection.This talk will describe a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add a new intermediate language, GCminor, that supports GC'ed languages and has a proven semantics-preserving translation to assembly code. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the GHC's Core intermediate language to GCminor. (This is joint work with Andrew McCreight and Tim Chevalier.)

bio:

Andrew Tolmach has been a faculty member at Portland State University since receiving his Ph.D.in Computer Science from Princeton in 1992. His current research interests, pursued under the aegis of the PSU High Assurance Systems Programming (HASP) project, focus on high-assurance systems software development, in particular using formal verification. His past publications, mostly about functional languages, include work on operating systems in Haskell, garbage collection, compilation, debugger implementation, integration with logic languages, and lazy functional algorithms. 

Introducing Well-Founded Recursion Eric Mertens

Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.

presenter: Taras Glek

abstract: A competitive browser market requires fast-paced improvements to the codebase. Such improvements may require significant refactoring of large parts of the codebase. Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce developer productivity. Mozilla developed C++ static analysis and refactoring tools to increase developer leverage in C++. Static analysis is done via Dehydra/Treehydra GCC plugins and refactoring is accomplished by extending the Elsa C++ parser. This talk will discuss why Mozilla needs static analysis, why there are so few tools for C++, and specific projects that we’ve embarked on.

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

IMPORTANT: Please note that this talk is Thursday.

title:

Categories are Databases 

presenter:

Dr. David Spivak 

time:

10:30 am, 03 June 2010, Thursday 

location

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

abstract:

Category theory is a powerful language for organizing layers of abstraction in all areas of mathematics. Databases are powerful tools for organizing information of all sorts. Whereas categories are often considered hopelessly abstract, databases are often considered horrifically mundane. Thus it is either strange or fitting that, mathematically speaking, categories and databases are the same concept. In this talk I’ll show how to turn any database into a category and any category into a database. I’ll also discuss functors and how they may be useful for issues of data migration and merging.

bio:

David Spivak graduated with a PhD in mathematics from UC Berkeley in 2007; his thesis used higher category theory to fix an old problem in geometry. From 2007 to the present, he have been a postdoc at the University of Oregon in the Math Department. During this time, his focus has moved toward the idea of using category theory to understand information and communication.  This summer, he will become a mathematics postdoc at MIT for three years, focusing on information and communication from a category-theoretic perspective. 

The L4.verified Project Presented by Dr. Gerwin Klein.

Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.

presenter: Mark Jones

abstract: Developers of systems software must often deal with low-level and performance-critical details that are hard to address in high-level programming languages. As a result, much of the systems software that is produced today is written in languages like C and assembly code, without the benefit of more expressive type systems or other features from modern functional programming languages that could help to increase programmer productivity or software quality. In this talk, we present an update on the status of Habit, a dialect of Haskell that we are designing, as part of the HASP project at PSU, to meet the needs of high assurance systems programming. Among other features, Habit provides: mechanisms for fine control over representation of bit-level and memory-based data structures; strong support for both functional and imperative programming; and a flexible type system that allows precise characterization of size and bound information via type level naturals, as well as termination properties resulting from the use of unpointed types.

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

The talk will be held at

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

Details:

* Presenter: Kathleen Fisher, AT&T Labs
* Date: Monday May 03, 2010
* Time: 3:30pm

Title: Typing Directories

Abstract: PADS describes the contents of individual ad hoc data files, but has no provisions for describing collections of files, i.e., directories. In this talk, I explore examples where having a declarative description of directories as well as files would be useful, including websites, source code trees, source code control systems, operating systems, and scientific data sets. As part of this exploration, I identify essential features of a directory description language and useful tools that might be produced from such a description. I end with a series of questions about how such a language might most easily be implemented in the context of Haskell.

This is joint work with David Walker and Kenny Zhu.

Bio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher is a Principal Member of the Technical Staff at AT&T Labs Research and a Consulting Faculty Member in the Computer Science Department at Stanford University. Kathleen’s research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data, including the Hancock system for efficiently building signatures from massive transaction streams and the PADS system for managing ad hoc data.

Kathleen is an ACM Distinguished Scientist. She has served as program chair for FOOL, CUFP, and ICFP. She is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), Co-Chair of CRA’s Committee on the Status of Women (CRA-W), and an editor of the Journal of Functional Programming. She is currently serving on the CRA Board.

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

The talk will be held at

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

Visualizing Information Flow through C Programs

Details:

* Presenter: Joe Hurd
* Date: Tuesday April 27, 2010
* Time: 10:30am

Abstract: The aim of the Automated Security Analysis project is to determine whether the information flows in a realistically-sized C codebase can be automatically deduced and communicated in an understandable way to someone unfamiliar with the code. To test this, a new information flow static analysis and visualization technique were developed, and implemented in a research prototype tool. This talk will present the novel features of the static analysis and demonstrate how the results are shown in the visualization tool: information flow between program storage locations is decomposed into two compositional properties, which can be computed using sound abstract interpretation techniques. For each deduced information flow, the static analysis keeps track of a set of source code locations which demonstrate the information flow, and this is used by the visualization component to communicate the information flow to a user browsing the source code.

Bio: Joe Hurd, Ph.D. is a Formal Methods Engineer at Galois, Inc. For the past ten years Dr. Hurd has been applying theorem proving techniques to formally verify the correctness of complex software, including probabilistic programs, elliptic curve cryptography and game tree analysis algorithms. He is also the developer of Metis, an automatic theorem prover for first order logic, and coordinates the OpenTheory project, a package management system for higher order logic theories. Dr. Hurd is an active member of the theorem proving research community, having organized conferences in 2005 and 2008, given invited talks, and regularly appears on program committees and reviews papers for conferences and journals. Prior to joining Galois in 2007, Dr. Hurd was a research fellow at Magdalen College, University of Oxford. He studied at the University of Cambridge, receiving a Masters level degree in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.

** NOTICE: This talk has been postponed until April 1 at 10:30am.

Building Refactoring Tools for Functional Languages

Details:

* Presenter: Prof. Simon Thompson
* Date: Thursday, April 1, 2010
* Time: 10:30am

Abstract: Refactoring is the process of changing the design of a program without changing what it does. Typical refactorings, such as function extraction and generalisation, are intended to make a program more amenable to extension, more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code (rather than within the bowels of a compiler), and in having an effect across a code base. Because of this, there is a need to give (semi-)automated support to the process. This talk will reflect on our experience of building tools to refactor functional programs written in Haskell (HaRe?) and Erlang (Wrangler). In doing this we will address system design, the pragmatics of system take-up, as well as contrasting the style of refactoring and tooling for Haskell and Erlang.

Bio: Simon Thompson is a Professor of Logic and Computation at the University of Kent.

Galois is pleased to host two tech talks on Wed., March 24.

Visualization and Diversity Information

Details:

* Presenter: Prof. Ron Metoyer
* Date: Wednesday, March 24, 2010
* Time: 10:30am

Abstract: The term “diversity’’ is used in many ways in many domains. People are concerned about the diversity of their work force, stock portfolios, student body, and forest insects, just to name a few. In this talk, I will discuss a work-in-progress visualization technique specifically designed to communicate diversity information. I will present the design concerns, resulting visualizations, and a study design for evaluating the method. I will conclude with a discussion of a case-study application to moth species data.

Bio: Ronald Metoyer is an Associate Professor in the School of Electrical Engineering and Computer Science at Oregon State University. He earned a Ph.D. from the Georgia Institute of Technology where he worked in the Graphics, Visualization and Usability Center with a focus on modeling and visualizing the motion of pedestrians in urban and architectural scenes. Dr. Metoyer currently co-directs the NVIDIA Graphics and Imaging Technologies Lab (GAIT) with his colleagues at OSU. His past research efforts have involved the investigation of techniques for manipulating motion capture data and for facilitating the creation of 3D content by end users with the goal of empowering domain experts to create compelling and interactive content for their domain specific needs. In 2002, he received an NSF CAREER Award for his work in “Understanding the Complexities of Animated Content”. Dr. Metoyer’s most recent research interests fall under the domain of information visualization.

TITLE: Scientific Data Visualization in a GPU World

Details:

* Presenter: Prof. Mike Bailey
* Date: Wednesday, March 24, 2010
* Time: 11:00am

Abstract: One of the fun aspects of scientific data visualization is that there are no rules — anything that adds insight to the data display is fair game. Add that to the fun of custom-programming the GPU, and you’ve really got something!

This talk will discuss some of the uses of custom GPU programming to create better and more interactive visualization displays. We will look at techniques in the realm of scalar visualization, vector visualization, volume visualization, and terrain mapping.

Bio: Mike Bailey is a Professor in Computer Science at Oregon State University. He specializes in scientific visualization, 3D interactive computer graphics, GPU programming, stereographics, and computer aided geometric design.

Haskell is an excellent language for combining the power of functional programming with imperative constructs. This characteristic led to the development of the Communicating Haskell Processes (CHP) libraries, which support imperative synchronous message-passing in Haskell. The core 'chp' library provides basic message-passing, concurrency and choice, as well as integrated support for tracing. The 'chp-plus' library provides higher-level features such as process composition operators and behaviour combinators. This talk provides an introduction to the two libraries and the programming style they engender -- as well as a brief look at the formal semantics underlying the libraries.

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.

The talk will be presented by Iavor Diatchki on Tuesday, February
16th, at 10:30am.

Abstract: GF is a programming language for multilingual grammar
applications. It may be seen in a number of different ways:

• as a special-purpose language for grammars, like YACC or Happy,  

but not restricted to programming languages;

• as a functional language, like Haskell or SML, but specialized to  

grammar writing;

• as a logical framework, like Agda or Coq, but equipped with  

concrete syntax in addition to logic;

• as a natural language processing framework, like LKB, or Regulus,  

but based on functional programming and type theory. This talk is an introduction to GF’s basic concepts by example. We
will look at how to define the meaning and syntax of a language,
perform simple translations, define semantic properties, and how to
use GF together with another language such as Haskell.

Bio: Iavor Diatchki is a R&D Engineer at Galois, Inc. with a Ph.D.
from the Oregon Graduate Institute.

Details:

• Date: February 16th, 2010, Tuesday
• Time: 10:30am
• Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of  

the Commonwealth building)

Hello,

The next Galois Tech Talk will be "An Introduction to the Maude Formal Tool Environment", presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am.

For more details, please visit: http://www.galois.com/blog/2010/01/29/tech-talk-an-introduction-to-the-maude-formal-tool-environment/

Hope to see you there! -Iavor

A Scalable I/O Manager for GHC

Presented by Johan Tibell.

Abstract: The Glasgow Haskell Compiler supports extraordinarily cheap threads. These are implemented using a two-level model, with threads scheduled across a set of OS-level threads. Since the lightweight threads can’t afford to block when performing I/O operations, when a Haskell program starts, it runs an I/O manager thread whose job is to notify other threads when they can safely perform I/O.

The I/O manager manages its file descriptors using the select system call. While select performs well for a small number of file descriptors, it doesn’t scale to a large number of concurrent clients, making GHC less attractive for use in large-scale server development.

This talk will describe a new, more scalable I/O manager that’s currently under development and that hopefully will replace the current I/O manager in a future release of GHC.

Details: Date: January 29th, 2010, Friday Time: 1:30pm Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

Bio: Johan Tibell is a Software Engineer at Google Inc. He received a M.S. in Software Engineering from the Chalmers University of Technology, Sweden, in 2007.

The next Galois Tech Talk will be delivered by Amit Goel. Come kick off 2010 with us!

Title: Ground Interpolation for Combined Theories

Abstract: We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.

* Date: Tuesday, 10:30am, 05 Jan 2010
* Time: 10:30am – 11:30am
* Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Bio: Amit Goel is a member of Intel’s Strategic CAD Labs.

The December 15th Galois Tech Talk will be delivered by John Launchbury. He will present Conal Elliott’s 2009 ICFP paper entitled Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.

Who : Anybody who wants to hack on Darcs (or Camp, Focal, SO6, etc) Beginners especially welcome!

Why : Darcs aims to have bi-annual hacking sprints so that we can get together on a regular basis, hold design discussions, hack up a storm and have a lot fun.

What : We plan to put some finishing touches on Darcs-2.4. Darcs 2.4 is a pretty exciting release because we expect it to offer nice performance enhancements from Petr's Google

Summer of Code Project, and also a nice new 'hunk splitting' feature.

We also intend to set aside at least one Darcs hacker for mentoring beginners, so if you're new to Haskell or to Darcs hacking, here's a good chance to plunge in and start working on a real world project.

How: Add yourself to http://wiki.darcs.net/Sprints/2009-11

[NB. This talk is on Friday, instead of the usual Tuesday slot.]

The next talk in the Galois Tech Seminar series:

• Date: Friday, November 13th, 2009
• Title: Hoare-Logic – fiddly details and small print
• Speaker: Rod Chapman
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/11/04/chapman-hoare/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, November 3rd, 2009
• Title: Testing First-Order-Logic Axioms in AutoCert
• Speaker: Ki Yung Ahn
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/28/ahn-autocert/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 27th, 2009
• Title: How to choose between a screwdriver and a drill
• Speaker: Tanya L. Crenshaw
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/20/crenshaw-simplex/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 20th, 2009
• Title: Writing Linux Kernel Modules with Haskell
• Speaker: Thomas DuBuisson
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/13/haskellkernelmodules/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 13th, 2009
• Title: Constructing A Universal Domain for Reasoning About Haskell Datatypes
• Speaker: Brian Huffman
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/06/huffman-universal/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 6th, 2009
• Title: Roll Your Own Test Bed for Embedded Real-Time Protocols: A Haskell Experience
• Speaker: Lee Pike
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/09/29/pike-haskell0/

Abstract: We present by example a new application domain for functional languages: emulators for embedded real-time protocols. As a case-study, we implement a simple emulator for the Biphase Mark Protocol, a physical-layer network protocol in Haskell. The surprising result is that a pure functional language with no built-in notion of time is extremely well-suited for constructing such emulators. Furthermore, we use Haskell’s property-checker QuickCheck to automatically generate real-time parameters for simulation. We also describe a novel use of QuickCheck as a probability calculator for reliability analysis.

Bio: Lee Pike is a member of the technical staff at Galois. Previously, he was a research scientist with the NASA Langley Formal Methods Group, primarily involved in the SPIDER project. His research interests include applying formal methods to safety-critical and security-critical applications, with a focus on industrial-scale endeavors.

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

[Note the Friday date, instead of the usual Tuesday slot!]

• Date: Friday, September 18th, 2009
• Title: Building Systems That Enforce Measurable Security Goals
• Speaker: Trent Jaeger
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/09/10/jaegermeasurablesecurit/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, August 25th, 2009
• Title: Programming the Fleet
• Speaker: Adam Megacz
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/08/19/programmingfleet/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The July 28th Galois Tech Talk will be delivered by Joe Hurd, titled “Mathematics of Cryptography: A Guided Tour.”

* Date: Tuesday, July 28th, 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: In this informal talk I’ll give a guided tour of the mathematics underlying cryptography. No prior knowledge will be assumed: the goal of the talk is to demonstrate how simple mathematical concepts from algebra and number theory are used to build a wide range of cryptographic algorithms, from the familiar (encryption) to the exotic (zero knowledge proofs).

Bio: Joe Hurd is a Formal Methods Engineer at Galois, Inc. He completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs, and his work since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world’s first formally verified chess endgame database.

Abstract: This talk describes a radically different architecture for computing called Fleet. Fleet accepts the limitations to computing imposed by physics: moving data around inside a computer costs more energy, more delay, and more chip area than the arithmetic and logical operations ordinarily called “computing.” Fleet puts the programmer firmly in charge of the most costly resource, communication, instead of in charge of the arithmetic and logical resources that are now almost free. Fleet treats arithmetic and logical operations as side effects of where the programmer sends data.

Fleet achieves high performance through fine grain concurrency. Everything Fleet does is concurrent at the lowest level; programmers who wish sequentiality must program it explicitly. Fleet presents a stark contrast to today’s multi-core machines in which programmers seek concurrency in an inherently sequential environment.

The Fleet architecture uses a uniform switch fabric to simplify chip design. A few thousand identical copies of a programmable interface connect a thousand or so repetitions of basic arithmetic, logical, input-output, and storage units to the switch fabric. The uniform switch fabric and its identical programmable interfaces replace many of the hard parts of designing the computing elements themselves.

Both software and FPGA simulators of a Fleet system are available at UC Berkeley. Berkeley students have written a variety of Fleet programs; their work helped to define what the programmable interface between computing and communication must do. A simple compiler now produces the programs required at source and destination to provide flow-controlled communication. We expect work on a higher-level language to appear soon as a PhD dissertation.

A recent 90 nanometer TSMC test chip, called Infinity, demonstrated switch fabric performance at about 4 GHz. A new test chip, called Marina, has just gone out for fabrication. Marina will test the programmable interface, and if successful, will give us confidence to build a complete Fleet. We seek participation from sponsors, programmers, and designers of basic computation elements.

Bio: Ivan Sutherland is a Visiting Scientist at Portland State University where he and Marly Roncken have recently established the “Asynchronous Research Center” (ARC). The ARC occupies both physical and intellectual space half way between the Computer Science (CS) and Electrical and Computer Engineering (ECE) departments at the university. The ARC seeks to free designers from the tyranny of the clock by developing better tools and teaching methods for design of self-timed systems. Prior to moving to Portland, Ivan spent 25 years as a Fellow and Vice President at Sun Microsystems. A graduate of Carnegie Tech, Ivan got his PhD at MIT in 1963 and has taught at Harvard, University of Utah, and Caltech.

Dr. Sutherland received the 1998 Turing Award, for his pioneering work in the field of computer graphics.

The next Galois Tech Talk, #2 for 2009, will be Isaac Potoczny-Jones (aka SyntaxNinja) on developing for the Android G1 phone.

The Android G1 is a TMobile phone whose operating system, Android is based on Linux and was developed by Google. It’s a very open smart-phone platform that rivals the iPhone.

While I’m no expert in Android or mobile platform development, I will discuss my experiences in Android development and demonstrate the toolchain used to develop software for the Android. I’ll outline the basic features of the platform, with a focus on the factors that make its openness so powerful:

* the inter-process communications mechanism whereby applications can advertise the services they offer and other applications can take advantage of those services,

* The open-source Java, Eclipse, and Linux-based toolchain,

* the OpenIntents project.

This will be an informal demonstration and discussion.

A group of us in collaboration between the Android Password Safe project and the Openintents project have implemented a cryptography service and a keystore service which other Android applications can use to keep data and passwords safe, in a way that’s convenient for the end user.

Our system allows a single password, and periodic single sign-on so that all applications can encrypt, decrypt, and store keys using the same master password that the user enters once. 

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

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.

PRESENTATION

Title: OpenTheory: Package Management for Higher Order Logic Theories

Speaker: Joe Hurd, Galois, Inc.

Abstract:

Interactive theorem has grown beyond toy examples in mathematics and program verification, as demonstrated by recent successes such as the Gonthier's formal proof of the four colour theorem and Leroy's verified compiler from a realistic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques, there is now a need for theory engineering techniques to support these major verification efforts.

In this talk I will present the OpenTheory project, which has defined a simple 'article' format to represent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover, compressed by a standalone tool, stored and read by a different theorem prover. Articles naturally support theory interpretations, which leads to more efficient developments of standard theories, and also provides one approach to handling difficult constructs such as monads without extending the underlying logic. Finally, the grand vision of the OpenTheory article repository is painted, with fully automatic installation and dependency resolution.

ABOUT THE GALOIS TECH TALKS:

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to donsATgaloisDOTcom is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Factor is a programming language which has been in development for a little over 5 years. Factor is influenced by Forth, Lisp, Smalltalk. Factor takes the best ideas from Forth — simplicity, short, succint, code, emphasis on interactive testing, and meta-programming. Factor also brings modern high-level language features such as garbage collection, object orientation and functional programming familiar to users of languages such as Lisp, Smalltalk and Python. Finally, recognizing that no programming language is an island, Factor is portable, ships with a full-featured standard library, deploys stand-alone binaries, and interoperates with C and Objective-C.

In this talk, I will give the rationale for Factor’s creation, present an overview of the language, and show how Factor can be used to solve real-world problems with a minimum of fuss. At the same time, I will emphasize Factor’s extensible syntax, meta-programming and reflection capabilities, and show that these features, which are unheard of in the world of mainstream programming languages, make programs easier to write, more robust, and fun.

Biography:

Slava was born in the former USSR and emigrated to New Zealand at the age of 7. He moved to Ottawa, Canada when he was 18 to study for a Bachelors and Masters degree in Mathematics.  He now resides in Minneapolis, Minnesota. An early adopter of Java, Slava wrote the popular jEdit text editor, then went on to design and implement the Factor programming language. At his day job he hacks on web apps, optimizing compilers, garbage collectors, and everything in between

. 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. If you're planning to attend, dropping a note to is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Next week's tech talk, a special treat, with Jason Dagit (aka. lispy on

haskell) dropping by to talk about using GADTs to clean up darcs' patch

theory implementation.

TITLE: Type Correct Changes A Safe Approach to Version Control Implementation

speaker: Jason Dagit

LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon

ABSTRACT:

This will be a talk about Darcs and type safe manipulations of changes:

Darcs is based on a data model, known as Patch Theory, that sets it apart from other version control systems. The power of this data model is that it allows Darcs to manage significant complexity with a relatively straightforward user interface.

We show that Generalized Algebraic Data Types (GADTs) can be used to express several fundamental invariants and properties derived from Patch Theory. This gives our compiler, GHC, a way to statically enforce our adherence to the essential rules of our data model.

Finally, we examine how these techniques can improve the quality of the darcs codebase in practice.

PRESENTER:

Jason Dagit graduated from Oregon State University with B.S. degrees in Computer Science and Mathematics. He is currently employed at PTV America while completing his Masters degree at Oregon State under co-advisors Dr. David Roundy and Dr. Martin Erwig. During his time in graduate school he has studied both usability and programming languages. He participated in the 2007 Google Summer of Code where he worked under Dr. Roundy to improve Darcs conflict handling.

ABOUT THE GALOIS TECH TALKS:

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Duncan Coutts, from Well-Typed (http://well-typed.com), will be giving a tech talk tomorrow about the technical direction of Cabal, Haskell package infrastructure, and the problems of managing very large amounts of Haskell code.

...

TITLE: The Future of Cabal -- "A language for build systems" and "Constraint solving problems in package deployment"

SPEAKER: Duncan Coutts, Well-Typed, LLP

DATE: Tuesday, Oct 7, 2008 10.30am

LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon

ABSTRACT:

This will be an informal talk and discussion on two topics:

1. A language for build systems

Build systems are easy to start but hard to get right. We'll take the view of a language designer and look at where our current tools fall down in terms of safety/correctness and expressiveness.

We'll then consider some very early ideas about what a build system language should look like and what properties it should have. Currently this takes the form of a design for a build DSL embedded in Haskell.

1. Constraint solving problems in package deployment

We are all familiar, at least peripherally, with package systems. Every Linux distribution has a notion of packages and most have high level tools to automate the installation of packages and all their dependencies. What is not immediately obvious is that the problem of resolving a consistent set of dependencies is hard, indeed it is NP-complete. It is possible to encode 3-SAT or Sudoku as a query on a specially crafted package repository.

We will look at this problem in a bit more detail and ask if the right approach might be to apply our knowledge about constraint solving rather than the current ad-hoc solvers that most real systems use. My hope is to provoke a discussion about the problem.

We can concentrate on one topic or the other depending on peoples interest.

ABOUT THE GALOIS TECH TALKS:

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Title: Bluespec: Advanced Modeling, Design and Verification using High-Level Synthesis Speaker: Rishiyur Nikhil CTO, Bluespec, Inc. Date: Thursday, October 2nd. 10.30am Location: Galois, Inc., 421 SW 6th Ave. Suite 300, (3rd floor of the Commonwealth Building)

ABSTRACT:

Over the past few years, several projects in major companies have been adopting BSV (Bluespec SystemVerilog) as their next-generation tool of choice for IP design, modeling (for both architecture exploration and early software development), and verification enviroments.

The reason for choosing BSV is its unique combination of:

(1) excellent computation model for expressing complex concurrency and communication, based on atomic transactions and atomic transactional inter-module methods

(2) very high level of abstraction and parameterization (principally inspired by Haskell)

(3) full synthesizability, enabling execution on FPGAs, obtaining better performance (3 to 4 orders of magnitude) and scalability than software simulation at comparable levels of detail.

In this presentation, I will provide a brief technical overview of BSV (points 1-3 above), and describe several customer projects using BSV. I will also briefly contrast BSV with other approaches to High Level Synthesis (particularly those based on C/C++/SystemC).

BIOGRAPHY:

Rishiyur S. Nikhil is co-founder and CTO of Bluespec, Inc., which develops tools that dramatically improve correctness, productivity, reuse and maintainability in the design, modeling and verification of digital designs (ASICs and FPGAs). The core technologies consist of a language, BSV (Bluespec SystemVerilog), which enables very abstract source descriptions based on scalable atomic transactions and extreme parameterization, and tools for high-quality synthesis of BSV into RTL. Earlier, from 2000 to 2003, he led a team inside Sandburst Corp. (later acquired by Broadcom) developing Bluespec technology and contributing to 10Gb/s enterprise network chip models, designs and design tools.

From 1991 to 2000 he was at Cambridge Research Laboratory (DEC/Compaq), including one and a half years as Acting Director. From 1984 to 1991 he was a professor of Computer Science and Engineering at MIT. He has led research teams, published widely, and holds several patents in functional programming, dataflow and multithreaded architectures, parallel processing, compiling, and EDA. He is a member of ACM and IFIP WG 2.8 on Functional Programming, and a Senior Member of IEEE. He received his Ph.D. and M.S.E.E. in Computer and Information Sciences from the Univ. of Pennsylvania, and his B.Tech in EE from IIT Kanpur.

ABOUT THE GALOIS TECH TALKS:

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

We're having an Open House to celebrate our new office space in downtown Portland's historic Commonwealth Building. Located on SW 6th Avenue between Stark and Washington streets, we're easily accessible via MAX or TriMet buses. We're up on the third floor.

Parking will also be available in the Alder Street Star Park parking garage located at 615 SW Alder, just one block from our building; validation will be provided at the event.

RSVP: Anne Marie @ ph. 503.626.6616, x153 or email anne at galois.com

Title: Theorem Proving for Verification

Speaker: John Harrison

        Principal Engineer
        Intel

Date: Tuesday, September 16th.

        10.30am

Location: Galois, Inc.

        421 SW 6th Ave. Suite 300
        (3rd floor of the Commonwealth Building)
        Portland, Oregon

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.

Biographical details:

John Harrison has worked in formal verification and automated theorem proving since 1990, when he joined Mike Gordon's "Hardware Verification Group" (HVG) at the University of Cambridge Computer Laboratory. As well as working on the development of the HOL theorem prover, he developed a particular interest in the formalization of real analysis and its application to formal verification of floating-point hardware. His PhD in this area, "Theorem Proving with the Real Numbers", written under Mike Gordon's supervision, won a UK Distinguished Dissertation award and was published as a book. He also redesigned HOL from scratch, resulting in an alternative version called HOL Light. After completing his PhD research in 1995, John Harrison spent a very enjoyable year at Abo Akademi University and Turku Centre for Computer Science (TUCS) in Turku, Finland, where he was a member of Ralph Back's Programming Methods Research Group. Among other activities, he championed the "declarative" proofs of the Mizar system and showed how these could be integrated into other theorem-provers, work subsequently taken up in DECLARE, Isar and other systems.

John Harrison then returned to Cambridge and worked on a formal model of floating-point arithmetic and its application to the verification of some realistic algorithms for transcendental functions. This work attracted the attention of Intel, and in 1998 John Harrison joined the company as a Senior Software Engineer (now Principal Engineer) specializing in the design and formal verification of mathematical algorithms. He has formally verified and in many cases designed or redesigned numerous algorithms for mathematical functions including division, square root and transcendental functions.

In his limited spare time over the past 10 years, John Harrison has been working on a book giving a comprehensive introduction to automated theorem proving.  (http://www.cambridge.org/9780521899574)

About the Galois Tech Talks.

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to <[email protected]> is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Title: Left-fold enumerators

        Towards a safe, expressive and efficient I/O interface for Haskell

Speaker: Johan Tibell

        Software Engineer
        Google

Date: Monday, September 15th.

        1pm

Location: Galois, Inc.

        421 SW 6th Ave. Suite 300
        (3rd floor of the Commonwealth Building)
        Portland, Oregon

Abstract:

I will describe a programming style for I/O operations that is based on left-fold enumerators. This style of programming is more expressive than imperative style I/O represented by the Unix functions read and write, and safer than lazy I/O using streams. Left-fold enumerators offers both high-performance using block based I/O and safety in terms of error handling and resource usage. I will demonstrate Hyena, a web server prototype written in Haskell, as an example of left-fold enumerator style of programming.

This talk is intended as a starting point for further discussions on what would be a good interface for I/O rather than a presentation of finished research.

About the Galois Tech Talks.

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to  is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

TITLE: Pretty-Printing a Really Long Formula (or, "What a Mathematician Could Learn from Haskell")

SPEAKER: Lee Pike, R&D Engineering, Galois, Inc.

DATE: Tuesday, September 9th. 10.30am

LOCATION:
Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon

ABSTRACT:

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport's brief paper, "How to Write a Long Formula" and "How to Write a Proof" in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.

I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I've written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a "HOL Normal Form" for presenting specifications, much like BNF is used for presenting language definitions.

BIOGRAPHICAL DETAILS:

http://galois.com/company/people/lee_pike/

ABOUT THE GALOIS TECH TALKS.

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Title: GpuGen: Bringing the Power of GPUs into the Haskell World

Speaker: Sean Lee

       Programming Languages & Systems
       UNSW, Sydney

Date: Tuesday, September 2nd.

       10.30am

Location: Galois, Inc.

       421 SW 6th Ave. Suite 300
       (3rd floor of the Commonwealth Building)
       Portland, Oregon

Abstract:

For the last decade, the performance of GPUs has out-grown CPUs, and their programmability has also improved to the level where they can be used fo general-purpose computations. Nonetheless, GPU programming is still limited only to those who understand the hardware architecture and the parallel processing. This is because the current GPU programming systems are based on the specialized parallel processing model, and require low-level attention in many aspects such as thread launching and synchronization.

The need for a programming system which provides a high-level abstraction layer on top of the GPU programming systems without losing the performance gain arises to facilitate the use of GPUs. Instead of writing a programming system from the scratch, the development of a Haskell extension has been chosen as the ideal approach, since the Haskell community has already accumulated a significant amount of research and resources for Nested Data Parallelism, which could be adopted to provide a high-level abstraction on GPU programming and even to broaden the applicability of GPU programming. In addition, the Foreign Function Interface of Haskell is sufficient to be the communication medium to the GPU.

GpuGen is what connects these two dots: GPUs and Haskell. It compiles the collective data operations such as scan, fold, map, etc, which incur most computation cost, to the GPU. The design of the system, the structure of the GpuGen compiler, and the current development status are to be discussed in the talk.

Biographical details:

Sean Lee is a PhD candidate at the UNSW, Sydney, working in the Programming Languages & Systems Group. This summer he's been interning at Nvidia in Santa Clara, working on programming GPUs with Haskell.

About the Galois Tech Talks.

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

TOPIC: Large Scale Monadic Refinement - Tales from L4.verified

SPEAKER: Thomas Sewell, NICTA

DATE: Wednesday , August 27th, 10.30am

LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon

ABSTRACT: Components of operating systems have emerged as an attractive target for formal analysis, thanks to the key importance of operating system correctness in establishing the security of a range of applications. These systems present a number of unique challenges for analysis, including their low level implementation and their detailed view of the system state. This talk will address none of these, instead focusing on the challenges of reasoning about (relatively) large, non-modular, inherently imperative software artefacts.

The talk will describe the formalisation of the seL4 microkernel using a state monad with nondeterminism and exceptions, present a refinement and Hoare calculus, and discuss the impact of this chosen approach on the effectiveness of the overall verification effort.

BIOGRAPHICAL DETAILS: Thomas Sewell is a software engineer with an interest in pure mathematics. He obtained his BE & BSc from UNSW in 2006, and has been working as a proof engineer for NICTA's L4.verified project for two and a half years.

ABOUT THE GALOIS TECH TALKS. Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.

Title: Adventures in Foreign Function Interfaces

Speaker: Joel Stanley

        Galois, Inc.

Date: Tuesday, August 19th, 10.30am

Location: Galois, Inc.

        421 SW 6th Ave. Suite 300
        (3rd floor of the Commonwealth Building)
        Portland, Oregon

Abstract:

In-process integration and data exchange between multiple language
runtimes is a classic software engineering challenge.  This talk
describes our experiences in building an open-source tool for
generating an "FFI bridge" between Poly/ML and OCaml, via the common
C FFI provided by both language's runtimes.

The first intended use of this tool is to programmatically generate
a bridge between Isabelle (on the Poly/ML side) and Intel's Decision
Procedure Toolkit API (on the OCaml side).

About the Galois Tech Talks.

Galois (http://galois.com) 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. If you're planning to attend, dropping
a note to <[email protected]> is appreciated, but not required.
If you're interested in giving a talk, we're always looking for new
speakers. 

Just a quick note about next week's Galois Tech Talk. Now that Galois has completed its move into downtown Portland, and a shiny new, centrally located, office space, we're opening up our tech talk series a bit more widely. If you're in Portland, and interested in functional programming and formal methods, drop by!

TITLE: Stream Fusion for Haskell Arrays

speaker: Don Stewart DATE: Tuesday, July 15th, 10.30am sharp.

LOCATION:
Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon

ABSTRACT:

Arrays have traditionally been an awkward data structure for Haskell programmers. Despite the large number of array libraries available, they have remained relatively awkward to use in comparison to the rich suite of purely functional data structures, such as fingertrees or finite maps. Arrays have simply not been first class citizens in the language.

In this talk we'll begin with a survey of the more than a dozen array types available, including some new matrix libraries developed in the past year. I'll then describe a new efficient, pure, and flexible array library for Haskell with a list like interface, based on work in the Data Parallel Haskell project, that employs stream fusion to dramatically reduce the cost of pure arrays. The implementation will be presented from the ground up, along with a discussion of the entire compilation process of the library, from source to assembly.

ABOUT THE GALOIS TECH TALKS:

Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, Don's always looking for new speakers.