Abstract EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable security style and cryptographic implementations used in practice; as a consequence, real-world cryptography is sometimes considered as “one of the many ongoing disaster areas in security. We have […]

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

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