default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndrey Rybalchenko
Person information
- affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2021
[c70]Nikolaj S. Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati:
Supercharging Plant Configurations Using Z3. CPAIOR 2021: 1-25
2010 – 2019
- 2019
- [c69]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: 116-132 - [c68]Nuno P. Lopes, Andrey Rybalchenko:
Fast BGP Simulation of Large Datacenters. VMCAI 2019: 386-408 - 2018
- [p2]Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko:
Predicate Abstraction for Program Verification. Handbook of Model Checking 2018: 447-491 - 2017
- [c67]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: 599-613 - 2016
- [j9]Daniel Kroening, Andrey Rybalchenko:
Preface: Special Issue on Interpolation. J. Autom. Reason. 57(1): 1-2 (2016) - [c66]Klaus von Gleissenthall, Nikolaj S. Bjørner, Andrey Rybalchenko:
Cardinalities and universal quantifiers for verifying parameterized systems. PLDI 2016: 599-613 - [c65]Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese:
Scaling network verification using symmetry and surgery. POPL 2016: 69-83 - [c64]Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko:
Efficient CTL Verification via Horn Constraints Solving. HCVS@ETAPS 2016: 1-14 - 2015
- [c63]Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c62]Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko:
Symbolic Polytopes for Quantitative Interpolation and Verification. CAV (1) 2015: 178-194 - [c61]Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko:
Recursive Games for Compositional Program Synthesis. VSTTE 2015: 19-39 - 2014
- [j8]Andrey Rybalchenko:
Verification column. ACM SIGLOG News 1(1): 9 (2014) - [c60]Klaus von Gleissenthall, Andrey Rybalchenko, Santiago Zanella Béguelin:
Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk). VPT@CAV 2014: 2 - [c59]Corneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm:
Reduction for compositional verification of multi-threaded programs. FMCAD 2014: 187-194 - [c58]Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko:
A constraint-based approach to solving games on infinite graphs. POPL 2014: 221-234 - [c57]Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko:
CTL+FO verification as constraint solving. SPIN 2014: 101-104 - [c56]Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
Generalised Interpolation by Solving Recursion-Free Horn Clauses. HCVS 2014: 31-38 - [e4]Ernie Cohen, Andrey Rybalchenko:
Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers. Lecture Notes in Computer Science 8164, Springer 2014, ISBN 978-3-642-54107-0 [contents] - [e3]Nikolaj S. Bjørner, Fabio Fioravanti, Andrey Rybalchenko, Valerio Senni:
Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. EPTCS 169, 2014 [contents] - [i8]Andrey Rybalchenko:
(Quantified) Horn Constraint Solving for Program Verification and Synthesis. CoRR abs/1405.7739 (2014) - [i7]Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko:
CTL+FO Verification as Constraint Solving. CoRR abs/1406.3988 (2014) - 2013
- [j7]Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko:
From tests to proofs. Int. J. Softw. Tools Technol. Transf. 15(4): 291-303 (2013) - [c55]Juan Antonio Navarro Pérez, Andrey Rybalchenko:
Separation Logic Modulo Theories. APLAS 2013: 90-106 - [c54]Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko:
Solving Existentially Quantified Horn Clauses. CAV 2013: 869-882 - [c53]Klaus von Gleissenthall, Andrey Rybalchenko:
An Epistemic Perspective on Consistency of Concurrent Computations. CONCUR 2013: 212-226 - [c52]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
On Solving Universally Quantified Horn Clauses. SAS 2013: 105-125 - [c51]Boris Köpf, Andrey Rybalchenko:
Automation of Quantitative Information-Flow Analysis. SFM 2013: 1-28 - [c50]Corneliu Popeea, Andrey Rybalchenko:
Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). TACAS 2013: 633-636 - [i6]Juan Antonio Navarro Pérez, Andrey Rybalchenko:
Separation Logic Modulo Theories. CoRR abs/1303.2489 (2013) - [i5]Klaus von Gleissenthall, Andrey Rybalchenko:
An Epistemic Perspective on Consistency of Concurrent Computations. CoRR abs/1305.2295 (2013) - [i4]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR abs/1306.5264 (2013) - [i3]Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder:
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). Dagstuhl Reports 3(4): 1-16 (2013) - 2012
- [c49]Nikolaj S. Bjørner, Kenneth L. McMillan, Andrey Rybalchenko:
Program Verification as Satisfiability Modulo Theories. SMT@IJCAR 2012: 3-11 - [c48]Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko:
Synthesizing software verifiers from proof rules. PLDI 2012: 405-416 - [c47]Ruslán Ledesma-Garza, Andrey Rybalchenko:
Binary Reachability Analysis of Higher Order Functional Programs. SAS 2012: 388-404 - [c46]Andrey Rybalchenko:
Towards Automatic Synthesis of Software Verification Tools. SPIN 2012: 22 - [c45]Corneliu Popeea, Andrey Rybalchenko:
Compositional Termination Proofs for Multi-threaded Programs. TACAS 2012: 237-251 - [c44]Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko:
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). TACAS 2012: 549-551 - [e2]Viktor Kuncak, Andrey Rybalchenko:
Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Lecture Notes in Computer Science 7148, Springer 2012, ISBN 978-3-642-27939-3 [contents] - 2011
- [j6]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Proving program termination. Commun. ACM 54(5): 88-98 (2011) - [c43]Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
Solving Recursion-Free Horn Clauses over LI+UIF. APLAS 2011: 188-203 - [c42]Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
Threader: A Constraint-Based Verifier for Multi-threaded Programs. CAV 2011: 412-417 - [c41]Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko:
HMC: Verifying Functional Programs Using Abstract Interpreters. CAV 2011: 470-485 - [c40]Juan Antonio Navarro Pérez, Andrey Rybalchenko:
Separation logic + superposition calculus = heap theorem prover. PLDI 2011: 556-566 - [c39]Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
Predicate abstraction and refinement for verifying multi-threaded programs. POPL 2011: 331-344 - [c38]Andrey Rybalchenko:
Towards automatic synthesis of software verification tools. PPDP 2011: 3-4 - [c37]Andreas Podelski, Andrey Rybalchenko:
Transition Invariants and Transition Predicate Abstraction for Program Termination. TACAS 2011: 3-10 - [c36]Nuno P. Lopes, Andrey Rybalchenko:
Distributed and Predictable Software Model Checking. VMCAI 2011: 340-355 - 2010
- [j5]Andrey Rybalchenko, Viorica Sofronie-Stokkermans:
Constraint solving for interpolation. J. Symb. Comput. 45(11): 1212-1233 (2010) - [j4]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): 691-707 (2010) - [c35]Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko:
Non-monotonic Refinement of Control Abstraction for Concurrent Programs. ATVA 2010: 188-202 - [c34]Andrey Rybalchenko:
Constraint Solving for Program Verification: Theory and Practice by Example. CAV 2010: 57-71 - [c33]Boris Köpf, Andrey Rybalchenko:
Approximation and Randomization for Quantitative Information-Flow Analysis. CSF 2010: 3-14 - [c32]Andrey Rybalchenko:
Constraint Solving for Program Verification: Theory and Practice by Example. CSL 2010: 51 - [c31]Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko:
Aligators for Arrays (Tool Paper). LPAR (Yogyakarta) 2010: 348-356 - [c30]Alexander Malkis, Andreas Podelski, Andrey Rybalchenko:
Thread-Modular Counterexample-Guided Abstraction Refinement. SAS 2010: 356-372 - [i2]Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko:
Refinement type inference via abstract interpretation. CoRR abs/1004.2884 (2010) - [i1]Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh:
Applying Prolog to Develop Distributed Systems. CoRR abs/1007.3835 (2010)
2000 – 2009
- 2009
- [j3]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Summarization for termination: no return! Formal Methods Syst. Des. 35(3): 369-387 (2009) - [c29]Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh:
Cardinality Abstraction for Declarative Networking Applications. CAV 2009: 584-598 - [c28]Ashutosh Gupta, Andrey Rybalchenko:
InvGen: An Efficient Invariant Generator. CAV 2009: 634-640 - [c27]Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis:
Finding heap-bounds for hardware synthesis. FMCAD 2009: 205-212 - [c26]Juan Antonio Navarro Pérez, Andrey Rybalchenko:
Operational Semantics for Declarative Networking. PADL 2009: 76-90 - [c25]Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko:
Verifying liveness for asynchronous programs. POPL 2009: 102-113 - [c24]Michael Backes, Boris Köpf, Andrey Rybalchenko:
Automatic Discovery and Quantification of Information Leaks. SP 2009: 141-153 - [c23]Andrey Rybalchenko, Rishabh Singh:
Subsumer-First: Steering Symbolic Reachability Analysis. SPIN 2009: 192-204 - [c22]Andrey Rybalchenko:
Automated Methods for Proving Program Termination and Liveness. SYNASC 2009: 17 - [c21]Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko:
From Tests to Proofs. TACAS 2009: 262-276 - [e1]Anna E. Frid, Andrey Morozov, Andrey Rybalchenko, Klaus W. Wagner:
Computer Science - Theory and Applications, Fourth International Computer Science Symposium in Russia, CSR 2009, Novosibirsk, Russia, August 18-23, 2009. Proceedings. Lecture Notes in Computer Science 5675, Springer 2009, ISBN 978-3-642-03350-6 [contents] - 2008
- [j2]Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko:
Model checking Duration Calculus: a practical approach. Formal Aspects Comput. 20(4-5): 481-505 (2008) - [c20]Andreas Podelski, Andrey Rybalchenko, Thomas Wies:
Heap Assumptions on Demand. CAV 2008: 314-327 - [c19]Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
Proving Conditional Termination. CAV 2008: 328-340 - [c18]Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu:
Proving non-termination. POPL 2008: 147-158 - 2007
- [j1]Andreas Podelski, Andrey Rybalchenko:
Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3): 15 (2007) - [c17]Andreas Podelski, Andrey Rybalchenko:
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. PADL 2007: 245-259 - [c16]Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko:
Path invariants. PLDI 2007: 300-309 - [c15]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Proving thread termination. PLDI 2007: 320-330 - [c14]Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi:
Proving that programs eventually do something good. POPL 2007: 265-276 - [c13]Alexander Malkis, Andreas Podelski, Andrey Rybalchenko:
Precise Thread-Modular Verification. SAS 2007: 218-232 - [c12]Andrey Rybalchenko, Viorica Sofronie-Stokkermans:
Constraint Solving for Interpolation. VMCAI 2007: 346-362 - [c11]Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko:
Invariant Synthesis for Combined Theories. VMCAI 2007: 378-394 - 2006
- [c10]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Terminator: Beyond Safety. CAV 2006: 415-418 - [c9]Alexander Malkis, Andreas Podelski, Andrey Rybalchenko:
Thread-Modular Verification Is Cartesian Abstract Interpretation. ICTAC 2006: 183-197 - [c8]Roland Meyer, Johannes Faber, Andrey Rybalchenko:
Model Checking Duration Calculus: A Practical Approach. ICTAC 2006: 332-346 - [c7]Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski:
Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. MoChArt 2006: 51-66 - [c6]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Termination proofs for systems code. PLDI 2006: 415-426 - 2005
- [b1]Andrey Rybalchenko:
Temporal verification with transition invariants. Saarland University, Saarbrücken, Germany, 2005, pp. I-XII, 1-89 - [c5]Andreas Podelski, Andrey Rybalchenko:
Transition predicate abstraction and fair termination. POPL 2005: 132-144 - [c4]Byron Cook, Andreas Podelski, Andrey Rybalchenko:
Abstraction Refinement for Termination. SAS 2005: 87-101 - [c3]Amir Pnueli, Andreas Podelski, Andrey Rybalchenko:
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS 2005: 124-139 - [p1]Andrey Rybalchenko:
Temporale Verifikation mit Transitionsinvarianten. Ausgezeichnete Informatikdissertationen 2005: 141-150 - 2004
- [c2]Andreas Podelski, Andrey Rybalchenko:
Transition Invariants. LICS 2004: 32-41 - [c1]Andreas Podelski, Andrey Rybalchenko:
A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004: 239-251
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
