Fast BGP Simulation of Large Datacenters
Nuno Lopes, Andrey Rybalchenko
VMCAI: Verification, Model Checking, and Abstract Interpretation | January 2019
Andrey Rybalchenko
Senior Principal Researcher
Publications
Publications by Year
-
-
CrystalNet: Faithfully Emulating Large Production Networks
Hongqiang Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno Lopes, Andrey Rybalchenko, Guohan Lu, Lihua Yuan
SOSP '17 Proceedings of the 26th Symposium on Operating Systems Principles | October 2017
ISBN: 978-1-4503-5085-3
-
Automatically verifying reachability and well-formedness in P4 Networks
Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
MSR-TR-2016-65 | September 2016
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
-
Symbolic Polytopes for Quantitative Interpolation and Verification
Klaus v. Gleissenthall, Boris Kopf, Andrey Rybalchenko
Computer Aided Verification (CAV) | July 2015
-
Reduction for Compositional Verification of Multi-Threaded Programs
Corneliu Popeea, Andreas Wilhelm, Andrey Rybalchenko
Formal Methods in Computer-Aided Design (FMCAD) | October 2014
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
Symposium on Model Checking of Software (SPIN) | July 2014
TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures
Marc Brockschmidt, Andrey Rybalchenko
June 2014
A Constraint-Based Approach to Solving Games on Infinite Graphs
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
Principles of Programming Languages (POPL) | January 2014
-
Separation Logic Modulo Theories
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Programming Languages and Systems (APLAS) | December 2013
An Epistemic Perspective on Consistency of Concurrent Computations
Klaus v. Gleissenthall, Andrey Rybalchenko
Concurrency Theory (CONCUR) | August 2013
Solving Existentially Quantified Horn Clauses
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
Computer Aided Verification (CAV) | Published by Springer | 2013
On Solving Universally Quantified Horn Clauses
Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
Static Analysis Symposium (SAS) | June 2013
Computing Relational Fixed Points using Interpolation
Kenneth McMillan, Andrey Rybalchenko
MSR-TR-2013-6 | January 2013
Publications by Research Area
-
Fast BGP Simulation of Large Datacenters
Nuno Lopes, Andrey Rybalchenko
VMCAI: Verification, Model Checking, and Abstract Interpretation | January 2019
Automatically verifying reachability and well-formedness in P4 Networks
Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
MSR-TR-2016-65 | September 2016
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
Symbolic Polytopes for Quantitative Interpolation and Verification
Klaus v. Gleissenthall, Boris Kopf, Andrey Rybalchenko
Computer Aided Verification (CAV) | July 2015
Reduction for Compositional Verification of Multi-Threaded Programs
Corneliu Popeea, Andreas Wilhelm, Andrey Rybalchenko
Formal Methods in Computer-Aided Design (FMCAD) | October 2014
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
Symposium on Model Checking of Software (SPIN) | July 2014
TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures
Marc Brockschmidt, Andrey Rybalchenko
June 2014
A Constraint-Based Approach to Solving Games on Infinite Graphs
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
Principles of Programming Languages (POPL) | January 2014
Separation Logic Modulo Theories
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Programming Languages and Systems (APLAS) | December 2013
An Epistemic Perspective on Consistency of Concurrent Computations
Klaus v. Gleissenthall, Andrey Rybalchenko
Concurrency Theory (CONCUR) | August 2013
Solving Existentially Quantified Horn Clauses
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
Computer Aided Verification (CAV) | Published by Springer | 2013
On Solving Universally Quantified Horn Clauses
Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
Static Analysis Symposium (SAS) | June 2013
Computing Relational Fixed Points using Interpolation
Kenneth McMillan, Andrey Rybalchenko
MSR-TR-2013-6 | January 2013
-
Fast BGP Simulation of Large Datacenters
Nuno Lopes, Andrey Rybalchenko
VMCAI: Verification, Model Checking, and Abstract Interpretation | January 2019
CrystalNet: Faithfully Emulating Large Production Networks
Hongqiang Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno Lopes, Andrey Rybalchenko, Guohan Lu, Lihua Yuan
SOSP '17 Proceedings of the 26th Symposium on Operating Systems Principles | October 2017
ISBN: 978-1-4503-5085-3
Automatically verifying reachability and well-formedness in P4 Networks
Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
MSR-TR-2016-65 | September 2016
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
-
Computing Relational Fixed Points using Interpolation
Kenneth McMillan, Andrey Rybalchenko
MSR-TR-2013-6 | January 2013
Publications by Type
-
Fast BGP Simulation of Large Datacenters
Nuno Lopes, Andrey Rybalchenko
VMCAI: Verification, Model Checking, and Abstract Interpretation | January 2019
CrystalNet: Faithfully Emulating Large Production Networks
Hongqiang Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno Lopes, Andrey Rybalchenko, Guohan Lu, Lihua Yuan
SOSP '17 Proceedings of the 26th Symposium on Operating Systems Principles | October 2017
ISBN: 978-1-4503-5085-3
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno Lopes, Andrey Rybalchenko, George Varghese
POPL | June 2016
Cardinalities and Universal Quantifers for Verifying Parameterized Systems
Klaus v. Gleissenthall , Nikolaj Bjørner, Andrey Rybalchenko
PLDI | June 2016
Symbolic Polytopes for Quantitative Interpolation and Verification
Klaus v. Gleissenthall, Boris Kopf, Andrey Rybalchenko
Computer Aided Verification (CAV) | July 2015
Reduction for Compositional Verification of Multi-Threaded Programs
Corneliu Popeea, Andreas Wilhelm, Andrey Rybalchenko
Formal Methods in Computer-Aided Design (FMCAD) | October 2014
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
Symposium on Model Checking of Software (SPIN) | July 2014
TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures
Marc Brockschmidt, Andrey Rybalchenko
June 2014
A Constraint-Based Approach to Solving Games on Infinite Graphs
Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
Principles of Programming Languages (POPL) | January 2014
Separation Logic Modulo Theories
Juan Antonio Navarro Pérez, Andrey Rybalchenko
Programming Languages and Systems (APLAS) | December 2013
An Epistemic Perspective on Consistency of Concurrent Computations
Klaus v. Gleissenthall, Andrey Rybalchenko
Concurrency Theory (CONCUR) | August 2013
On Solving Universally Quantified Horn Clauses
Nikolaj Bjørner, Kenneth McMillan, Andrey Rybalchenko
Static Analysis Symposium (SAS) | June 2013
-
Automatically verifying reachability and well-formedness in P4 Networks
Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjørner, Andrey Rybalchenko
MSR-TR-2016-65 | September 2016
Computing Relational Fixed Points using Interpolation
Kenneth McMillan, Andrey Rybalchenko
MSR-TR-2013-6 | January 2013
-
Solving Existentially Quantified Horn Clauses
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
Computer Aided Verification (CAV) | Published by Springer | 2013