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