Andrey Rybalchenko

Andrey Rybalchenko

28.03.2013: I joined Microsoft Research

01.2010-01.2014: Professor of Theoretical Computer Science at TUM

Curriculum vitae

Emailfirst five letters of my last name @in.tum.de
Phone+49 89 289 17209
Fax +49 89 289 17207
Office MI 03.11.044 in Garching
MailInstitut für Informatik (I7), Technische Universität München,
 Boltzmannstr. 3, 85748 Munich, Germany

Research

Temporal verification of reactive systems, proving liveness and termination, program analysis and verification,
automated abstraction and refinement, constraint-based verification, verification of liveness properties,
invariant and ranking function generation, interpolation, contraint logic programming,
development and verification of distributed systems, (quantitative and qualitative) information flow analysis

Recent publications
  • New: A Constraint-Based Approach to Solving Games on Infinite Graphs, POPL'2014
  • New: Separation Logic Modulo Theories, APLAS'2013
  • New: Automation of Quantitative Information-Flow Analysis, SFM'2013
  • New: Program Verification as Horn Constraint Solving (tutorial slides), 2013
  • New: An Epistemic Perspective on Consistency of Concurrent Computations, CONCUR'2013
  • New: On Solving Universally Quantified Horn Clauses, SAS'2013
  • New: Solving Existentially Quantified Horn Clauses, CAV'2013
  • New: Separation Logic Modulo Theories, CoRR TR, 2013
  • New: Generalised Interpolation by Solving Recursion-Free Horn Clauses, CoRR TR, 2013
  • New: Threader: A Verifier for Multi-threaded Programs - (Competition Contribution), TACAS'2013
  • New: ERC Starting Grant: Automatic Synthesis of Software Verification Tools from Proof Rules, 2012-2017
  • Program Verification as Satisfiability Modulo Theories, SMT'2012
  • Binary Reachability Analysis of Higher Order Functional Programs, SAS'2012
  • Synthesizing software verifiers from proof rules, PLDI'2012
  • HSF(C): a software verifier based on Horn clauses, Software verification competition at TACAS'2012
  • Compositional Termination Proofs for Multi-Threaded Programs, TACAS'2012
  • Solving Recursion-Free Horn Clauses over LI+UIF, APLAS'2011
  • HMC: Verifying Functional Programs Using Abstract Interpreters, CAV'2011
  • Threader: A Constraint-based Verifier for Multi-Threaded Programs, CAV'2011
  • Separation Logic + Superposition Calculus = Heap Theorem Prover, PLDI'2011
  • Transition Invariants and Transition Predicate Abstraction for Program Termination, TACAS'2011
  • Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs, POPL'2011
  • Distributed and Predictable Software Model Checking, VMCAI'2011
  • Complete list (DBLP and Scholar )
Software
  • ARMC - abstraction refinement-based model checker for safety and liveness properties.
  • Cardan - cardinality abstraction-based verifier for declarative networking applications.
  • CLP-Prover - constraint-based tool for interpolant generation.
  • DAHL - a Prolog-based distributed programming system.
  • HSF - a constraint solver for Horn clauses
  • InvGen - an efficient invariant generator.
  • RankFinder - well-foundedness checker and ranking function synthesizer.
  • Terminator - termination checker for C.

Students

Graduated students

Lectures

2014: PLDI, ICLP
2013: Software Correctness and Reliability, DEDUCTION, TAPAS, AVM, Formal Techniques, Model Checking
2012: SPIN, Model Checking, Pearls of Computer Science 3, Fundamental Algorithms
2011: Einführung in die Informatik II, Perlen der Informatik, Model Checking
2010: Einführung in die Informatik II, CAV (tutorial), CSL, HTDC, Model Checking
2009: WING, SYNASC
2008: MOVEP, VSTTE-THEORY
2007: Software Model Checking (Winter 2007/08)

Service

Program committee:
2014: POPL, RV, FoSSaCS, GRAPHITE, TGC, PLDI ERC, PSI
2013: ISSTA, VSTTE (co-chair), PSSV, ASE
2012: POPL ERC, VMCAI (co-chair), TACAS, LOPSTR, PSSV
2011: CAV, ESOP, PLDI ERC, VMCAI, MEMICS, ATVA, 2FC (co-chair)
2010: POPL, PLPV, VSTTE, SAS, PASTE, LPAR, WING, SAVCBS
2009: VMCAI, APV, CSR (application track chair), CAV, Beyond SAT, FMICS
2008: LPAR
2007: PPDP

Awards

In the news