Andrey Rybalchenko
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
60
Venues
21
Active years
2004–2021
Best venue rank
A*
Where they publish
Papers
60 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2021 | CPAIOR | Supercharging Plant Configurations Using Z3. | Nikolaj S. Bjrner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati |
| 2019 | TACAS | SL-COMP: Competition of Solvers for Separation Logic. | Mihaela Sighireanu, Juan Antonio Navarro Prez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Toms Vojnar, Constantin Enea, Ondrej Lengl, Chong Gao, Zhilin Wu |
| 2019 | VMCAI | Fast BGP Simulation of Large Datacenters. | Nuno P. Lopes, Andrey Rybalchenko |
| 2017 | SOSP | CrystalNet: Faithfully Emulating Large Production Networks. | Hongqiang Harry Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno P. Lopes, Andrey Rybalchenko, Guohan Lu, Lihua Yuan |
| 2016 | PLDI | Cardinalities and universal quantifiers for verifying parameterized systems. | Klaus von Gleissenthall, Nikolaj S. Bjrner, Andrey Rybalchenko |
| 2016 | POPL | Scaling network verification using symmetry and surgery. | Gordon D. Plotkin, Nikolaj S. Bjrner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese |
| 2015 | CAV | Symbolic Polytopes for Quantitative Interpolation and Verification. | Klaus von Gleissenthall, Boris Kpf, Andrey Rybalchenko |
| 2014 | CAV | Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk). | Klaus von Gleissenthall, Andrey Rybalchenko, Santiago Zanella-Bguelin |
| 2014 | FMCAD | Reduction for compositional verification of multi-threaded programs. | Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm |
| 2014 | POPL | A constraint-based approach to solving games on infinite graphs. | Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko |
| 2013 | APLAS | Separation Logic Modulo Theories. | Juan Antonio Navarro Prez, Andrey Rybalchenko |
| 2013 | CAV | Solving Existentially Quantified Horn Clauses. | Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko |
| 2013 | CONCUR | An Epistemic Perspective on Consistency of Concurrent Computations. | Klaus von Gleissenthall, Andrey Rybalchenko |
| 2013 | SAS | On Solving Universally Quantified Horn Clauses. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2013 | TACAS | Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). | Corneliu Popeea, Andrey Rybalchenko |
| 2012 | CADE | Program Verification as Satisfiability Modulo Theories. | Nikolaj S. Bjrner, Kenneth L. McMillan, Andrey Rybalchenko |
| 2012 | PLDI | Synthesizing software verifiers from proof rules. | Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko |
| 2012 | SAS | Binary Reachability Analysis of Higher Order Functional Programs. | Rusln Ledesma-Garza, Andrey Rybalchenko |
| 2012 | TACAS | HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). | Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko |
| 2012 | TACAS | Compositional Termination Proofs for Multi-threaded Programs. | Corneliu Popeea, Andrey Rybalchenko |
| 2011 | APLAS | Solving Recursion-Free Horn Clauses over LI+UIF. | Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2011 | CAV | Threader: A Constraint-Based Verifier for Multi-threaded Programs. | Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2011 | CAV | HMC: Verifying Functional Programs Using Abstract Interpreters. | Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko |
| 2011 | PLDI | Separation logic + superposition calculus = heap theorem prover. | Juan Antonio Navarro Prez, Andrey Rybalchenko |
| 2011 | POPL | Predicate abstraction and refinement for verifying multi-threaded programs. | Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2011 | PPDP | Towards automatic synthesis of software verification tools. | Andrey Rybalchenko |
| 2011 | TACAS | Transition Invariants and Transition Predicate Abstraction for Program Termination. | Andreas Podelski, Andrey Rybalchenko |
| 2011 | VMCAI | Distributed and Predictable Software Model Checking. | Nuno P. Lopes, Andrey Rybalchenko |
| 2010 | ATVA | Non-monotonic Refinement of Control Abstraction for Concurrent Programs. | Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko |
| 2010 | CAV | Constraint Solving for Program Verification: Theory and Practice by Example. | Andrey Rybalchenko |
| 2010 | CSL | Constraint Solving for Program Verification: Theory and Practice by Example. | Andrey Rybalchenko |
| 2010 | LPAR | Aligators for Arrays (Tool Paper). | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrey Rybalchenko |
| 2010 | SAS | Thread-Modular Counterexample-Guided Abstraction Refinement. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2009 | CAV | InvGen: An Efficient Invariant Generator. | Ashutosh Gupta, Andrey Rybalchenko |
| 2009 | CAV | Cardinality Abstraction for Declarative Networking Applications. | Juan Antonio Navarro Prez, Andrey Rybalchenko, Atul Singh |
| 2009 | FMCAD | Finding heap-bounds for hardware synthesis. | Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jir Simsa, Satnam Singh, Viktor Vafeiadis |
| 2009 | PADL | Operational Semantics for Declarative Networking. | Juan Antonio Navarro Prez, Andrey Rybalchenko |
| 2009 | POPL | Verifying liveness for asynchronous programs. | Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko |
| 2009 | SP | Automatic Discovery and Quantification of Information Leaks. | Michael Backes, Boris Kpf, Andrey Rybalchenko |
| 2009 | SYNASC | Automated Methods for Proving Program Termination and Liveness. | Andrey Rybalchenko |
| 2009 | TACAS | From Tests to Proofs. | Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko |
| 2008 | CAV | Proving Conditional Termination. | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
| 2008 | CAV | Heap Assumptions on Demand. | Andreas Podelski, Andrey Rybalchenko, Thomas Wies |
| 2008 | POPL | Proving non-termination. | Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu |
| 2007 | PADL | ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. | Andreas Podelski, Andrey Rybalchenko |
| 2007 | PLDI | Path invariants. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2007 | PLDI | Proving thread termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2007 | POPL | Proving that programs eventually do something good. | Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi |
| 2007 | SAS | Precise Thread-Modular Verification. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2007 | VMCAI | Invariant Synthesis for Combined Theories. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2007 | VMCAI | Constraint Solving for Interpolation. | Andrey Rybalchenko, Viorica Sofronie-Stokkermans |
| 2006 | CAV | Terminator: Beyond Safety. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | ICTAC | Thread-Modular Verification Is Cartesian Abstract Interpretation. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2006 | ICTAC | Model Checking Duration Calculus: A Practical Approach. | Roland Meyer, Johannes Faber, Andrey Rybalchenko |
| 2006 | PLDI | Termination proofs for systems code. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2005 | POPL | Transition predicate abstraction and fair termination. | Andreas Podelski, Andrey Rybalchenko |
| 2005 | SAS | Abstraction Refinement for Termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2005 | TACAS | Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. | Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
| 2004 | LICS | Transition Invariants. | Andreas Podelski, Andrey Rybalchenko |
| 2004 | VMCAI | A Complete Method for the Synthesis of Linear Ranking Functions. | Andreas Podelski, Andrey Rybalchenko |