Talk: Formal methods in the Industry

Moderator: Automated Theorem Proving

Beiträge: 31
Registriert: 10. Apr 2012 11:21

Talk: Formal methods in the Industry

Beitrag von bubel »

You are cordially invited to the following presentation as part of our seminar series software engineering using formal methods.
This time Keiko Nakata, an employee of the company FireEye, will talk about

“Formal Methods at FireEye: Goals and Challenges”

Date: Tue, 17th February
Time: 10:00-10:45
Room: A126 in the Piloty Building (S2|02)


FireEye is a US-based public network security company, founded in
2004. It develops an innovative security platform, which detects
malware through its malicious behaviour and uses virtualisation for
behaviour inspection.

The objective of FireEye's formal methods team in Dresden is to
mathematically prove security properties of FireEye's kernel
products. The software is written in C++, executes concurrently, uses
pointer arithmetic, embeds assembly codes, implementing system-level
infrastructure such as a micro-kernel. Currently we work with the Coq
proof assistant, applying programming language technologies. We are
also looking at off-the-shelf program analysers and verifiers.

In the talk, I will overview our goals and technical challenges.

Zurück zu „Automated Theorem Proving“