1. Formal Verification of Cyber-Physical Systems

    59:34

    from Galois Video / Added

    128 Plays / / 0 Comments

    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 in safety critical applications including aeronautics, automotive, medical devices and industrial process control, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The talk will focus on an important feature of cyber-physical systems, namely, the mixed discrete-continuous behaviors manifesting as a result of the interaction of a network of embedded processors with the physical world. Hybrid Automata are a popular formalism for modeling systems exhibiting both discrete and continuous behaviors. We discuss formal approaches for the verification of hybrid automata. More precisely, scalable approaches based on approximations, including predicate abstraction, counter-example guided abstraction refinement and bounded error approximations, will be discussed in the context of safety and stability analysis. We will present applications of the techniques on hybrid automata models. bio: Pavithra Prabhakar is on the faculty at the IMDEA Software Institute in Madrid, Spain, since 2011. Previously, she obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India. She spent the year between 2011-2012 at the California Institute of Technology as a CMI (Center for Mathematics of Information) fellow. Her main research interest is in Formal Analysis of Cyber-Physical Systems, more precisely, hybrid systems, with focus on both theoretical and practical aspects.

    + More details
    • Property Directed Reachability

      01:04:28

      from Galois Video / Added

      477 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 in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it. Relevant links: the paper http://www.eecs.berkeley.edu/~alanmi/publications/2011/fmcad11_pdr.pdf slides for the talk http://www.eecs.berkeley.edu/~alanmi/presentations/pdr01.ppt bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification

      + More details
      • Franco Bagnoli

        03:35

        from The Awareness Initiative / Added

        20 Plays / / 0 Comments

        Franco Bagnoli is a researcher in physics, in the department of Energy, University of Florence. He is the co-head of the Laboratory of Physics of Complex Systems (FiSiCo). He is also a member of the Center for the Study of Complex Systems (CSDC - University of Florence) and the local organizer of the experiment TO61 (physics and biology) of the Italian Institute of Nuclear Physics (INFN).

        + More details
        • Educed - Engineering Made Better

          02:19

          from André Passos / Added

          1,132 Plays / / 0 Comments

          Educed is company created to exploit the application of formal methods for the development of safe and reliable software systems. Educed is motivated by the strong belief that mathematically-based techniques can support industry to achieve better engineering, overcoming many of the challenges and time-consuming tasks in the specification, development and verification of high integrity systems.

          + More details
          • The Strategy Challenge in Computer Algebra

            52:19

            from Galois Video / Added

            405 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 reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different. In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worst-case doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one? The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification tool-chains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions). bio: Grant Olney Passmore is a Postdoctoral Associate at Clare Hall, University Cambridge and Research Associate at LFCS, University Edinburgh. He works on the joint Cambridge-Edinburgh EPSRC grant "Automatic Proof Procedures for Polynomials and Special Functions" with Larry Paulson (Cambridge) and Paul B. Jackson (Edinburgh), continuing work begun in his Edinburgh PhD dissertation "Combined Decision Procedures for Nonlinear Arithmetics: Real and Complex" (supervised by Paul B. Jackson). He is currently on short leave from the grant as a Visiting Researcher with Yuri Gurevich at Microsoft Research, Redmond.

            + More details
            • Verifying seL4-Based Systems

              55:53

              from Galois Video / Added

              294 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 systems. In this talk I give an overview of the ongoing work into systems verification in the Trustworthy Embedded Systems project. In particular, I will focus on the use of access control results to reason about the properties of systems in the presence of large untrusted components, such as a Linux kernel. bio: Simon Winwood is a researcher in NICTA's Trustworthy Embedded Systems project, investigating system-level security properties . Simon completed his PhD in the PLS group at UNSW. He also worked as a research engineer on the L4.verified project at NICTA. He is interested in software verification, type systems, and programming languages in general.

              + More details
              • Formal Methods Applied to Control Software

                01:04:11

                from Galois Video / Added

                452 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 understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the Frama-C tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers. bio: Alwyn Goodloe obtained his B.Sc. in Computer Science from Old Dominion University in 1985 and an M.Sc. in Mathematics from George Mason University in 1992. He worked for fourteen years in the software industry as a software engineer, database administrator, Unix system administrator, and technologist. In 1999, he returned to graduate school to study at the University of Pennsylvania, where he obtained a Ph.D. in Computer and Information Science in 2008. At Penn he conducted research in the area of computer and network security. He is currently a research scientist at the National Institute of Aerospace in Hampton, Virginia. At NIA his research focus has been formal methods applied to high-reliable systems such as avionics.

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

                  53:48

                  from Galois Video / Added

                  1,242 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. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos. bio: Lee Pike has worked in Research & Development at Galois, Inc. since 2005. His primary area of research is dependable embedded systems, including both safety-critical and security-critical systems. Previously, he was a research scientist with the NASA Langley Formal Methods Group. He has a Ph.D in Computer Science from Indiana University. He has a Best Paper award from Formal Methods in Computer-Aided Design (FMCAD’2007), and service includes being on the program committees of FMCAD and Interactive Theorem Proving. His publications and other information can be found at http://www.cs.indiana.edu/~lepike.

                  + More details
                  • Verification of Galois Field Multipliers

                    01:16:26

                    from Galois Video / Added

                    435 Plays / / 0 Comments

                    abstract: Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others. My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the word-length (k) in such multipliers can be very large: typically, k = 256. Due to such large word-lengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome. bio: Priyank Kalla recieved the Bachelors degree in Electronics engineering from Sardar Patel University in India in 1993; and Masters and PhD from University of Massachusetts Amherst in 1998 and 2002, respectively. Since 2002, he is a faculty member in the ECE Dept. at the Univ. of Utah. His research interests are in the general areas of Logic Synthesis and Design Verification. Over the past few years, he has been investigating the use of computer algebra techniques over finite integer rings (Z/mZ) and finite fields (GF(2^m)) for optimization and verification of arithmetic datapaths. He is a recepient of the NSF CAREER award and the ACM TODAES 2009 best paper award. For more information, visit http://www.ece.utah.edu/~kalla

                    + More details
                    • Introduction to Logic Synthesis

                      01:10:55

                      from Galois Video / Added

                      846 Plays / / 0 Comments

                      abstract: The lecture describes the problems solved by logic synthesis. It presents functional representations and typical computations applied to Boolean networks, such as traversal, windowing, cut computation, simulation, Boolean reasoning. Presented next are And-Inverter Graphs (AIGs) that are increasingly used as a unifying representation for all problems. The lecture is finished by an overview of AIG-based solutions in synthesis, technology mapping, and formal verification. bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification.

                      + More details

                      What are Tags?

                      Tags

                      Tags are keywords that describe videos. For example, a video of your Hawaiian vacation might be tagged with "Hawaii," "beach," "surfing," and "sunburn."