or cancel
  1. Databases are Categories

    01:13:19

    from Galois Video / Added

    2,547 Plays / / 5 Comments

    Talk presented by David Spivak on June 3, 2010, part of the Galois Tech Talk series. See http://www.galois.com/blog/2010/05/27/tech-talk-categories-are-databases/ for slides and further information.

    + More details
    • Hacking Internet Voting via Ballot Tampering

      02:40

      from Galois Video / Added

      915 Plays / / 1 Comment

      Election Day was this week. If you took advantage of early voting, or you live overseas, you probably used a paper ballot you received in the mail a few weeks ago. A digital alternative, being considered…

      + More details
      • Introducing Well-founded Recursion

        01:08:48

        from Galois Video / Added

        481 Plays / / 1 Comment

        + More details
        • Large-Scale Static Analysis at Mozilla

          01:00:40

          from Galois Video / Added

          2,241 Plays / / 1 Comment

          Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce…

          + More details
          • The Strategy Challenge in Computer Algebra

            52:19

            from Galois Video / Added

            391 Plays / / 0 Comments

            abstract: In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: user-specifiable adaptations of general reasoning mechanisms…

            + More details
            • Faster persistent data structures through hashing

              51:19

              from Galois Video / Added

              1,387 Plays / / 0 Comments

              abstract: The most commonly used map (dictionary) data type in Haskell is implemented using a size balanced tree. While size balanced trees provide good asymptotic performance, their real world performance…

              + More details
              • Program Inconsistency Detection using Weakest Preconditions

                01:09:21

                from Galois Video / Added

                276 Plays / / 0 Comments

                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
                • Verifying seL4-Based Systems

                  55:53

                  from Galois Video / Added

                  273 Plays / / 0 Comments

                  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
                  • Control Flow Graph-guided Exploration in DDT

                    01:06:16

                    from Galois Video / Added

                    454 Plays / / 0 Comments

                    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
                    • Haskell and the Social Web

                      50:39

                      from Galois Video / Added

                      1,186 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
                      • Engineers Without Borders

                        38:36

                        from Galois Video / Added

                        343 Plays / / 0 Comments

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

                          49:25

                          from Galois Video / Added

                          197 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

                          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