or cancel
  1. OpenTheory

    52:36

    from Galois Video / Added

    837 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

      from Galois Video / Added

      1,176 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

        342 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
        • Faster persistent data structures through hashing

          51:19

          from Galois Video / Added

          1,368 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
          • The Strategy Challenge in Computer Algebra

            52:19

            from Galois Video / Added

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

              55:53

              from Galois Video / Added

              263 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
              • Program Inconsistency Detection using Weakest Preconditions

                01:09:21

                from Galois Video / Added

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

                  01:06:16

                  from Galois Video / Added

                  438 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
                  • The Rubinius Virtual Machine

                    01:09:36

                    from Galois Video / Added

                    1,779 Plays / / 0 Comments

                    abstract: Ruby is a highly dynamic, strongly-typed programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single…

                    + More details
                    • Formal Methods Applied to Control Software

                      01:04:11

                      from Galois Video / Added

                      438 Plays / / 0 Comments

                      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,219 Plays / / 0 Comments

                        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

                          527 Plays / / 0 Comments

                          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

                          Galois Tech Talks” by Galois Video has 35 videos.

                          Follow

                          Browse This Channel

                          Channels are a simple, beautiful way to showcase and watch videos. Browse more Channels. Channels