Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] PhD position in Formal Methods at the Univers...


view this post on Zulip Email Gateway (Jan 18 2024 at 14:50):

From: Gerhard Schellhorn <schellhorn@informatik.uni-augsburg.de>
The chair of Prof. Reif at the University of Augsburg, Germany
is looking for new team members for a project on

Correct translation of abstract specifications to C-Code (VeriCode)

If you are a formal methods person interested in a PhD position
in our group please contact schellhorn@informatik.uni-augsburg.de.

The goal of the project is to develop a systematic approach
to translate an abstract specification language, that includes
algebraic data types, abstract, concurrent imperative programs
and software components connected by refinement to efficient
C-Code that does not need garbage collection.

To achieve this the main aim of this project is to develop
a systematic data flow analysis that allows the generation
of optimal C-Code with a minimum of copy operations.
We want to formally specify the core of the data flow analysis
and to verify that the transformation from the
specification language yields correct code without memory leaks.

We are seeking persons with a degree (M.Sc.) in computer science,
having a strong interest in formal verification, and speaking German
and English fluently.

For more information on the project see
https://www.uni-augsburg.de/en/fakultaet/fai/isse/projects/vericode/


Last updated: Apr 29 2024 at 04:18 UTC