Andrey Rybalchenko
According to our database^{1},
Andrey Rybalchenko
authored at least 87 papers
between 2004 and 2018.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at twitter.com
On csauthors.net:
Bibliography
2018
Predicate Abstraction for Program Verification.
Proceedings of the Handbook of Model Checking., 2018
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 SIGPLANSIGACT 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 RecursionFree 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 constraintbased approach to solving games on infinite graphs.
Proceedings of the 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 2014
Reduction for compositional verification of multithreaded programs.
Proceedings of the Formal Methods in ComputerAided 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
Higherorder Program Verification as Satisfiability Modulo Theories with Algebraic Datatypes.
CoRR, 2013
Threader: A Verifier for Multithreaded Programs  (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013
Automation of Quantitative InformationFlow 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 Multithreaded 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 multithreaded programs.
Proceedings of the 38th ACM SIGPLANSIGACT 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 ConstraintBased Verifier for Multithreaded Programs.
Proceedings of the Computer Aided Verification  23rd International Conference, 2011
Solving RecursionFree 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
ThreadModular CounterexampleGuided 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 InformationFlow 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
Nonmonotonic 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
SubsumerFirst: 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 SIGPLANSIGACT Symposium on Principles of Programming Languages, 2009
Operational Semantics for Declarative Networking.
Proceedings of the Practical Aspects of Declarative Languages, 2009
Finding heapbounds for hardware synthesis.
Proceedings of 9th International Conference on Formal Methods in ComputerAided 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 nontermination.
Proceedings of the 35th ACM SIGPLANSIGACT 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 ThreadModular Verification.
Proceedings of the Static Analysis, 14th International Symposium, 2007
Proving that programs eventually do something good.
Proceedings of the 34th ACM SIGPLANSIGACT 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
ThreadModular 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 WellFoundedness 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 SIGPLANSIGACT 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