Systems Analysis

SAFE provides a rigorous and automated methodology for systematically detecting errors in concurrent software, addressing the challenges posed by multi-core processors and concurrency bugs. Building on technology from the SYMBIOSYS project, SAFE’s approach has already demonstrated success in identifying bugs in real-world software.

SYMBIOSYS develops a novel methodology for analyzing the temporal and functional behavior of networked systems by combining symbolic execution with distributed and temporal execution techniques. The project enables efficient exploration of distributed execution paths, uncovering critical bugs in real-world software and advancing the reliability of networked systems.

KleeNet uses symbolic execution to detect low-probability bugs before deployment. It integrates with the COOJA simulator to enable high-coverage testing and early detection of complex interaction bugs.