formal verification

forum

Visible to the public PhD Student or Postdoc Position in Alexander von Humboldt Professor group

Submitted by Andre Platzer on Tue, 07/12/2022 - 4:33am

The group of Andre Platzer, the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems, in the Department of Informatics at KIT is recruiting a PhD student or postdoc (TVL E13, full-time). Our research develops the logical foundations for cyber-physical systems and practical theorem proving tools for analyzing and correctly building such systems, including the theorem prover KeYmaera X, verified runtime monitoring ModelPlex, verified compilation, and verified safe machine learning techniques.

file

Visible to the public High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

Abstract: In the **High Assurance Rigorous Digital Engineering for Nuclear Safety** (HARDENS) project, Galois has developed a high-assurance, safety-critical demonstration system for the Nuclear Regulatory Commission using Rigorous Digital Engineering (RDE). The system in question is a Digital Instrumentation and Control (DI&C) system for Nuclear Power Plants (NPPs), and is called the Reactor Trip System (RTS).