Verification and testing: Enabling behaviour tree verification via a translation to BIP.- Verified fault handling for modern board management controllers.- Testing compositionality. Formal models: Correct pattern-based development through refinements and weakest preconditions calculus.- Coq formalization of orientation representation: matrix, Euler angles, axis-angle and quaternion.- Reactive graphs in action. Security and blockchain: Extracting formal smart-contract specifications from natural language with LLMs.- How do asynchronous communication models impact the composability of information flow security?
