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.
Network generators help to provide synthethic instances with controllable parameters by algorithm developers and researchers. KaGen provides generators for a large variety of network models, which are communication-free by making use of pseudorandomization and divide-and-conquer schemes.
KaHyPar is a fast, high-quality, and scalable algorithm for partitioning graphs and hypergraphs with billions of edges. It finds applications in minimizing communication costs for distributed (hyper)graph computations, quantum circuit simulations, storage sharding in databases, and VLSI design.
KaMPIng is a flexible and (near) zero-overhead C++ wrapper for MPI, covering the whole range of abstraction levels from low-level MPI calls to convenient STL-style bindings. This allows for both rapid prototyping and highly engineered distributed algorithms.
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
Automated Reasoning in HPC and Cloud Environments: Scheduling, Solving, Proving
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