Explaining Data Type Reduction in the Shape Analysis Framework. - Björn Wachter (Trustworthy Software, 2006)

A Definition and Classification of Timing Anomalies. - Jan Reineke 001; Björn Wachter; Stephan Thesing; Reinhard Wilhelm; Ilia Polian; Jochen Eisinger; Bernd Becker 001 (WCET, 2006)

Probabilistic Model Checking Modulo Theories. - Björn Wachter; Lijun Zhang 001; Holger Hermanns (QEST, 2007)

The Spotlight Principle. - Björn Wachter; Bernd Westphal (VMCAI, 2007)

Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models. - Stephan Wilhelm; Björn Wachter (WCET, 2007)

Probabilistic CEGAR. - Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2008)

Abstract Interpretation with Applications to Timing Validation. - Reinhard Wilhelm; Björn Wachter (CAV, 2008)

INFAMY: An Infinite-State Markov Model Checker. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2009)

Symbolic state traversal for WCET analysis. - Stephan Wilhelm; Björn Wachter (EMSOFT, 2009)

Improving Timing Analysis for Matlab Simulink/Stateflow. - Lili Tan; Björn Wachter; Philipp Lucas 001; Reinhard Wilhelm (ACES-MB@MoDELS, 2009)

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (Fundam. Informaticae, 2009)

PARAM: A Model Checker for Parametric Markov Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (CAV, 2010)

PASS: Abstraction Refinement for Infinite Probabilistic Models. - Ernst Moritz Hahn; Holger Hermanns; Björn Wachter; Lijun Zhang 001 (TACAS, 2010)

Best Probabilistic Transformers. - Björn Wachter; Lijun Zhang 001 (VMCAI, 2010)

Static Timing Analysis for Hard Real-Time Systems. - Reinhard Wilhelm; Sebastian Altmeyer; Claire Burguière; Daniel Grund; Jörg Herter; Jan Reineke 001; Björn Wachter; Stephan Wilhelm (VMCAI, 2010)

Language Equivalence for Probabilistic Automata. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (CAV, 2011)

Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. - Ernst Moritz Hahn; Gethin Norman; David Parker 001; Björn Wachter; Lijun Zhang 001 (QEST, 2011)

Probabilistic Logical Characterization. - Holger Hermanns; Augusto Parma; Roberto Segala; Björn Wachter; Lijun Zhang 001 (Inf. Comput., 2011)

Refined probabilistic abstraction. - Björn Wachter (2011)

Variable Probabilistic Abstraction Refinement. - Luis María Ferrer Fioriti; Ernst Moritz Hahn; Holger Hermanns; Björn Wachter (ATVA, 2012)

Improving the Precision of WCET Analysis by Input Constraints and Model-Derived Flow Constraints. - Reinhard Wilhelm; Philipp Lucas 001; Oleg Parshin; Lili Tan; Björn Wachter (Advances in Real-Time Systems, 2012)

APEX: An Analyzer for Open Probabilistic Programs. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (CAV, 2012)

On the Complexity of the Equivalence Problem for Probabilistic Automata. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (FoSSaCS, 2012)

Three tokens in Herman's algorithm. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (Formal Aspects Comput., 2012)

Verifying multi-threaded software with impact. - Björn Wachter; Daniel Kroening; Joël Ouaknine (FMCAD, 2013)

On the Complexity of Equivalence and Minimisation for Q-weighted Automata - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (Log. Methods Comput. Sci., 2013)

Algorithmic probabilistic game semantics - Playing games with automata. - Stefan Kiefer; Andrzej S. Murawski; Joël Ouaknine; Björn Wachter; James Worrell 001 (Formal Methods Syst. Des., 2013)

Stability and Complexity of Minimising Probabilistic Automata. - Stefan Kiefer; Björn Wachter (ICALP (2), 2014)

AbPress: Flexing Partial-Order Reduction and Abstraction. - Daniel Kroening; Subodh Sharma 001; Björn Wachter (CoRR, 2014)

Verifying synchronous reactive systems using lazy abstraction. - Kumar Madhukar; Mandayam K. Srivas; Björn Wachter; Daniel Kroening; Ravindra Metta (DATE, 2015)

Accelerating Invariant Generation. - Kumar Madhukar; Björn Wachter; Daniel Kroening; Matt Lewis; Mandayam K. Srivas (FMCAD, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (T). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ASE, 2015)

Synthesising Interprocedural Bit-Precise Termination Proofs (extended version). - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (CoRR, 2015)

Sound static deadlock analysis for C/Pthreads. - Daniel Kroening; Daniel Poetzl; Peter Schrammel; Björn Wachter (ASE, 2016)

Sound Static Deadlock Analysis for C/Pthreads (Extended Version). - Daniel Kroening; Daniel Poetzl; Peter Schrammel; Björn Wachter (CoRR, 2016)

Bit-Precise Procedure-Modular Termination Analysis. - Hong-Yi Chen; Cristina David; Daniel Kroening; Peter Schrammel; Björn Wachter (ACM Trans. Program. Lang. Syst., 2018)