VASSAL
VASSAL (Verification and Analysis for Safety and Security of Applications in Life) is a project funded by the European Union under Horizon Europe. It establishes a virtual research centre for the fundamental technologies behind automated verification, analysis, and model-based design of safe and secure software, from logics and automata to analysis at the source code level, and examines the economic implications of these technologies for small and medium-sized enterprises. We collaborate with Brno University of Technology, Masaryk University Brno, and CEA Paris-Saclay.
AUTOSARD
AUTOSARD (Automated Sublinear Amortised Resource Analysis of Data Structures) is funded by the Austrian Science Fund FWF (P 36623) and carried out jointly with Georg Moser (University of Innsbruck). Data structures of sublinear complexity, such as self-adjusting search trees, Fibonacci heaps, and skip lists, require potential functions containing sublinear terms such as the logarithm, which has so far largely resisted automation. We automate their amortised cost analysis by fixing a parameterised potential function, deriving a constraint system over its parameters from the program's syntax tree, and solving it with an optimising constraint solver. Starting from functional programs, we extend the approach to persistent and probabilistic data structures.