| 2012 | ISoLA | Behavioral Specification Based Runtime Monitors for OSGi Services. | Jan Olaf Blech, Ylis Falcone, Harald Rue, Bernhard Schtz |
| 2011 | VMCAI | Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice. | Chih-Hong Cheng, Harald Rue, Alois C. Knoll, Christian Buckl |
| 2008 | ISoLA | Non-functional Avionics Requirements. | Michael Paulitsch, Harald Rue, Maria Sorea |
| 2004 | CADE | The ICS Decision Procedures for Embedded Deduction. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar |
| 2004 | CAV | SAL 2. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
| 2004 | CAV | An Experimental Evaluation of Ground Decision Procedures. | Leonardo Mendona de Moura, Harald Rue |
| 2004 | ICSE | Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report. | Vu Ha, Murali Rangarajan, Darren D. Cofer, Harald Rue, Bruno Dutertre |
| 2003 | CAV | Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). | Leonardo Mendona de Moura, Harald Rue, Maria Sorea |
| 2003 | ICALP | Monadic Second-Order Logics with Cardinalities. | Felix Klaedtke, Harald Rue |
| 2003 | WSC | Simulation and verification I: from simulation to verification (and back). | Harald Rue, Leonardo Mendona de Moura |
| 2002 | CADE | Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. | Leonardo Mendona de Moura, Harald Rue, Maria Sorea |
| 2001 | CAV | ICS: Integrated Canonizer and Solver. | Jean-Christophe Fillitre, Sam Owre, Harald Rue, Natarajan Shankar |
| 2001 | LICS | Deconstructing Shostak. | Harald Rue, Natarajan Shankar |
| 2001 | TACAS | A Technique for Invariant Generation. | Ashish Tiwari, Harald Rue, Hassen Sadi, Natarajan Shankar |
| 2000 | CADE | Rigid | Ashish Tiwari, Leo Bachmair, Harald Rue |
| 2000 | CAV | Integrating WS1S with PVS. | Sam Owre, Harald Rue |
| 2000 | SP | Protocol-Independent Secrecy. | Jonathan K. Millen, Harald Rue |
| 1998 | FMCAD | Solving Bit-Vector Equations. | M. Oliver Mller, Harald Rue |
| 1997 | CAV | An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. | David Cyrluk, M. Oliver Mller, Harald Rue |
| 1997 | FM | Formal Verification of Transformations for Peephole Optimization. | Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rue |
| 1996 | CADE | Reflection of Formal Tactics in a Deductive Reflection Framework. | Harald Rue |
| 1996 | CAV | Modular Verification of SRT Division. | Harald Rue, Natarajan Shankar, Mandayam K. Srivas |
| 1996 | FMCAD | Hierarchical Verification of Two-Dimensional High-Speed Multiplication in PVS: A Case Study. | Harald Rue |