Verified Computing Tools

Over the last decade SAT and SMT solver technology has revolutionized our ability to prove many relevant properties of substantial pieces of software. The fact that verifying software approaches practical feasibility today is based on two corner stones: it is certainly the theoretical advancements in the theory of verification, but even more so the practical improvements in the performance proof engines. This presentations in this session show how software verification tools benefit from the enormous improvements in prover technology to automate different kinds of verification activities.

Speaker Details

Andy Gordon is a Principal Researcher at MSR Cambridge. His research interests are in the general areas of security and programming languages. His work at Microsoft has involved applying type theory and other formal techniques to problems of computer security, in projects including the following: an analysis (with Don Syme) of the type system underlying the bytecode verifier of the Microsoft .NET Common Language Runtime; Cryptyc (with Alan Jeffrey), a type-checker for cryptographic protocols; and the Samoa Project (with Karthik Bhargavan and Cédric Fournet) on formal tools for the security of XML Web Services. He is currently excited about the many possibilities of refinement types, and is actively developing them in the context of F7, an enhanced typechecker for the F# programming language. F7 is work in collaboration with Karthik Bhargavan, Cédric Fournet, and our colleagues.

Bart Jacobs is a professor of computer science at the Katholieke Universiteit Leuven, Belgium. His research focus is on the verification of safety and security properties of imperative programs. He obtained his PhD at Katholieke Universiteit Leuven, supervised by Prof. Frank Piessens, in 2007. During his PhD, he interned extensively in the Spec# team at Microsoft Research in Redmond, WA, USA.

Dr. Markus Dahlweid is a Lead Software Design Engineer at the European Microsoft Innovation Center in Aachen, Germany.

Dr. Dahlweid studied Computer Sciences and holds a PhD from Bremen University on “High Level Transition Systems of CSP Specifications”. Before joining Microsoft, he worked at Verified Systems, Bremen as software development and testing engineer, with special focus on safety-critical embedded systems in the area of avionics. After joining the European Microsoft Innovation Center (EMIC) in 2008, his primary focus was on verifying the Microsoft Hyper-V Hypervisor kernel as part of the Verisoft XT research project funded by BMBF and developing the verification tools needed to verify C code. His current focus is on the design and implementation of tools and method for model based development, especially on the topic of design-space exploration of models capturing functional- and non-functional requirements.

Date:
Speakers:
Andy Gordon, Bart Jacobs, and Markus Dahlweid
Affiliation:
MSR Cambridge, Katholieke Universiteit Leuven, European Microsoft Innovation Center
    • Portrait of Andy Gordon

      Andy Gordon

      Partner Research Manager

    • Portrait of Jeff Running

      Jeff Running

    • Portrait of Markus Dahlweid

      Markus Dahlweid