Abstract QuickCheck is a powerful library for automatic test-case generation. Because QuickCheck performs random testing, some of the counterexamples discovered are very large. QuickCheck provides an interface for the user to write shrink functions to attempt to reduce the size of counterexamples. Hand-written implementations of shrink can be complex, inefficient, and consist of significant boilerplate […]

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

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

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

Abstract While the monad abstraction has risen to a certain flavor of fame in the Haskell community and beyond, its equally fascinating dual, the comonad, remains relatively unknown. I’ll tell the tale of my exploration into comonadic structures and computation, which led me to the creation of a library for concisely and generically expressing efficient […]

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

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

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

We are pleased to announce the availability of a new tech talk video: “A short examination on the intersection of security and usability (or How usable security could save us all)”, presented by Morgan Miller. For more details, please visit the talk announcement page. For more videos, please visit our Vimeo channel.

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.) title: A Gentle Introduction to Hiding Usage Patterns speaker: Rafail Ostrovsky time: Friday, 25 April 2014, 10am location: Galois Inc. 421 SW 6th Ave. Suite 300, Portland, […]