A Helmholtz Pilot Program
In the information age, computers are a major driver of progress in all areas of research, technology, economy, and society. Thus, high quality software and hardware (correct, dependable, secure, efficient, with sophisticated functionality, fair, . . . ) becomes a genuine subject of provisional research and a matter of technological sovereignty. Therefore, core informatics was established by the Helmholtz Association to research on generic (yet application-oriented) methods of informatics.
Core informatics is divided into three research areas:
ArDoCo (Architecture Documentation Consistency) is a framework to connect architecture documentation and models while identifying missing or deviating elements (inconsistencies). An element can be any representable item of the model like a software component.
With CorC, we implemented an IDE to create programs following the Correctness-by-Construction approach. Starting with an abstract specification, CorC supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinements.
GBD is a comprehensive suite of tools for provisioning and sustainably maintaining benchmark instances and their metadata for empirical research on hard algorithmic problem classes.
KaRRi is a state-of-the-art dispatcher for the dynamic taxi sharing problem with meeting points. KaRRi utilizes highly engineered many-to-many shortest path queries to compute optimal assignments of riders to vehicles and according meeting points within milliseconds.
KeY is a deductive verification system for Java programs
An aXiomatic Tactical Theorem Prover for Hybrid Systems
Decentralized job scheduling platform for HPC and cloud environments, featuring an award-winning distributed engine for automated reasoning (SAT solving)
Palladio is a software architecture simulation approach which analyses software at the model level for performance bottlenecks, scalability issues, reliability threats, and allows for subsequent optimisation.
This header-only library contains a highly tuned (uncompressed) bit vector implementation with multiple space efficient rank and select support data structures. Our fastest rank and select support has a space overhead of only ~3.51% and makes use of data level parallelism via SIMD instructions.
A perfect hash function is a function that has no collisions on a given set. ShockHash constructs very compact perfect hash functions significantly faster than previous approaches.
A perfect hash function is a function that has no collisions on a given set. SicHash places objects in a cuckoo hash table and then stores the final hash function choice of each object in a retrieval data structure. Using irregular cuckoo hashing, each object has a different number of hash functions
View-based System Development on Consistent Models