Sven Schewe


Background

Sven Schewe I gained a Diplom degree in Computer Science (Diplom Informatiker) with a minor in Operations Research and Planning in 1997 from the University of the Federal Armed Forces Munich. Then I worked in the Command and Control Systems Command of the German Navy as a Systems Engineer in different fields of the analysis and construction of safety-critical systems, including the specification and construction of such systems as well as quality assurance and project management. To complement this, I gave myself a treat and studied Math at the FernUniversität in Hagen, earning a degree in Mathematics (Diplom Mathematiker) in 2004. Returning to education, I joined the Reactive Systems Group at the Department of Computer Science of Saarland University in 2004, and obtained a PhD (Dr. rer. nat.) in Computer Science in 2008.
I was appointed Lecturer in the Department of Computer Science at the University of Liverpool in September 2008.

Research Interests

I am interested in automata and game theory and its applications in the construction and analysis of safety-critical systems. This includes constructions and decision procedures for automata over infinite words and trees and games with infinite duration, as well as algorithms and tools for the automated verification and synthesis of reactive systems. My research concerns reactive computer systems and protocols: systems of concurrent processes that interact with each other and with their environment over a possibly infinite run. This family of systems contains many safety-critical applications like air traffic control systems, communication controllers in automotive systems, and security protocols. Parallelism and non-determinism make it difficult to design such systems correctly. I study automated methods that prove that an implementation satisfies a logical property (verification) and that derive implementations from logical specifications (synthesis).
I am a member of the Logic and Computation research group and affiliated with the Institute for Risk and Uncertainty.

Research Projects

Together with Ashutosh Trivedi, I will study the Stochastic Control of Cyber-Physical Systems. Ashutosh's research visit is supported by a Liverpool India Fellowship.

Together with Lijun Zhang, I will study the Analysis and Control of Markovian Systems. Lijun's research visit is supported by a Visiting Fellowship.

Together with Idress Husien, I study the control of adaptive systems and self learning intelligent systems, supported by an overseas PhD scholarship from the Iraqi Government (since January 2014).

Together with Anshul Gupta, I study equilibria of non-terminating multi player games, supported by a studentship of the School of Electrical Engineering, Electronics and Computer Science (since February 2013).

Together with Thomas Praveen Methrayil Varghese, I study finite automata over infinite objects, supported by the competitive International Doctoral Studentship, funded by the EPSRC (since November 2011).

Together with John Fearnley (RA), Lesie Ann Goldberg (CI till June 2013), Tom Shenton (CI), and Dominik Wojtczak (CI since June 2013), I (PI) have studied the control of Markov games and decision processes in the EPSRC project Synthesis and Verification in Markov Game Structures (October 2010--November 2013).

I have visited Anca Muscholl on a Visiting Professorship from Université Bordeaux I in September 2012 and January 2013.

I have visited Farn Wang on a travel grant for international scholars from the National Taiwan University in October 2012.

Together with Doron Peled, I have studied the synthesis of concise systems in February 2012, supported by a travel grant of the ESF Networking Programme on Games for Design and Verification.

Together with Nathlie Bertrand, I have studied the Analysis of Probabilistic Systems. Nathalie's sabbatical visit from November 2011 till July 2012 was supported by a Leverhulme Visiting Fellowship.

Together with Doron Peled, I have studied the control of distributed monitors on our joint Royal Society grant Synthesising Permissive Monitors (November 2010--February 2011).

I have also been associated with the EPSRC funded project Verifying Interoperability Requirements in Pervasive Systems.

If you are interested in drafting a research project with me, please contact me. If you want to do a PhD with me, please contact me as well.

Teaching

Current Courses

COMP524 - Safety and Dependability (since 2008/2009)
The module on "safety and dependability" covers topics such as: safety-critical systems, security, trusted systems, dependability and reliability, formal requirements engineering, design and development techniques and verification techniques. The module is intended for MSc students of six MSc programmes and MEng students in their final year. 
COMP516 - Research Methods in Computer Science (since 2014, with Dominik Wojtczak)
The module on "research methods" spans four MSc programmes. It is an introductory course on research in computer science on the postgraduate level. 

Previous Courses

University of Liverpool

COMP525 - Reasoning About Action and Change (2009/2010)
Dynamism and rapid change are features of the modern world. The module on "reasoning about action and change" is concerned with how to specify and verify dynamic systems. Different approaches to representing and reasoning about systems that change are studied, including topics such as: temporal logic, model checking, dynamic logic, and modelling change in artificial intelligence. Such techniques are useful in detecting errors in the design of systems at an early stage. The module is intended for MSc students. 

Saarland University, Co-Lectured with Bernd Finkbeiner

Automata, Games, and Verification (SS 08)
The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their non-terminating behaviour and persistent interaction with their environment. In this course we study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis. 
Games in Verification and Synthesis (SS 08)
In this seminar, we will study game-theoretic methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification). In both cases, we view the interaction between a software component and its environment as an infinite game; verification then amounts to checking that the strategy represented by the program is winning; synthesis amounts to deriving a winning strategy from a logical description of the winning condition.
Bachelor Seminar (WS 07/08) 
Verification (WS 07/08)
This course gives an introduction to various fields of systems verification, with an emphasis on algorithmic verification (model checking) and deductive verification (theorem proving). 
Automata, Games, and Verification (WS 06/07) 
Bachelor Seminar (SS 05) 

Research Students

Idress Husien studies the control of adaptive and self learning intelligent systems during his PhD. Second Supervisor: Dominik Wojtczak
Anshul Gupta studies equilibria of finte multi player games of infintie duration in her PhD thesis. Second Supervisor: Piotr Krysta
Thomas Praveen Methrayil Varghese studies finite automata over infinite objects and their transformations in his PhD thesis. Second Supervisor: Frank Wolter
I am also adviser to Yuji Dong (XJTLU), Christof Spanring and Muhammed Tufail and second supervisor to Mehmet Kurucan.

Previous Students

Markus Rabe. Optimal Schedulers for Time-Bounded Reachability in CTMDPs. Master Thesis (2009) 
   (Won the Günter Hotz Medaille 2010) 
Thomas von Bomhard. Minimization of Tree Automata. Bachelor Thesis (2008) 
Arnaud Fietzke. Learning Minimal Requirements for Compositional Verification. Bachelor Thesis (2006) 
Hans-Jörg Peter. Controller Program Synthesis for Industrial Machines. Diploma Thesis (2005) 
   (Won the Software-Engineering-Prize 2006 of the Ernst Denert Stiftung
Jens Regenberg. Synthesis of Reactive Systems. Diploma Thesis (2005) 
Tobias Maurer. Distributed Games For Reactive Systems. Diploma Thesis (2005) 

External Examinee

Wladimir Fridman. A Study of Pushdown Games. PhD Thesis, RWTH Aachen (2013) 

Publications

Here is a BibTex file containing references to most items listed below.

Journals

Conferences

Workshops

Thesis

Sven Schewe. Synthesis of Distributed Systems. PhD Thesis. 

Invited

Edited

Doron Peled and Sven Schewe. Editorial: Special Issue on Synthesis. Acta Informatica 51(3-4), 2014. 
Doron Peled and Sven Schewe. Proceedings of the First Workshop on Synthesis. EPTCS 84, 2012. 

Ongoing Work / Technical Reports

Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, and Lijun Zhang. Lazy determinisation for quantitative model checking. Computing Research Repository, arxiv.org/abs/1311.2928, 2013. 
Anshul Gupta and Sven Schewe. The benefit of law-making power. Computing Research Repository, arxiv.org/abs/1307.2051, 2013. 
John Fearnley, Doron Peled, and Sven Schewe. Synthesis of Succinct Systems. Computing Research Repository, arxiv.org/abs/1202.5449, 2012. 
John Fearnley and Sven Schewe. Time and Space Results for Parity Games with Bounded Treewidth. Computing Research Repository, arxiv.org/abs/1112.0221, 2011. 
John Fearnley, Markus Rabe, Sven Schewe, and Lijun Zhang. Efficient Approximation of Optimal Control for Markov Games. Computing Research Repository, arxiv.org/abs/1011.0397, 2010. 
Sven Schewe. Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata. Computing Research Repository, arxiv.org/abs/1007.1333, 2010. 
Markus Rabe and Sven Schewe. Optimal Schedulers for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games. Computing Research Repository, arxiv.org/abs/1004.4005, 2010. 
Markus Rabe and Sven Schewe. Optimal Schedulers for Time-Bounded Reachability in CTMDPs. AVACS Technical Report (ATR), 2009. 

Professional Activities

Past Visitors

Administration

I serve as the Admission Officer for Postgraduate Research students of the Department of Computer Science, the Widening Participation Officer of the School of Electrical Engineering, Electronics and Computer Science, and as a reviewer of our Ethics committee.
From 2010 to 2013, I have served as Undergrad Admission Officer, as an elected member of our Board of Studies, and as a member of the Board of Examiners for our joint courses with Carmel College and our disance learning programmes with Laureate. Prior to that, I was the Deputy Exams and Assessment Officer of our department.

Awards

Finalist for the ERCIM Cor Baayen Award 2010. Annual career award of the European Research Consortium for Informatics and Mathematics (ERCIM) for young researchers in computer science and applied mathematics. 

Dr. Eduard Martin Preis 2009. Annual interdisciplinary award for outstanding theses of Saarland University.

GI Dissertation Award 2008. Annual award for the best computer science dissertation in Germany, Austria, and Switzerland. The prize is jointly awarded by the Gesellschaft für Informatik e.V. (GI), Schweizer Informatik Gesellschaft (SI), Österreichischen Computergesellschaft (OCG), and the German Chapter of the ACM (GChACM)

Contact Details


  Sven Schewe
  University of Liverpool
  Department of Computer Science
  Ashton Building
  Ashton Street
  Liverpool L69 3BX
  United Kingdom

Office: Room G.14, Ashton Building email sven.schewe@liverpool.ac.uk tel (+44 151) 795 4242 fax (+44 151) 795 4235