Andrey Rybalchenko

Publication Activity (10 Years)

Years Active: 2004-2021
Publications (10 Years): 8

Top Venues

CoRR

TACAS

SPIN

PLDI

Saarland University, Saarbrücken, Germany (PHD)

Education History

Saarland University, Saarbrücken, Germany

PHD

Publications

Nikolaj Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati
Supercharging Plant Configurations Using Z3. CPAIOR (2021)
Mihaela Sighireanu, Juan Antonio Navarro Pérez, 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, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu
SL-COMP: Competition of Solvers for Separation Logic. TACAS (3) (2019)
Nuno P. Lopes, Andrey Rybalchenko
Fast BGP Simulation of Large Datacenters. VMCAI (2019)
Hongqiang Harry Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno P. Lopes, Andrey Rybalchenko, Guohan Lu, Lihua Yuan
CrystalNet: Faithfully Emulating Large Production Networks. SOSP (2017)
Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese
Scaling network verification using symmetry and surgery. POPL (2016)
Daniel Kroening, Andrey Rybalchenko
Preface: Special Issue on Interpolation. J. Autom. Reason. 57 (1) (2016)
Klaus von Gleissenthall, Nikolaj Bjørner, Andrey Rybalchenko
Cardinalities and universal quantifiers for verifying parameterized systems. PLDI (2016)
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
Efficient CTL Verification via Horn Constraints Solving. HCVS@ETAPS (2016)
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
Recursive Games for Compositional Program Synthesis. VSTTE (2015)
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II (2015)
Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko
Symbolic Polytopes for Quantitative Interpolation and Verification. CAV (1) (2015)
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
CTL+FO Verification as Constraint Solving. CoRR (2014)
Andrey Rybalchenko
(Quantified) Horn Constraint Solving for Program Verification and Synthesis. CoRR (2014)
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Generalised Interpolation by Solving Recursion-Free Horn Clauses HCVS (2014)
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
CTL+FO verification as constraint solving. SPIN (2014)
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
A constraint-based approach to solving games on infinite graphs. POPL (2014)
Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm
Reduction for compositional verification of multi-threaded programs. FMCAD (2014)
Andrey Rybalchenko
Verification column. ACM SIGLOG News 1 (1) (2014)
Klaus von Gleissenthall, Andrey Rybalchenko, Santiago Zanella Béguelin
Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk). VPT@CAV (2014)
Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko
From tests to proofs. Int. J. Softw. Tools Technol. Transf. 15 (4) (2013)
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Separation Logic Modulo Theories CoRR (2013)
Corneliu Popeea, Andrey Rybalchenko
Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). TACAS (2013)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR (2013)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
On Solving Universally Quantified Horn Clauses. SAS (2013)
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Separation Logic Modulo Theories. APLAS (2013)
Klaus von Gleissenthall, Andrey Rybalchenko
An Epistemic Perspective on Consistency of Concurrent Computations. CONCUR (2013)
Boris Köpf, Andrey Rybalchenko
Automation of Quantitative Information-Flow Analysis. SFM (2013)
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). Dagstuhl Reports 3 (4) (2013)
Klaus von Gleissenthall, Andrey Rybalchenko
An Epistemic Perspective on Consistency of Concurrent Computations CoRR (2013)
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
Solving Existentially Quantified Horn Clauses. CAV (2013)
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). TACAS (2012)
Ruslán Ledesma-Garza, Andrey Rybalchenko
Binary Reachability Analysis of Higher Order Functional Programs. SAS (2012)
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko
Synthesizing software verifiers from proof rules. PLDI (2012)
Corneliu Popeea, Andrey Rybalchenko
Compositional Termination Proofs for Multi-threaded Programs. TACAS (2012)
Nikolaj Bjørner, Kenneth L. McMillan, Andrey Rybalchenko
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR (2012)
Andrey Rybalchenko
Towards Automatic Synthesis of Software Verification Tools. SPIN (2012)
Nuno P. Lopes, Andrey Rybalchenko
Distributed and Predictable Software Model Checking. VMCAI (2011)
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Threader: A Constraint-Based Verifier for Multi-threaded Programs. CAV (2011)
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Predicate abstraction and refinement for verifying multi-threaded programs. POPL (2011)
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Separation logic + superposition calculus = heap theorem prover. PLDI (2011)
Andreas Podelski, Andrey Rybalchenko
Transition Invariants and Transition Predicate Abstraction for Program Termination. TACAS (2011)
Andrey Rybalchenko
Towards automatic synthesis of software verification tools. PPDP (2011)
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
HMC: Verifying Functional Programs Using Abstract Interpreters. CAV (2011)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Proving program termination. Commun. ACM 54 (5) (2011)
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Solving Recursion-Free Horn Clauses over LI+UIF. APLAS (2011)
Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh
Applying Prolog to develop distributed systems. Theory Pract. Log. Program. 10 (4-6) (2010)
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Non-monotonic Refinement of Control Abstraction for Concurrent Programs. ATVA (2010)
Andrey Rybalchenko
Constraint Solving for Program Verification: Theory and Practice by Example. CSL (2010)
Alexander Malkis, Andreas Podelski, Andrey Rybalchenko
Thread-Modular Counterexample-Guided Abstraction Refinement. SAS (2010)
Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh
Applying Prolog to Develop Distributed Systems CoRR (2010)
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
Refinement type inference via abstract interpretation CoRR (2010)
Boris Köpf, Andrey Rybalchenko
Approximation and Randomization for Quantitative Information-Flow Analysis. CSF (2010)
Andrey Rybalchenko
Constraint Solving for Program Verification: Theory and Practice by Example. CAV (2010)
Andrey Rybalchenko, Viorica Sofronie-Stokkermans
Constraint solving for interpolation. J. Symb. Comput. 45 (11) (2010)
Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko
Aligators for Arrays (Tool Paper). LPAR (Yogyakarta) (2010)
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Operational Semantics for Declarative Networking. PADL (2009)
Andrey Rybalchenko
Automated Methods for Proving Program Termination and Liveness. SYNASC (2009)
Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh
Cardinality Abstraction for Declarative Networking Applications. CAV (2009)
Andrey Rybalchenko, Rishabh Singh
Subsumer-First: Steering Symbolic Reachability Analysis. SPIN (2009)
Ashutosh Gupta, Andrey Rybalchenko
InvGen: An Efficient Invariant Generator. CAV (2009)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Summarization for termination: no return! Formal Methods Syst. Des. 35 (3) (2009)
Michael Backes, Boris Köpf, Andrey Rybalchenko
Automatic Discovery and Quantification of Information Leaks. IEEE Symposium on Security and Privacy (2009)
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis
Finding heap-bounds for hardware synthesis. FMCAD (2009)
Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko
Verifying liveness for asynchronous programs. POPL (2009)
Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko
From Tests to Proofs. TACAS (2009)
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv
Proving Conditional Termination. CAV (2008)
Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko
Model checking Duration Calculus: a practical approach. Formal Aspects Comput. 20 (4-5) (2008)
Andreas Podelski, Andrey Rybalchenko, Thomas Wies
Heap Assumptions on Demand. CAV (2008)
Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu
Proving non-termination. POPL (2008)
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi
Proving that programs eventually do something good. POPL (2007)
Andrey Rybalchenko, Viorica Sofronie-Stokkermans
Constraint Solving for Interpolation. VMCAI (2007)
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko
Invariant Synthesis for Combined Theories. VMCAI (2007)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Proving thread termination. PLDI (2007)
Andreas Podelski, Andrey Rybalchenko
Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29 (3) (2007)
Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko
Path invariants. PLDI (2007)
Alexander Malkis, Andreas Podelski, Andrey Rybalchenko
Precise Thread-Modular Verification. SAS (2007)
Andreas Podelski, Andrey Rybalchenko
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. PADL (2007)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Terminator: Beyond Safety. CAV (2006)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Termination proofs for systems code. PLDI (2006)
Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski
Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. MoChArt (2006)
Alexander Malkis, Andreas Podelski, Andrey Rybalchenko
Thread-Modular Verification Is Cartesian Abstract Interpretation. ICTAC (2006)
Roland Meyer, Johannes Faber, Andrey Rybalchenko
Model Checking Duration Calculus: A Practical Approach. ICTAC (2006)
Amir Pnueli, Andreas Podelski, Andrey Rybalchenko
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS (2005)
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Abstraction Refinement for Termination. SAS (2005)
Andrey Rybalchenko
Temporale Verifikation mit Transitionsinvarianten. Ausgezeichnete Informatikdissertationen (2005)
Andreas Podelski, Andrey Rybalchenko
Transition predicate abstraction and fair termination. POPL (2005)
Andreas Podelski, Andrey Rybalchenko
A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI (2004)
Andreas Podelski, Andrey Rybalchenko
Transition Invariants. LICS (2004)

Andrey Rybalchenko.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Andrey Rybalchenko