Lehrstuhl Informatik II   
Sprachen und Beschreibungsstrukturen      
   Home Lehre Sommersemester 15 Seminare Tools für die Anwendung formaler Methoden bei der Software-Entwicklung login

Tools für die Anwendung formaler Methoden bei der Software-Entwicklung

Dozent:Dr. Michael Petter
Ort/Zeit:tue/wed June 9th/10th en bloque in MI 02.07.034
ModulNummer:IN2107 IN0014
Beschreibung:    We shed light on different tools that assist software development with formal methods

Seminar

The seminar is happening in MI 02.07.034 from 9:00 till 19:00

Kickoff

The recorded kickoff can be found here

Content

We see different areas in the software development, where traditional development greatly benefits from the application of formal methods during development. We will have a look at several state-of-the-art tools and upcoming approaches to leverage software development to new heights.

Topics Collection:

  • Biyik: Whitebox fuzzing with Java Path Finder
  • Dongen: Astree Runtime-Error Analyzer
  • Enghofer: Data Race Detection with Locksmith
  • Ershov: Automatic optimal fence placement in relaxed memory models with Fender
  • Foegelle: A verification oriented Programming Language: SPARK and GNATprove
  • Hahn: Another verification oriented programming language: MS Dafny and Boogie/Z3
  • Hanselmann: Programming with contract and verifying them with MS Spec#
  • O'Connor: Analyze the Reachability of Program states with CPAchecker
  • Saljic: Analyzing dynamic data structures with Predator
  • ??: Analyzing security properties of probabilistic models like communication protocols with PRISM
  • Thilo: Analyzing interactions of real time systems with UPAAL
  • ??: Verifying a C Compiler via theorem proving with Coq
  • ??: Diverse static and dynamic Java Bytecode analyses with Chord
  • ??: Dynamic Analysis of Java Bytecode with DiSL/ShadowVM
  • ??: Static Analysis to create parallelization candidates with Sambamba
  • Weicker: Symbolic Execution with KLEE/LLVM


Templates


angehängte Dateien:

    specsharp.pdf
    whiteboxfuzzing.pdf
    astree.pdf
    adagnat.pdf
    kleellvm.pdf
    dafnyboogie.pdf
    locksmith.pdf

TUM - Lehrstuhl Informatik II (Sprachen und Beschreibungsstrukturen) Thanks: Tango and TinyMCE     Generationszeit: 10 ms