A complete method for the synthesis of linear ranking functions A Podelski, A Rybalchenko International Workshop on Verification, Model Checking, and Abstract …, 2004 | 545 | 2004 |
Termination proofs for systems code B Cook, A Podelski, A Rybalchenko ACM SIGPLAN Notices 41 (6), 415-426, 2006 | 476 | 2006 |
Transition invariants A Podelski, A Rybalchenko Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science …, 2004 | 380 | 2004 |
Synthesizing software verifiers from proof rules S Grebenshchikov, NP Lopes, C Popeea, A Rybalchenko ACM SIGPLAN Notices 47 (6), 405-416, 2012 | 345 | 2012 |
Horn clause solvers for program verification N Bjørner, A Gurfinkel, K McMillan, A Rybalchenko Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the …, 2015 | 304 | 2015 |
Automatic discovery and quantification of information leaks M Backes, B Köpf, A Rybalchenko 2009 30th IEEE Symposium on Security and Privacy, 141-153, 2009 | 277 | 2009 |
Path invariants D Beyer, TA Henzinger, R Majumdar, A Rybalchenko Proceedings of the 28th ACM SIGPLAN Conference on Programming Language …, 2007 | 261 | 2007 |
Proving non-termination A Gupta, TA Henzinger, R Majumdar, A Rybalchenko, RG Xu Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2008 | 230 | 2008 |
ARMC: the logical choice for software model checking with abstraction refinement A Podelski, A Rybalchenko Practical Aspects of Declarative Languages: 9th International Symposium …, 2007 | 207 | 2007 |
Invgen: An efficient invariant generator A Gupta, A Rybalchenko Computer Aided Verification: 21st International Conference, CAV 2009 …, 2009 | 205 | 2009 |
TERMINATOR: beyond safety B Cook, A Podelski, A Rybalchenko Computer Aided Verification, 415-418, 2006 | 184* | 2006 |
Proving program termination B Cook, A Podelski, A Rybalchenko Communications of the ACM 54 (5), 88-98, 2011 | 174 | 2011 |
On solving universally quantified horn clauses N Bjørner, K McMillan, A Rybalchenko Static Analysis: 20th International Symposium, SAS 2013, Seattle, WA, USA …, 2013 | 161 | 2013 |
Abstraction refinement for termination B Cook, A Podelski, A Rybalchenko Static Analysis: 12th International Symposium, SAS 2005, London, UK …, 2005 | 149 | 2005 |
Automatically verifying reachability and well-formedness in P4 Networks N Lopes, N Bjørner, N McKeown, A Rybalchenko, D Talayco, G Varghese Technical Report, Tech. Rep, 2016 | 144 | 2016 |
Transition predicate abstraction and fair termination A Podelski, A Rybalchenko ACM SIGPLAN Notices 40 (1), 132-144, 2005 | 143 | 2005 |
Invariant synthesis for combined theories D Beyer, TA Henzinger, R Majumdar, A Rybalchenko International Workshop on Verification, Model Checking, and Abstract …, 2007 | 138 | 2007 |
Proving that programs eventually do something good B Cook, A Gotsman, A Podelski, A Rybalchenko, MY Vardi ACM SIGPLAN Notices 42 (1), 265-276, 2007 | 136 | 2007 |
Solving existentially quantified horn clauses TA Beyene, C Popeea, A Rybalchenko Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013 | 129 | 2013 |
Predicate abstraction and refinement for verifying multi-threaded programs A Gupta, C Popeea, A Rybalchenko Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2011 | 123 | 2011 |