|
|
Andrey Rybalchenko
Professor of Theoretical Computer
Science at TUM
|
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
- New: HMC: Verifying Functional Programs Using Abstract Interpreters, CAV'2011
- New: Threader: A Constraint-based Verifier for Multi-Threaded Programs, CAV'2011
- New: Separation Logic + Superposition Calculus = Heap Theorem Prover, PLDI'2011
- New: Transition Invariants and Transition Predicate Abstraction for Program Termination, TACAS'2011
- New: Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs, POPL'2011
- New: Distributed and Predictable Software Model Checking, VMCAI'2011
- New: From Tests to Proofs, journal version in STTT'2011
- New: Alligators for Arrays, LPAR'2010
- New: A Multi-Modal Framework for Achieving Accountability in Multi-Agent Systems, LIS'2010
- New: Non-Monotonic Refinement of Control Abstraction for Concurrent Programs, ATVA'2010
- New: Constraint Solving for Program Verification: Theory and Practice by Example (tutorial slides), CAV'2010
- New: Analyzing OCaml Using Verifiers for Imperative Programs, arXiv
- New: Thread-Modular Counterexample-Guided Abstraction Refinement, SAS'2010
- New: Applying Prolog to Develop Distributed Systems, ICLP'2010
- New: Approximation and Randomization for Quantitative Information-Flow Analysis, CSF'2010
- New: Constraint Based Interpolation, JSC, 2010
- New: Proving Program Termination, CACM, 2010 (ACM Digial Library)
- Finding Heap-Bounds For Hardware Synthesis, FMCAD'2009
- 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 (DBLP, Scholar, Arnetminer )
- 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.
- InvGen - an efficient invariant generator.
- RankFinder - well-foundedness checker and ranking function synthesizer.
- Terminator - termination checker for C.
Students
- Ashutosh Gupta
- Ruslán Ledesma Garza
- Swing by to discuss diplom/master project topics
Graduated students
- Nuno Lopes, Master's thesis (see VMCAI'2011 and ICLP'2010)
- Ashutosh Gupta, Master's thesis (see POPL'2008)
Lectures
2011:
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:
2012:
POPL ERC,
VMCAI (co-chair),
TACAS
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
- MIT TR35 (TUM press release, CIO.de article (in German))
- Microsoft Research Faculty Fellow
- Otto Hahn Medal
- Otto Hahn independent research group
- Günter-Hotz-Preis