Formal methods provide means for rigorously specifying the desired behaviour of a hardware or software system, making a precise model of its actual behaviour, and then verifying whether that actual behaviour corresponds to the specification.<br><br> My habiliation thesis reports on various contributions to this realm, where my main interest has been on algorithmic aspects. This is motivated by the observation that asymptotic worst-case complexity, often used to characterize the difficulty of algorithmic problems, is only loosely related to the difficulty encountered in solving those problems in practice.<br><br> The two main types of system I have been working on are pushdown systems and Petri nets. Both are fundamental notions of computation, and both offer, in my opinion, particularly nice opportunities for combining theory and algorithmics.<br><br> Pushdown systems are finite automata equipped with a stack; since the height of the stack is not bounded, they represent a class of infinite-state systems that model programs with (recursive) procedure calls. Moreover, we shall see that specifying authorizations is another, particularly interesting application of pushdown systems.<br><br> While pushdown systems are primarily suited to express sequential systems, Petri nets model concurrent systems. My contributions in this area all concern unfoldings. In a nutshell, the unfolding of a net N is an acyclic version of N in which loops have been unrolled. Certain verification problems, such as reachability, have a lower complexity on unfoldings than on general Petri nets.