automated proof

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 - 3: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.

group_project

Visible to the public TTP: Medium: Crowd Sourcing Annotations

Submitted by David Cok on Thu, 12/21/2017 - 12:35pm

Both sound software verification techniques and heuristic software flaw-finding tools benefit from the presence of software annotations that describe the behavior of software components. Function summaries (in the form of logical annotations) allow modular checking of software and more precise reasoning. However, such annotations are difficult to write and not commonly produced by software developers, despite their benefits to static analysis. The Crowdsourcing Annotations project will address this deficiency by encouraging software-community-based crowd-sourced generation of annotations.

Outcomes Report URL: 
https://www.research.gov/research-portal/appmanager/base/desktop?_nfpb=true&_win...