Program Analysis

Next Steps in LLM-Supported Java Verification
Next Steps in LLM-Supported Java Verification

We evaluate the effectiveness of feedback provided to a Large Language Model by the theorem prover KeY for verification of Java software using LLM-generated auxilliary annotations.

15. Dec 2024

Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification

We evaluate the potential of Large Language Models (specifically GPT 3.5 and GPT 4o) for the generation of code annotations in the Java Modelling Language using a prototypical integration of the Java verification tools KeY and JJBMC with OpenAI's API.

27. Oct 2024

An Information-Flow Perspective on Algorithmic Fairness
An Information-Flow Perspective on Algorithmic Fairness

An exploration of the relationships between qualitative and quantitative information flow and various causal and non-causal fairness definitions with applications to program analysis.

20. Feb 2024

Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis

A formal approach for the quantiative assessment of service-oriented software which combines high-level software architecture modelling with deductive verification.

8. Jan 2024

Formally Verified Algorithmic Fairness using Information-Flow Tools (Extended Abstract)
Formally Verified Algorithmic Fairness using Information-Flow Tools (Extended Abstract)

We demonstrate preliminary results on strong connections between Information Flow and Algorithmic Fairness Analysis

1. May 2023

Quantifying Software Reliability via Model-Counting
Quantifying Software Reliability via Model-Counting

We present and evaluate a pipeline allowing for the quantification of C-programs according to their specification adherence.

23. Aug 2021