Andrey Rybalchenko

95 papers A* 25A 7B 19C 5Misc 2Journal 17Unranked 14

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