Andrey Rybalchenko

Verification Systems Group

Contact

Email
Phone+49 681 9325 668 (please email first)
Fax +49 681 9325 299 (not private)
MailMax Planck Institute for Software Systems
 Campus E1 4, D-66123 Saarbrücken, Germany
Office Martin-Luther-Strasse 12    (map)
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