Transition Invariants. - Andreas Podelski; Andrey Rybalchenko (LICS, 2004)

A Complete Method for the Synthesis of Linear Ranking Functions. - Andreas Podelski; Andrey Rybalchenko (VMCAI, 2004)

Temporal verification with transition invariants. - Andrey Rybalchenko (2005)

Temporale Verifikation mit Transitionsinvarianten. - Andrey Rybalchenko (Ausgezeichnete Informatikdissertationen, 2005)

Abstraction Refinement for Termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (SAS, 2005)

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. - Amir Pnueli; Andreas Podelski; Andrey Rybalchenko (TACAS, 2005)

Terminator: Beyond Safety. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (CAV, 2006)

Thread-Modular Verification Is Cartesian Abstract Interpretation. - Alexander Malkis; Andreas Podelski; Andrey Rybalchenko (ICTAC, 2006)

Model Checking Duration Calculus: A Practical Approach. - Roland Meyer 001; Johannes Faber; Andrey Rybalchenko (ICTAC, 2006)

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. - Jörg Hoffmann 001; Jan-Georg Smaus; Andrey Rybalchenko; Sebastian Kupferschmid; Andreas Podelski (MoChArt, 2006)

Termination proofs for systems code. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (PLDI, 2006)

ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. - Andreas Podelski; Andrey Rybalchenko (PADL, 2007)

Path invariants. - Dirk Beyer 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko (PLDI, 2007)

Proving thread termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (PLDI, 2007)

Proving that programs eventually do something good. - Byron Cook; Alexey Gotsman; Andreas Podelski; Andrey Rybalchenko; Moshe Y. Vardi (POPL, 2007)

Precise Thread-Modular Verification. - Alexander Malkis; Andreas Podelski; Andrey Rybalchenko (SAS, 2007)

Invariant Synthesis for Combined Theories. - Dirk Beyer 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko (VMCAI, 2007)

Transition predicate abstraction and fair termination. - Andreas Podelski; Andrey Rybalchenko (ACM Trans. Program. Lang. Syst., 2007)

Proving Conditional Termination. - Byron Cook; Sumit Gulwani; Tal Lev-Ami; Andrey Rybalchenko; Mooly Sagiv (CAV, 2008)

Heap Assumptions on Demand. - Andreas Podelski; Andrey Rybalchenko; Thomas Wies (CAV, 2008)

Proving non-termination. - Ashutosh Gupta 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko; Ru-Gang Xu (POPL, 2008)

Model checking Duration Calculus: a practical approach. - Roland Meyer 001; Johannes Faber; Jochen Hoenicke; Andrey Rybalchenko (Formal Aspects Comput., 2008)

InvGen: An Efficient Invariant Generator. - Ashutosh Gupta 001; Andrey Rybalchenko (CAV, 2009)

Cardinality Abstraction for Declarative Networking Applications. - Juan Antonio Navarro Pérez; Andrey Rybalchenko; Atul Singh (CAV, 2009)

Finding heap-bounds for hardware synthesis. - Byron Cook; Ashutosh Gupta 001; Stephen Magill; Andrey Rybalchenko; Jirí Simsa; Satnam Singh; Viktor Vafeiadis (FMCAD, 2009)

Operational Semantics for Declarative Networking. - Juan Antonio Navarro Pérez; Andrey Rybalchenko (PADL, 2009)

Verifying liveness for asynchronous programs. - Pierre Ganty; Rupak Majumdar; Andrey Rybalchenko (POPL, 2009)

Automatic Discovery and Quantification of Information Leaks. - Michael Backes 001; Boris Köpf; Andrey Rybalchenko (SP, 2009)

Subsumer-First: Steering Symbolic Reachability Analysis. - Andrey Rybalchenko; Rishabh Singh (SPIN, 2009)

Automated Methods for Proving Program Termination and Liveness. - Andrey Rybalchenko (SYNASC, 2009)

Summarization for termination: no return! - Byron Cook; Andreas Podelski; Andrey Rybalchenko (Formal Methods Syst. Des., 2009)

Non-monotonic Refinement of Control Abstraction for Concurrent Programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (ATVA, 2010)

Constraint Solving for Program Verification: Theory and Practice by Example. - Andrey Rybalchenko (CAV, 2010)

Approximation and Randomization for Quantitative Information-Flow Analysis. - Boris Köpf; Andrey Rybalchenko (CSF, 2010)

Aligators for Arrays (Tool Paper). - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrey Rybalchenko (LPAR (Yogyakarta), 2010)

Thread-Modular Counterexample-Guided Abstraction Refinement. - Alexander Malkis; Andreas Podelski; Andrey Rybalchenko (SAS, 2010)

Refinement type inference via abstract interpretation - Ranjit Jhala; Rupak Majumdar; Andrey Rybalchenko (CoRR, 2010)

Constraint solving for interpolation. - Andrey Rybalchenko; Viorica Sofronie-Stokkermans (J. Symb. Comput., 2010)

Applying Prolog to develop distributed systems. - Nuno P. Lopes; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Atul Singh (Theory Pract. Log. Program., 2010)

Solving Recursion-Free Horn Clauses over LI+UIF. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (APLAS, 2011)

Threader: A Constraint-Based Verifier for Multi-threaded Programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (CAV, 2011)

HMC: Verifying Functional Programs Using Abstract Interpreters. - Ranjit Jhala; Rupak Majumdar; Andrey Rybalchenko (CAV, 2011)

Separation logic + superposition calculus = heap theorem prover. - Juan Antonio Navarro Pérez; Andrey Rybalchenko (PLDI, 2011)

Predicate abstraction and refinement for verifying multi-threaded programs. - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (POPL, 2011)

Towards automatic synthesis of software verification tools. - Andrey Rybalchenko (PPDP, 2011)

Transition Invariants and Transition Predicate Abstraction for Program Termination. - Andreas Podelski; Andrey Rybalchenko (TACAS, 2011)

Distributed and Predictable Software Model Checking. - Nuno P. Lopes; Andrey Rybalchenko (VMCAI, 2011)

Proving program termination. - Byron Cook; Andreas Podelski; Andrey Rybalchenko (Commun. ACM, 2011)

Program Verification as Satisfiability Modulo Theories. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (SMT@IJCAR, 2012)

Synthesizing software verifiers from proof rules. - Sergey Grebenshchikov; Nuno P. Lopes; Corneliu Popeea; Andrey Rybalchenko (PLDI, 2012)

Binary Reachability Analysis of Higher Order Functional Programs. - Ruslán Ledesma-Garza; Andrey Rybalchenko (SAS, 2012)

HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). - Sergey Grebenshchikov; Ashutosh Gupta 001; Nuno P. Lopes; Corneliu Popeea; Andrey Rybalchenko (TACAS, 2012)

Compositional Termination Proofs for Multi-threaded Programs. - Corneliu Popeea; Andrey Rybalchenko (TACAS, 2012)

Separation Logic Modulo Theories. - Juan Antonio Navarro Pérez; Andrey Rybalchenko (APLAS, 2013)

Solving Existentially Quantified Horn Clauses. - Tewodros A. Beyene; Corneliu Popeea; Andrey Rybalchenko (CAV, 2013)

An Epistemic Perspective on Consistency of Concurrent Computations. - Klaus von Gleissenthall; Andrey Rybalchenko (CONCUR, 2013)

On Solving Universally Quantified Horn Clauses. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (SAS, 2013)

Automation of Quantitative Information-Flow Analysis. - Boris Köpf; Andrey Rybalchenko (SFM, 2013)

Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). - Corneliu Popeea; Andrey Rybalchenko (TACAS, 2013)

Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. - Nikolaj S. Bjørner; Kenneth L. McMillan; Andrey Rybalchenko (CoRR, 2013)

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). - Bernadette Charron-Bost; Stephan Merz; Andrey Rybalchenko; Josef Widder (Dagstuhl Reports, 2013)

From tests to proofs. - Ashutosh Gupta 001; Rupak Majumdar; Andrey Rybalchenko (Int. J. Softw. Tools Technol. Transf., 2013)

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk). - Klaus von Gleissenthall; Andrey Rybalchenko; Santiago Zanella-Béguelin (VPT@CAV, 2014)

Reduction for compositional verification of multi-threaded programs. - Corneliu Popeea; Andrey Rybalchenko; Andreas Wilhelm (FMCAD, 2014)

A constraint-based approach to solving games on infinite graphs. - Tewodros A. Beyene; Swarat Chaudhuri; Corneliu Popeea; Andrey Rybalchenko (POPL, 2014)

CTL+FO verification as constraint solving. - Tewodros A. Beyene; Marc Brockschmidt; Andrey Rybalchenko (SPIN, 2014)

(Quantified) Horn Constraint Solving for Program Verification and Synthesis. - Andrey Rybalchenko (CoRR, 2014)

Generalised Interpolation by Solving Recursion-Free Horn Clauses - Ashutosh Gupta 001; Corneliu Popeea; Andrey Rybalchenko (HCVS, 2014)

Verification column. - Andrey Rybalchenko (ACM SIGLOG News, 2014)

Horn Clause Solvers for Program Verification. - Nikolaj S. Bjørner; Arie Gurfinkel; Kenneth L. McMillan; Andrey Rybalchenko (Fields of Logic and Computation II, 2015)

Symbolic Polytopes for Quantitative Interpolation and Verification. - Klaus von Gleissenthall; Boris Köpf; Andrey Rybalchenko (CAV (1), 2015)

Recursive Games for Compositional Program Synthesis. - Tewodros A. Beyene; Swarat Chaudhuri; Corneliu Popeea; Andrey Rybalchenko (VSTTE, 2015)

Cardinalities and universal quantifiers for verifying parameterized systems. - Klaus von Gleissenthall; Nikolaj S. Bjørner; Andrey Rybalchenko (PLDI, 2016)

Scaling network verification using symmetry and surgery. - Gordon D. Plotkin; Nikolaj S. Bjørner; Nuno P. Lopes; Andrey Rybalchenko; George Varghese (POPL, 2016)

Efficient CTL Verification via Horn Constraints Solving. - Tewodros A. Beyene; Corneliu Popeea; Andrey Rybalchenko (HCVS@ETAPS, 2016)

Preface: Special Issue on Interpolation. - Daniel Kroening; Andrey Rybalchenko (J. Autom. Reason., 2016)

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 (SOSP, 2017)

Predicate Abstraction for Program Verification. - Ranjit Jhala; Andreas Podelski; Andrey Rybalchenko (Handbook of Model Checking, 2018)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

Fast BGP Simulation of Large Datacenters. - Nuno P. Lopes; Andrey Rybalchenko (VMCAI, 2019)

Supercharging Plant Configurations Using Z3. - Nikolaj S. Bjørner; Maxwell Levatich; Nuno P. Lopes; Andrey Rybalchenko; Chandrasekar Vuppalapati (CPAIOR, 2021)