s
or cancel
  1. Property Directed Reachability

    01:04:28

    by Galois Video / Added

    136 Plays / / 0 Comments

    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 introduced…

    + More details
    • Introducing Well-founded Recursion

      01:08:48

      by Galois Video / Added

      358 Plays / / 1 Comment

      + More details
      • Galois Tech Talk: On Deadlock Verification in Micro-Architectural Models of Communication Fabrics

        55:35

        by Galois Video / Added

        13 Plays / / 0 Comments

        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
        • Galois Tech Talk: Formalizing Haskell 98 in the K Semantic Framework

          56:51

          by Galois Video / Added

          269 Plays / / 0 Comments

          abstract: Formal semantics is notoriously hard. The K semantic framework is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework…

          + More details
          • Candid Experiences from a Hardware Startup

            01:05:56

            by Galois Video / Added

            144 Plays / / 0 Comments

            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 aesthetic…

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

              01:10:46

              by Galois Video / Added

              135 Plays / / 0 Comments

              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
              • Parallel K-Induction Based Model Checking

                49:25

                by Galois Video / Added

                141 Plays / / 0 Comments

                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
                • Building an Open-Source Autonomous Quad-Copter

                  44:35

                  by Galois Video / Added

                  1,913 Plays / / 0 Comments

                  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 mentored…

                  + More details
                  • Empirical Sampling With Haskell

                    42:52

                    by Galois Video / Added

                    327 Plays / / 0 Comments

                    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 approaches…

                    + More details
                    • RNA Networks

                      43:08

                      by Galois Video / Added

                      125 Plays / / 0 Comments

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

                      + More details
                      • OpenTheory

                        52:36

                        by Galois Video / Added

                        412 Plays / / 0 Comments

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

                        + More details
                        • Haskell and the Social Web

                          50:39

                          by Galois Video / Added

                          905 Plays / / 0 Comments

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

                          + More details

                          Browse 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

                          More stuff from Galois Video

                          Keyboard Shortcuts

                          Just think about it… What if you were trapped under something heavy and the mouse was out of your reach? Scary, right? That's exactly why we have these keyboard shortcuts so you can still use Vimeo until the help arrives.

                          • [ Prev video
                          • ] Next video
                          • L Like this video
                          • S Share this video
                          • F Full screen
                          • V Couch Mode
                          • M More videos
                          • ? More shortcuts