Andrey Rybalchenko

Professor

Contact

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

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: Proving Program Termination, CACM
  • New: Finding Heap-Bounds For Hardware Synthesis, FMCAD'2009
  • New: Summarization For Termination: No Return! FMSD
  • Subsumer-First: Steering Symbolic Reachability Analysis, SPIN'2009
  • Cardinality Abstraction For Declarative Networking, CAV'2009
  • InvGen: An Efficient Invariant Generator, CAV'2009
  • Automatic Discovery and Quantification of Information Leaks, Security & Privacy'2009
  • From Tests To Proofs, TACAS'2009 (best paper award at ETAPS'2009 from EAPLS)
  • Verifying Liveness for Asynchronous Programs, POPL'2009
  • Operational Semantics for Declarative Networking, PADL'2009
  • Complete list

Verification tools

  • 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.
  • InvGen - an efficient invariant generator.
  • RankFinder - well-foundedness checker and ranking function synthesizer.
  • Terminator - termination checker for C.

Current students

Graduated students

  • Nuno Lopes (master's thesis on declarative distributed programming and model checking PDF)

Lectures

Service

In the news