We develop formal, mathematically precise methods for the description and analysis of hardware or software systems. The developed methods are implemented in tools and evaluated on case studies. Besides sequential verification techniques we currently focus on (a) verification of parallel programs, in particular concurrent data structures and software transactional memory algorithms, (b) taint analysis of Android apps and (c) the analysis of “learned” software. More information can be found on our research pages.