BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × China
1 × Czech Republic
1 × Estonia
1 × Finland
1 × Germany
1 × Russia
14 × USA
2 × Denmark
2 × Italy
5 × United Kingdom
6 × France
Collaborated with:
A.Podelski C.Popeea A.Gupta B.Cook R.Majumdar J.A.N.Pérez N.P.Lopes N.Bjørner B.Köpf T.A.Henzinger K.v.Gleissenthall K.L.McMillan A.Malkis T.A.Beyene A.Singh R.Ledesma-Garza D.Beyer V.Sofronie-Stokkermans S.Grebenshchikov R.Jhala P.Ganty T.Wies A.Pnueli S.Chaudhuri S.Gulwani T.Lev-Ami M.Sagiv R.Xu A.Gotsman M.Y.Vardi G.D.Plotkin G.Varghese
Talks about:
program (12) termin (9) abstract (8) verifi (8) thread (7) verif (7) solv (6) constraint (5) softwar (5) invari (5)

♂ Person: Andrey Rybalchenko

DBLP DBLP: Rybalchenko:Andrey

Facilitated 3 volumes:

ASE 2013ExpertReviewPa
ASE 2013PrBoard
VMCAI 2012Ed

Contributed to:

CAV 20152015
POPL 20142014
CAV 20132013
SAS 20132013
SFM 20132013
TACAS 20132013
PLDI 20122012
SAS 20122012
SMT 20122012
TACAS 20122012
CAV 20112011
PLDI 20112011
POPL 20112011
PPDP 20112011
TACAS 20112011
VMCAI 20112011
CAV 20102010
CSL 20102010
ICLP 20102010
SAS 20102010
CAV 20092009
PADL 20092009
POPL 20092009
TACAS 20092009
CAV 20082008
POPL 20082008
PADL 20072007
PLDI 20072007
POPL 20072007
SAS 20072007
VMCAI 20072007
CAV 20062006
PLDI 20062006
POPL 20052005
SAS 20052005
TACAS 20052005
LICS 20042004
VMCAI 20042004
PLDI 20162016
POPL 20162016

Wrote 46 papers:

CAV-2015-GleissenthallKR #verification
Symbolic Polytopes for Quantitative Interpolation and Verification (KvG, BK, AR), pp. 178–194.
POPL-2014-BeyeneCPR #approach #constraints #game studies #graph #infinity
A constraint-based approach to solving games on infinite graphs (TAB, SC, CP, AR), pp. 221–234.
CAV-2013-BeyenePR #horn clause #quantifier
Solving Existentially Quantified Horn Clauses (TAB, CP, AR), pp. 869–882.
SAS-2013-BjornerMR #horn clause #on the #quantifier
On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.
SFM-2013-KopfR #analysis #automation #data flow
Automation of Quantitative Information-Flow Analysis (BK, AR), pp. 1–28.
TACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread #verification
Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.
PLDI-2012-GrebenshchikovLPR #proving #verification
Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
SAS-2012-Ledesma-GarzaR #analysis #functional #higher-order #reachability #source code
Binary Reachability Analysis of Higher Order Functional Programs (RLG, AR), pp. 388–404.
SMT-2012-BjornerMR #modulo theories #satisfiability #verification
Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
TACAS-2012-GrebenshchikovGLPR #contest #horn clause #verification
HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.
TACAS-2012-PopeeaR #composition #concurrent #multi #proving #source code #termination #thread
Compositional Termination Proofs for Multi-threaded Programs (CP, AR), pp. 237–251.
CAV-2011-GuptaPR #concurrent #constraints #multi #named #source code #thread #verification
Threader: A Constraint-Based Verifier for Multi-threaded Programs (AG, CP, AR), pp. 412–417.
CAV-2011-JhalaMR #functional #named #source code #using #verification
HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.
PLDI-2011-PerezR #calculus #logic #proving #theorem proving
Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.
POPL-2011-GuptaPR #abstraction #concurrent #multi #refinement #source code #thread #verification
Predicate abstraction and refinement for verifying multi-threaded programs (AG, CP, AR), pp. 331–344.
PPDP-2011-Rybalchenko #automation #synthesis #tool support #towards #verification
Towards automatic synthesis of software verification tools (AR), pp. 3–4.
TACAS-2011-PodelskiR #abstraction #invariant #termination
Transition Invariants and Transition Predicate Abstraction for Program Termination (AP, AR), pp. 3–10.
VMCAI-2011-LopesR #distributed #model checking #predict
Distributed and Predictable Software Model Checking (NPL, AR), pp. 340–355.
CAV-2010-Rybalchenko #constraints #theorem proving #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CSL-2010-Rybalchenko #constraints #theorem proving #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), p. 51.
ICLP-J-2010-LopesNRS #distributed #prolog
Applying Prolog to develop distributed systems (NPL, JANP, AR, AS), pp. 691–707.
SAS-2010-MalkisPR #abstraction #refinement #thread
Thread-Modular Counterexample-Guided Abstraction Refinement (AM, AP, AR), pp. 356–372.
CAV-2009-GuptaR #generative #invariant #named #performance
InvGen: An Efficient Invariant Generator (AG, AR), pp. 634–640.
CAV-2009-PerezRS #abstraction #declarative #network
Cardinality Abstraction for Declarative Networking Applications (JANP, AR, AS), pp. 584–598.
PADL-2009-NavarroR #declarative #network #semantics
Operational Semantics for Declarative Networking (JANP, AR), pp. 76–90.
POPL-2009-GantyMR #liveness #source code #verification
Verifying liveness for asynchronous programs (PG, RM, AR), pp. 102–113.
TACAS-2009-GuptaMR #proving #testing
From Tests to Proofs (AG, RM, AR), pp. 262–276.
CAV-2008-CookGLRS #proving #termination
Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
CAV-2008-PodelskiRW
Heap Assumptions on Demand (AP, AR, TW), pp. 314–327.
POPL-2008-GuptaHMRX #proving
Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.
PADL-2007-PodelskiR #abstraction #logic #model checking #named #refinement
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement (AP, AR), pp. 245–259.
PLDI-2007-BeyerHMR #invariant
Path invariants (DB, TAH, RM, AR), pp. 300–309.
PLDI-2007-CookPR #concurrent #proving #termination #thread
Proving thread termination (BC, AP, AR), pp. 320–330.
POPL-2007-CookGPRV #proving #source code
Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
SAS-2007-MalkisPR #precise #thread #verification
Precise Thread-Modular Verification (AM, AP, AR), pp. 218–232.
VMCAI-2007-BeyerHMR #invariant #synthesis
Invariant Synthesis for Combined Theories (DB, TAH, RM, AR), pp. 378–394.
VMCAI-2007-RybalchenkoS #constraints #theorem proving
Constraint Solving for Interpolation (AR, VSS), pp. 346–362.
CAV-2006-CookPR #named #safety
Terminator: Beyond Safety (BC, AP, AR), pp. 415–418.
PLDI-2006-CookPR #proving #termination
Termination proofs for systems code (BC, AP, AR), pp. 415–426.
POPL-2005-PodelskiR #abstraction #termination
Transition predicate abstraction and fair termination (AP, AR), pp. 132–144.
SAS-2005-CookPR #abstraction #refinement #termination
Abstraction Refinement for Termination (BC, AP, AR), pp. 87–101.
TACAS-2005-PnueliPR #analysis
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems (AP, AP, AR), pp. 124–139.
LICS-2004-PodelskiR #invariant
Transition Invariants (AP, AR), pp. 32–41.
VMCAI-2004-PodelskiR #linear #ranking #synthesis
A Complete Method for the Synthesis of Linear Ranking Functions (AP, AR), pp. 239–251.
PLDI-2016-GleissenthallBR #quantifier #verification
Cardinalities and universal quantifiers for verifying parameterized systems (KvG, NB, AR), pp. 599–613.
POPL-2016-PlotkinBLRV #network #scalability #symmetry #using #verification
Scaling network verification using symmetry and surgery (GDP, NB, NPL, AR, GV), pp. 69–83.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.