Machine learning and artificial intelligence used successfully in many application areas. Still, its use in high-assurance systems is limited by the lack of formal verification techniques that satisfy the requirements of industrial certification standards such as EN 50128 (safety) or Common Criteria (security) that high-assurance systems often need to comply to.

The formal analysis of security protocols is dominated by automated protocol verification tools. They are based on abstract interpretation techniques and other over-approximations and their implementations are highly optimized and complex.

Application Security Testing (*AST) is a corner stone of secure software development or a Security Development Life Cycle (SDLC). To improve the efficiency and effectiveness of security testing we research on hybrid approaches: combining dynamic, static, and interactive testing as well as testing of hybrid applications.

Theorem-prover based testing combines testing and verification: tests are derived from a formal specification (or model, i.e., it is a model-based testing technique) proof techniques. HOL-TestGen is a theorem-prover based testing environment on top of Isabelle.

HOL-OCL enables the formal analysis of UML/OCL models by addressing two key issues: first, it provides a formal semantics that aims for standard compliance (e.g., a four-valued logic) and, second, it is verification environment for UML/OCL.

Web browsers are conquering more and more areas of our interactions with IT systems. In fact, they are increasingly taking over the role of operating systems: critical parts of personal or business life are supported by web apps, i.e., executed in the browser.

Application security programs, as part of a Security Development Life Cycle (SDLC) often need to prove that they actually pay off. Also, it is not always clear what are the most economical way of fixing a security vulnerability - in particular if the vulnerability is, as part of a secure software supply-chain a consumed third-party component.

Modern enterprise systems need to implement and comply to increasingly complex security, compliance, and privacy policies. To address this need, we developed SecureBPMN, a model-driven security approach for process-driven systems.

Security policies often need to resolve the conflict between protecting assets (or complying with laws and regulations) and the risk of hindering businesses or people. For example, health records are sensitive and need to be protected carefully. At the same time, hindering doctors to access, in an emergency, them might endanger lives.