or cancel
  1. Empirical Sampling With Haskell

    42:52

    from Galois Video Added 473 2 0

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

    + More details
    • Building an Open-Source Autonomous Quad-Copter

      44:35

      from Galois Video Added 3,001 9 0

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

      + More details
      • Parallel K-Induction Based Model Checking

        49:25

        from Galois Video Added 217 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
        • Combining Denotational and Operational Semantics for Scalable Proof Development

          01:10:46

          from Galois Video Added 282 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
          • Candid Experiences from a Hardware Startup

            01:05:56

            from Galois Video Added 308 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
            • Galois Tech Talk: On Deadlock Verification in Micro-Architectural Models of Communication Fabrics

              55:35

              from Galois Video Added 49 0 0

              abstract: Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been…

              + More details
              • Property Directed Reachability

                01:04:28

                from Galois Video Added 713 2 0

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

                + More details
                • Program Inconsistency Detection using Weakest Preconditions

                  01:09:21

                  from Galois Video Added 414 2 0

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

                  + More details
                  • Control Flow Graph-guided Exploration in DDT

                    01:06:16

                    from Galois Video Added 506 4 0

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

                    + More details
                    • Formal Methods Applied to Control Software

                      01:04:11

                      from Galois Video Added 484 2 0

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

                      + More details
                      • Copilot: A Hard Real-Time Runtime Monitor

                        53:48

                        from Galois Video Added 1,261 2 0

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

                        + More details
                        • Databases are Categories 2: Refinements and Extensions

                          01:02:55

                          from Galois Video Added 632 1 0

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

                          + 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