or cancel
  1. Engineers Without Borders

    38:36

    from Galois Video Added 350 2 0

    abstract: 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…

    + More details
    • Automatic Function Annotations for Hoare Logic

      47:37

      from Galois Video Added 349 1 0

      abstract: 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…

      + More details
      • Verifying seL4-Based Systems

        55:53

        from Galois Video Added 324 1 0

        abstract: 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…

        + More details
        • Candid Experiences from a Hardware Startup

          01:05:56

          from Galois Video Added 306 2 0

          abstract: 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…

          + More details
          • Haskell Bytes

            01:04:03

            from Galois Video Added 298 5 0

            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…

            + More details
            • Dependently typed functional programming in Idris, 3 of 3

              59:14

              from Galois Video Added 282 4 0

              abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as…

              + More details
              • Combining Denotational and Operational Semantics for Scalable Proof Development

                01:10:46

                from Galois Video Added 273 0 0

                abstract: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…

                + More details
                • Trust relationship modeling for software assurance

                  24:54

                  from Galois Video Added 260 2 0

                  In-absentia presentation to the FAST 2010 audience. Abstract: Software assurance, as practiced through the Common Criteria, is a mixture of processes, heuristics, and lessons learned from earlier…

                  + More details
                  • Getting a Quick Fix on Comonads

                    01:13:39

                    from Galois Video Added 231 3 0

                    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…

                    + More details
                    • Parallel K-Induction Based Model Checking

                      49:25

                      from Galois Video Added 214 0 0

                      abstract: 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,…

                      + More details
                      • Tech Talk: Read-copy update (RCU) validation and verification for Linux

                        01:07:11

                        from Galois Video Added 203 1 0

                        abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002.…

                        + More details
                        • Formal Verification of Cyber-Physical Systems

                          59:34

                          from Galois Video Added 193 1 0

                          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…

                          + More details

                          Browse Videos

                          Videos Galois Video

                          Here are all of the videos that Galois Video has uploaded to Vimeo. Appearances are videos that Galois Video has been credited in by others.

                          Also Check Out