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.

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.

Web browsers are conquer 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.

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.

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.

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 optimised and complex. Such a complex verification tool may suffer from bugs resulting in accepting some incorrect protocols as correct.

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.

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 an consumed third-party component.