• Adjunct Professor of Practice, Computer Science & Engineering
Dr. Flemming Andersen

Educational Background

  • Ph.D. Computer Science, A Theorem Prover for UNITY in Higher Order Logic, Technical University of Denmark, Lyngby, Denmark, 1992
  • M.Sc. EE., A Formal Model of Pascal Plus - and its Realization, Technical University of Denmark, Lyngby, Denmark, 1983

Research Interests

    • Formal Methods, and Verification for Hardware and Software Systems
    • Security
    • Concurrency
    • Programming Languages
    • Semantics
    • Compilers
    • Databases
    • Theorem Proving
    • Model Checking
    • Higher Order Logic

Industry Experience

    • Research Engineer at Galois Inc. working with formal methods, and tools for verification of security and functionality of hardware and software.
    • Professor of Practice at Texas A&M University.
    • Worked at Intel as formal verification manager, technical leader and principal engineer. Responsible for the formal verification of the hardware components that implement floating point arithmetic, cache coherence protocols, and ECC on the first Atom processor, the Larrabee processors, and all the Xeon Phi Products.
    • IBM Austin Texas as technical leader of the formal verification of the first PowerPC 4 processor.
    • Visiting associate working with Professor Mani Chandy at the California Institute of Technology towards the formal verification of C-libraries using the HOL-UNITY tools set that were developed at TeleDanmark Research.
    • Owned and managed the development of internet services for two years at TeleDanmark R&D, during which the Danish yellow pages, an early IP-telephony service similar to the later Skype, and video streaming services were developed.
    • Spent two years at the IBM Heidelberg Science Center in Germany inventing and implementing a new hierarchical database language that later contributed to parts of SQL2.
    • Research scientist at TeleDanmark Research, first participating in the development of a CHILL (CCITT High Level Language) compiler and its symbolic debugger, later inventing, leading and managing the development of the HOL-UNITY system.

Selected Publications

  • Jesse Bingham, John Erickson, Gaurav Singh, Flemming Andersen. Industrial Strength Refinement Checking. FMCAD, 2009.
  • Kris Tiri, Onur Aciicmez, Michael Neve de Mevergnies, Flemming Andersen. An Analytical Model for Time-Driven Attacks. International Association for Cryptologic Research, 2007.
  • Rebekah Leslie, Levent Erkök, Flemming Andersen. Formalizing Information Flow in a Haskell Hypervisor. Published at MIKES, 2007.
  • Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen. An Abstraction Algorithm for the Verification of Generalized C-Slow Designs. Published at CAV, 2000.
  • Flemming Andersen, Kim Dam Petersen, and Jimmi S. Pettersson. A Graphical Tool for Proving UNITY Progress, pages 17–33. LNCS 859. Springer–Verlag, 1994.
  • P. Pistor and F. Andersen. Designing a Generalized NF2 Model with an SQL-like Interface. In VLDB 86, Kyoto, pages 278–288, August 1986.