Andrey Kupriyanov (Ph.D. Student)
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.
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).
- Arctor is a termination prover for multi-threaded programs.
- SLAB is a certifying model checker for infinite state concurrent systems.
|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.|
- 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