• Sesamo Project – The SESAMO project addresses the root causes of problems arising with convergence of safety and security in embedded systems at architectural level.


  • TTool is a toolkit dedicated to the edition of UML and SysML diagrams, and to the simulation and formal verification (safety, security, performance) of those diagrams.
  • HEPSYCODE is a prototypal tool to improve the design time of embedded applications. It is based on a System-Level methodology for HW/SW CO-DEsign of HEterogeneous Parallel dedicated SYstems. The whole framework drives the designer from an Electronic System-Level (ESL) behavioral model, with related Non-Functional requirements, including real-time and mixed-criticality ones, to the final HW/SW implementation, considering specific HW technologies, scheduling policies and Inter-Process Communication mechanisms.
  • ANaConDA is a framework that simplifies the creation of dynamic analysers for analysing multithreaded C/C++ programs on the binary level. The framework provides a monitoring layer offering notification about important events, such as thread synchronisation or memory accesses, so that developers of dynamic analysers can focus solely on coding the logic of their analysers. In addition, the framework also supports noise injection techniques to increase the number of thread interleavings witnessed in testing runs and hence to increase chances to find concurrency-related errors.
  • Perun is a performance versioning system and a performance tool suite. It serves as a wrapper over existing version control systems (such as git) and maintains the context of performance profiles for individual versions of programs. Perun is not focused on any particular application domain and can be used for regular performance testing of programs or for catching performance bugs early in the development. Perun can be used, e.g., to find performance bugs in the project, to model the overall performance or resource consumption for different configurations and runs of the project, to verify performance expectations (e.g. that some cryptographic functions work in the same time for all kinds of keys), or to find time-consuming or faulty inputs for the programs. 
  • 2LS is a verification tool for C programs. It is built upon the CPROVER framework (, which supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It allows verifying array bounds (buffer overflows), pointer safety, exceptions, user-specified assertions, and termination properties. The analysis is performed by template-based predicate synthesis and abstraction refinements techniques.
  • VeriFIT Static Analysis Plugins is the suite of tools for static analysis developed by BUT within the project that includes several completely new or significantly extended tools or plugins of generic static analysis frameworks. They target both safety properties (in particular, memory-related and concurrency-related) as well as performance properties.