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: Rybalchenko:Andrey
Facilitated 3 volumes:
ExpertReviewPaPrBoard
EdContributed to:
2015
20142013
2013
2013
2013
20122012
20122012201120112011
2011201120112010
2010
201020102009
200920092009200820082007200720072007200720062006200520052005
2004200420162016Wrote 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.