Andrey Kupriyanov
Contact
Andrey Kupriyanov
eMail: andrey X kupriyanov Y ist.ac.at (replace X with . and Y with @)
About me
I have moved to the Institute of Science and Technology (IST) Austria, and work currently as a postdoctoral researcher in the research group of Prof. Tom Henzinger.
I have completed my Ph.D under the supervision of Prof. Bernd Finkbeiner in the Reactive Systems Group at Saarland University.
Research Interests
Temporal verification of concurrent and infinite-state programs, compositional methods and abstraction, synthesis of reactive programs, logic and decision procedures, automated reasoning. The unifying theme is the development of formal analysis and synthesis methods that scale up to real-life software and hardware systems.
Publications
Causal Termination of Multi-threaded Programs.
with Bernd Finkbeiner.26th International Conference on Computer Aided Verification (CAV 2014).
Causality-Based Verification of Multi-threaded Programs.
with Bernd Finkbeiner.24th International Conference on Concurrency Theory (CONCUR 2013).
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems.
with Klaus Dräger, Bernd Finkbeiner and Heike Wehrheim.16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010).
Tools
- Arctor is a termination prover for multi-threaded programs.
- SLAB is a certifying model checker for infinite state concurrent systems.
Teaching
SS 2014 | Advisor for the seminar Advanced Topics in Infinite Games |
WS 2013/14 | Advisor for the proseminar: The Time Machine |
SS 2013 | Tutor for the core lecture: Verification |
SS 2011 | Teaching assistant for the advanced lecture: Automata, Games and Verification. |
SS 2011 | Seminar instructor: Games, Synthesis and Robotics. |
WS 2009/10 | Teaching assistant for the core lecture: Verification. |
Selected Presentations
- Causality-based LTL Model Checking without Automata: Slides, Poster
Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October 2014
- Causality-based Verification of Multi-threaded Programs: Slides
Plenary talk, project meeting of SFB/TR 14 AVACS, Saarbrücken, Germany, September 2014
- Causality-based LTL Model Checking without Automata: Slides
Highlights of Logic, Games, and Automata 2014, Paris, France, September 2014
- Causal Termination of Multi-threaded Programs: Slides
Computer Aided Verification, CAV 2014, Vienna, Austria, July 2014
- Causality-Based Verification of Multi-threaded Programs: Slides
Concurrency Theory, CONCUR 2013, Buenos-Aires, Argentina, August 2013
- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems: Slides
Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Paphos, Cyprus, March 2010