| Mechanizing and improving dependency pairs J Giesl, R Thiemann, P Schneider-Kamp, S Falke Journal of Automated Reasoning 37 (3), 155-203, 2006 | 266 | 2006 |
| LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR F Merz, S Falke, C Sinz International Conference on Verified Software: Tools, Theories, Experiments …, 2012 | 226 | 2012 |
| Automated termination proofs with AProVE J Giesl, R Thiemann, P Schneider-Kamp, S Falke International Conference on Rewriting Techniques and Applications, 210-220, 2004 | 217 | 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 | 95 | 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 | 91 | 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 …, 2011 | 73 | 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 | 67 | 2009 |
| A Precise Memory Model for {Low-Level} Bounded Model Checking C Sinz, S Falke, F Merz 5th International Workshop on Systems Software Verification (SSV 10), 2010 | 62 | 2010 |
| Improving dependency pairs J Giesl, R Thiemann, P Schneider-Kamp, S Falke Logic for Programming, Artificial Intelligence, and Reasoning: 10th …, 2003 | 57 | 2003 |
| Termination analysis of imperative programs using bitvector arithmetic S Falke, D Kapur, C Sinz Verified Software: Theories, Tools, Experiments: 4th International …, 2012 | 55 | 2012 |
| The bounded model checker LLBMC S Falke, F Merz, C Sinz 2013 28th IEEE/ACM International Conference on Automated Software …, 2013 | 53 | 2013 |
| LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) S Falke, F Merz, C Sinz International Conference on Tools and Algorithms for the Construction and …, 2013 | 41 | 2013 |
| A term rewriting approach to the automated termination analysis of imperative programs S Falke, D Kapur International Conference on Automated Deduction, 277-293, 2009 | 40 | 2009 |
| Rewriting Induction+ Linear Arithmetic= Decision Procedure S Falke, D Kapur | 39 | 2012 |
| LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation C Sinz, F Merz, S Falke | 31* | 2012 |
| Dependency pairs for rewriting with built-in numbers and semantic data structures S Falke, D Kapur International Conference on Rewriting Techniques and Applications, 94-109, 2008 | 29 | 2008 |
| Extending the theory of arrays: memset, memcpy, and beyond S Falke, F Merz, C Sinz Verified Software: Theories, Tools, Experiments: 5th International …, 2014 | 19 | 2014 |
| Inductive decidability using implicit induction S Falke, D Kapur International Conference on Logic for Programming Artificial Intelligence …, 2006 | 19 | 2006 |
| 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 | 14 | 2012 |
Jürgen GieslProfessor of Computer Science, RWTH Aachen UniversityBestätigte E-Mail-Adresse bei informatik.rwth-aachen.de
