# Andrey Rybalchenko

According to our database

^{1}, Andrey Rybalchenko## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2017

CrystalNet: Faithfully Emulating Large Production Networks.

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

2016

Preface: Special Issue on Interpolation.

J. Autom. Reasoning, 2016

Efficient CTL Verification via Horn Constraints Solving.

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

Scaling network verification using symmetry and surgery.

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

Cardinalities and universal quantifiers for verifying parameterized systems.

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

2015

Recursive Games for Compositional Program Synthesis.

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

Symbolic Polytopes for Quantitative Interpolation and Verification.

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

Horn Clause Solvers for Program Verification.

Proceedings of the Fields of Logic and Computation II, 2015

2014

Verification column.

SIGLOG News, 2014

Generalised Interpolation by Solving Recursion-Free Horn Clauses

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

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

CoRR, 2014

CTL+FO Verification as Constraint Solving.

CoRR, 2014

CTL+FO verification as constraint solving.

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

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

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

Reduction for compositional verification of multi-threaded programs.

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

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

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

2013

From tests to proofs.

STTT, 2013

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).

Dagstuhl Reports, 2013

An Epistemic Perspective on Consistency of Concurrent Computations

CoRR, 2013

Separation Logic Modulo Theories

CoRR, 2013

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

CoRR, 2013

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

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

Automation of Quantitative Information-Flow Analysis.

Proceedings of the Formal Methods for Dynamical Systems, 2013

On Solving Universally Quantified Horn Clauses.

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

An Epistemic Perspective on Consistency of Concurrent Computations.

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

Solving Existentially Quantified Horn Clauses.

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

Separation Logic Modulo Theories.

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

2012

Compositional Termination Proofs for Multi-threaded Programs.

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).

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

Towards Automatic Synthesis of Software Verification Tools.

Proceedings of the Model Checking Software - 19th International Workshop, 2012

Binary Reachability Analysis of Higher Order Functional Programs.

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

Synthesizing software verifiers from proof rules.

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

Program Verification as Satisfiability Modulo Theories.

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

2011

Proving program termination.

Commun. ACM, 2011

Distributed and Predictable Software Model Checking.

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

Transition Invariants and Transition Predicate Abstraction for Program Termination.

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

Towards automatic synthesis of software verification tools.

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.

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

Separation logic + superposition calculus = heap theorem prover.

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

HMC: Verifying Functional Programs Using Abstract Interpreters.

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

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

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

Solving Recursion-Free Horn Clauses over LI+UIF.

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

2010

Applying Prolog to develop distributed systems.

TPLP, 2010

Constraint solving for interpolation.

J. Symb. Comput., 2010

Applying Prolog to Develop Distributed Systems

CoRR, 2010

Refinement type inference via abstract interpretation

CoRR, 2010

Thread-Modular Counterexample-Guided Abstraction Refinement.

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

Aligators for Arrays (Tool Paper).

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

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

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Approximation and Randomization for Quantitative Information-Flow Analysis.

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

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

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

Non-monotonic Refinement of Control Abstraction for Concurrent Programs.

Proceedings of the Automated Technology for Verification and Analysis, 2010

2009

Summarization for termination: no return!

Formal Methods in System Design, 2009

From Tests to Proofs.

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

Automated Methods for Proving Program Termination and Liveness.

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

Subsumer-First: Steering Symbolic Reachability Analysis.

Proceedings of the Model Checking Software, 2009

Automatic Discovery and Quantification of Information Leaks.

Proceedings of the 30th IEEE Symposium on Security and Privacy (S&P 2009), 2009

Verifying liveness for asynchronous programs.

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

Operational Semantics for Declarative Networking.

Proceedings of the Practical Aspects of Declarative Languages, 2009

Finding heap-bounds for hardware synthesis.

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

Cardinality Abstraction for Declarative Networking Applications.

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

InvGen: An Efficient Invariant Generator.

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

2008

Model checking Duration Calculus: a practical approach.

Formal Asp. Comput., 2008

Proving non-termination.

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

Heap Assumptions on Demand.

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

Proving Conditional Termination.

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

2007

Transition predicate abstraction and fair termination.

ACM Trans. Program. Lang. Syst., 2007

Constraint Solving for Interpolation.

Proceedings of the Verification, 2007

Invariant Synthesis for Combined Theories.

Proceedings of the Verification, 2007

Precise Thread-Modular Verification.

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

Proving that programs eventually do something good.

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

Proving thread termination.

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

Path invariants.

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.

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

2006

Termination proofs for systems code.

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

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL.

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

Model Checking Duration Calculus: A Practical Approach.

Proceedings of the Theoretical Aspects of Computing, 2006

Thread-Modular Verification Is Cartesian Abstract Interpretation.

Proceedings of the Theoretical Aspects of Computing, 2006

Terminator: Beyond Safety.

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

2005

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

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

Abstraction Refinement for Termination.

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

Transition predicate abstraction and fair termination.

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Temporale Verifikation mit Transitionsinvarianten.

Proceedings of the Ausgezeichnete Informatikdissertationen 2005, 2005

Temporal verification with transition invariants.

PhD thesis, 2005

2004

A Complete Method for the Synthesis of Linear Ranking Functions.

Proceedings of the Verification, 2004

Transition Invariants.

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