Mechanizing and improving dependency pairs J Giesl, R Thiemann, P Schneider-Kamp, S Falke Journal of automated reasoning 37 (3), 155-203, 2006 | 253 | 2006 |
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR F Merz, S Falke, C Sinz Verified Software: Theories, Tools, Experiments: 4th International …, 2012 | 216 | 2012 |
Automated Termination Proofs with AProVE J Giesl, R Thiemann, P Schneider-Kamp, S Falke Rewriting Techniques and Applications: 15th International Conference, RTA …, 2004 | 207 | 2004 |
Alternating runtime and size complexity analysis of integer programs M Brockschmidt, F Emmes, S Falke, C Fuhs, J Giesl Tools and Algorithms for the Construction and Analysis of Systems: 20th …, 2014 | 88 | 2014 |
Analyzing runtime and size complexity of integer programs M Brockschmidt, F Emmes, S Falke, C Fuhs, J Giesl ACM Transactions on Programming Languages and Systems (TOPLAS) 38 (4), 1-50, 2016 | 81 | 2016 |
Termination analysis of C programs using compiler intermediate languages S Falke, D Kapur, C Sinz 22nd International Conference on Rewriting Techniques and Applications (RTA'11), 2011 | 66 | 2011 |
Proving termination of integer term rewriting C Fuhs, J Giesl, M Plücker, P Schneider-Kamp, S Falke Rewriting Techniques and Applications: 20th International Conference, RTA …, 2009 | 64 | 2009 |
A precise memory model for low-level bounded model checking C Sinz, S Falke, F Merz Proceedings of the 5th international conference on Systems software …, 2010 | 58 | 2010 |
Termination analysis of imperative programs using bitvector arithmetic S Falke, D Kapur, C Sinz Verified Software: Theories, Tools, Experiments: 4th International …, 2012 | 53 | 2012 |
Improving dependency pairs J Giesl, R Thiemann, P Schneider-Kamp, S Falke Logic for Programming, Artificial Intelligence, and Reasoning: 10th …, 2003 | 51 | 2003 |
The bounded model checker LLBMC S Falke, F Merz, C Sinz 2013 28th IEEE/ACM International Conference on Automated Software …, 2013 | 49 | 2013 |
LLBMC: Improved bounded model checking of C programs using LLVM S Falke, F Merz, C Sinz Tools and Algorithms for the Construction and Analysis of Systems 7795, 623-626, 2013 | 41 | 2013 |
A term rewriting approach to the automated termination analysis of imperative programs S Falke, D Kapur Automated Deduction–CADE-22: 22nd International Conference on Automated …, 2009 | 37 | 2009 |
LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation C Sinz, F Merz, S Falke | 32* | 2012 |
Rewriting Induction+ Linear Arithmetic= Decision Procedure S Falke, D Kapur | 31 | 2012 |
Dependency pairs for rewriting with built-in numbers and semantic data structures S Falke, D Kapur Rewriting Techniques and Applications: 19th International Conference, RTA …, 2008 | 27 | 2008 |
Inductive decidability using implicit induction S Falke, D Kapur Logic for Programming, Artificial Intelligence, and Reasoning: 13th …, 2006 | 19 | 2006 |
Extending the Theory of Arrays: memset, memcpy, and Beyond S Falke, F Merz, C Sinz Verified Software: Theories, Tools, Experiments: 5th International …, 2014 | 17 | 2014 |
AProVE: A system for proving termination J Giesl, R Thiemann, P Schneider-Kamp, S Falke Extended Abstracts of the 6th International Workshop on Termination, WST 3 …, 2003 | 16 | 2003 |
A Theory of Arrays with set and copy Operations S Falke, C Sinz, F Merz SMT Workshop 2012 10th International Workshop on Satisfiability Modulo …, 2012 | 13 | 2012 |