Andrey Rybalchenko

According to our database, Andrey Rybalchenko authored at least 81 papers between 2004 and 2021.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2021

Supercharging Plant Configurations Using Z3.

Nikolaj S. Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati

Proceedings of the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, 2021

2019

Fast BGP Simulation of Large Datacenters.

Nuno P. Lopes, Andrey Rybalchenko

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

SL-COMP: Competition of Solvers for Separation Logic.

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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018

Predicate Abstraction for Program Verification.

Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Handbook of Model Checking., 2018

2017

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

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

2016

Preface: Special Issue on Interpolation.

Daniel Kroening, Andrey Rybalchenko

J. Autom. Reason., 2016

Efficient CTL Verification via Horn Constraints Solving.

Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, 2016

Scaling network verification using symmetry and surgery.

Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Cardinalities and universal quantifiers for verifying parameterized systems.

Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

2015

Recursive Games for Compositional Program Synthesis.

Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Symbolic Polytopes for Quantitative Interpolation and Verification.

Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Horn Clause Solvers for Program Verification.

Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko

Proceedings of the Fields of Logic and Computation II, 2015

2014

Verification column.

Andrey Rybalchenko

ACM SIGLOG News, 2014

Generalised Interpolation by Solving Recursion-Free Horn Clauses

Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014

(Quantified) Horn Constraint Solving for Program Verification and Synthesis.

Andrey Rybalchenko

CoRR, 2014

CTL+FO verification as constraint solving.

Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko

Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

A constraint-based approach to solving games on infinite graphs.

Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Reduction for compositional verification of multi-threaded programs.

Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk).

Klaus von Gleissenthall, Andrey Rybalchenko, Santiago Zanella Béguelin

Proceedings of the VPT 2014. Second International Workshop on Verification and Program Transformation, 2014

2013

From tests to proofs.

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko

Int. J. Softw. Tools Technol. Transf., 2013

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).

Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder

Dagstuhl Reports, 2013

Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types.

Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko

CoRR, 2013

Threader: A Verifier for Multi-threaded Programs - (Competition Contribution).

Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Automation of Quantitative Information-Flow Analysis.

Boris Köpf, Andrey Rybalchenko

Proceedings of the Formal Methods for Dynamical Systems, 2013

On Solving Universally Quantified Horn Clauses.

Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko

Proceedings of the Static Analysis - 20th International Symposium, 2013

An Epistemic Perspective on Consistency of Concurrent Computations.

Klaus von Gleissenthall, Andrey Rybalchenko

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Solving Existentially Quantified Horn Clauses.

Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Separation Logic Modulo Theories.

Juan Antonio Navarro Pérez, Andrey Rybalchenko

Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012

Compositional Termination Proofs for Multi-threaded Programs.

Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution).

Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Binary Reachability Analysis of Higher Order Functional Programs.

Ruslán Ledesma-Garza, Andrey Rybalchenko

Proceedings of the Static Analysis - 19th International Symposium, 2012

Synthesizing software verifiers from proof rules.

Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Program Verification as Satisfiability Modulo Theories.

Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

Proving program termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Commun. ACM, 2011

Distributed and Predictable Software Model Checking.

Nuno P. Lopes, Andrey Rybalchenko

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Transition Invariants and Transition Predicate Abstraction for Program Termination.

Andreas Podelski, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Towards automatic synthesis of software verification tools.

Andrey Rybalchenko

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Predicate abstraction and refinement for verifying multi-threaded programs.

Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Separation logic + superposition calculus = heap theorem prover.

Juan Antonio Navarro Pérez, Andrey Rybalchenko

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

HMC: Verifying Functional Programs Using Abstract Interpreters.

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Threader: A Constraint-Based Verifier for Multi-threaded Programs.

Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Solving Recursion-Free Horn Clauses over LI+UIF.

Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

Applying Prolog to develop distributed systems.

Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh

Theory Pract. Log. Program., 2010

Constraint solving for interpolation.

Andrey Rybalchenko, Viorica Sofronie-Stokkermans

J. Symb. Comput., 2010

Refinement type inference via abstract interpretation

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko

CoRR, 2010

Thread-Modular Counterexample-Guided Abstraction Refinement.

Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Static Analysis - 17th International Symposium, 2010

Aligators for Arrays (Tool Paper).

Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Approximation and Randomization for Quantitative Information-Flow Analysis.

Boris Köpf, Andrey Rybalchenko

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Constraint Solving for Program Verification: Theory and Practice by Example.

Andrey Rybalchenko

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Non-monotonic Refinement of Control Abstraction for Concurrent Programs.

Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko

Proceedings of the Automated Technology for Verification and Analysis, 2010

2009

Summarization for termination: no return!

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Formal Methods Syst. Des., 2009

Automated Methods for Proving Program Termination and Liveness.

Andrey Rybalchenko

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Subsumer-First: Steering Symbolic Reachability Analysis.

Andrey Rybalchenko, Rishabh Singh

Proceedings of the Model Checking Software, 2009

Automatic Discovery and Quantification of Information Leaks.

Michael Backes, Boris Köpf, Andrey Rybalchenko

Proceedings of the 30th IEEE Symposium on Security and Privacy (SP 2009), 2009

Verifying liveness for asynchronous programs.

Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Operational Semantics for Declarative Networking.

Juan Antonio Navarro Pérez, Andrey Rybalchenko

Proceedings of the Practical Aspects of Declarative Languages, 2009

Finding heap-bounds for hardware synthesis.

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Cardinality Abstraction for Declarative Networking Applications.

Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

InvGen: An Efficient Invariant Generator.

Ashutosh Gupta, Andrey Rybalchenko

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Model checking Duration Calculus: a practical approach.

Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko

Formal Aspects Comput., 2008

Proving non-termination.

Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Heap Assumptions on Demand.

Andreas Podelski, Andrey Rybalchenko, Thomas Wies

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Proving Conditional Termination.

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Transition predicate abstraction and fair termination.

Andreas Podelski, Andrey Rybalchenko

ACM Trans. Program. Lang. Syst., 2007

Invariant Synthesis for Combined Theories.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko

Proceedings of the Verification, 2007

Precise Thread-Modular Verification.

Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Static Analysis, 14th International Symposium, 2007

Proving that programs eventually do something good.

Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Proving thread termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Path invariants.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement.

Andreas Podelski, Andrey Rybalchenko

Proceedings of the Practical Aspects of Declarative Languages, 9th International Symposium, 2007

2006

Termination proofs for systems code.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 2006

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL.

Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski

Proceedings of the Model Checking and Artificial Intelligence, 4th Workshop, 2006

Model Checking Duration Calculus: A Practical Approach.

Roland Meyer, Johannes Faber, Andrey Rybalchenko

Proceedings of the Theoretical Aspects of Computing, 2006

Thread-Modular Verification Is Cartesian Abstract Interpretation.

Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Theoretical Aspects of Computing, 2006

Terminator: Beyond Safety.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.

Amir Pnueli, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Abstraction Refinement for Termination.

Byron Cook, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Static Analysis, 12th International Symposium, 2005

Temporale Verifikation mit Transitionsinvarianten.

Andrey Rybalchenko

Proceedings of the Ausgezeichnete Informatikdissertationen 2005, 2005

Temporal verification with transition invariants.

Andrey Rybalchenko

PhD thesis, 2005

2004

A Complete Method for the Synthesis of Linear Ranking Functions.

Andreas Podelski, Andrey Rybalchenko

Proceedings of the Verification, 2004

Transition Invariants.

Andreas Podelski, Andrey Rybalchenko

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004