Andrey Rybalchenko

Contact

01.01.2010: I moved to the Technische Universität München.

Visit my homepage at TUM.

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