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.
Research Projects
Together with Doron Peled, I will study 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 Thomas Praveen Methrayil Varghese, I will study finite automata over infinite objects, suported by the competetive annual International Doctoral Studentship awarded by the School of Electrical Engineering, Electronics and Computer Science (since November 2011).
Together with John Fearnley (RA), Lesie Ann Goldberg (CI), Tom Shenton (CI), I (PI) study the control of Markov games and decision processes in the EPSRC project Synthesis and Verification in Markov Game Structures (October 2010--November 2013).
Together with Nathlie Bertrand I study the Analysis of Probabilistic Systems. Nathalie's sabatical visit from November 2011 till July 2012 is supported by a Leverhulme Visiting Fellowship.
Together with Doron Peled, I studied the control of distributed Monitors on our joint Royal Society grant Synthesising Permissive Monitors (November 2010--February 2011).
I am also 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 Course
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 our three MSc programmes, MRes students, and MEng students in their final year. |
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
| Thomas Praveen Methrayil Varghese studies finite automata over infinite objects and their transformations in his PhD thesis.
Frank Wolter is his second supervisor. |
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)
Publications
Here is a BibTex file containing references to most items listed below.
Please respect the copyright held by the respective publishers.
Journals
|
| Bernd Finkbeiner and Sven Schewe. Bounded Synthesis. International Journal on Software Tools for Technology Transfer, to appear. |
| Markus Rabe and Sven Schewe. Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games. Acta Informatica, 2011. |
| Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. Synthesizing Certificates in Networks of Timed Automata. IET Software, 2010. |
| Myrto Arapinis, Muffy Calder, Louise Denis, Michael Fisher, Philip Gray, Savas Konur, Alice
Miller, Eike Ritter, Mark Ryan, Sven Schewe, Chris Unsworth and Rehana Yasmin. Towards the Verification of Pervasive Systems. Electronic Communications of the EASST, 2010. |
| Sven Schewe and Bernd Finkbeiner. Semi-Automatic Distributed Synthesis. International Journal of Foundations of Computer Science, 2007. |
Conferences
| John Fearnley and Sven Schewe. Time and Parallelizability Results for Parity Games with Bounded Treewidth. ICALP 2012. |
| John Fearnley, Markus Rabe, Sven Schewe, and Lijun Zhang. Efficient Approximation of Optimal Control for Continuous-Time Markov Games. FSTTCS 2011. |
| Gal Katz, Doron Peled, and Sven Schewe. The Buck Stops Here: Order, Chance, and Coordination in Distributed Control. ATVA 2011. |
| Sven Schewe and Cong Tian. Synthesising Classic and Interval Temporal Logic. TIME 2011. |
| Gal Katz, Doron Peled, and Sven Schewe. Synthesis of Distributed Control through Knowledge Accumulation. CAV 2011. |
| Sven Schewe. Beyond Hyper-Minimisation--Minimising DBAs and DPAs is NP-Complete. FSTTCS 2010. |
| Bernd Finkbeiner and Sven Schewe. Coordination Logic. CSL 2010. |
| Sven Schewe. From Parity and Payoff Games to Linear Programming. MFCS 2009. |
| Sven Schewe. Tighter Bounds for the Determinisation of Büchi Automata. FoSSaCS 2009 (extended version). |
| Sven Schewe. Büchi Complementation Made Tight. STACS 2009. |
| Bernd Finkbeiner, Hans-Jörg Peter and Sven Schewe. Synthesizing Certificates in Networks of Timed Automata. RTSS 2008. |
| Sven Schewe. An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games. CSL 2008. |
| Sven Schewe. ATL* Satisfiability is 2EXPTIME-complete. ICALP 2008. |
| Bernd Finkbeiner, Hans-Jörg Peter and Sven Schewe. RESY: Requirement Synthesis for Compositional Model Checking. TACAS 2008. |
| Sven Schewe. Solving Parity Games in Big Steps. FSTTCS 2007. |
| Sven Schewe and Bernd Finkbeiner. Distributed Synthesis for Alternating-Time Logics. ATVA 2007. |
| Sven Schewe and Bernd Finkbeiner. Bounded Synthesis. ATVA 2007. |
| Sven Schewe. Synthesis for Probabilistic Environments. ATVA 2006 |
| Malte Helmert, Robert Mattmüller, and Sven Schewe. Selective Approaches for Solving Weak Games. ATVA 2006 |
| Bernd Finkbeiner, Sven Schewe, and Matthias Brill. Automatic Synthesis of Assumptions for Compositional Model Checking. FORTE 2006 |
| Sven Schewe and Bernd Finkbeiner. Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus. CSL 2006 |
| Sven Schewe and Bernd Finkbeiner. Synthesis of Asynchronous Systems. LOPSTR 2006. |
| Bernd Finkbeiner and Sven Schewe. Semi-Automatic Distributed Synthesis. ATVA 2005. |
| Bernd Finkbeiner and Sven Schewe. Uniform Distributed Synthesis.
LICS 2005. |
Workshops
| Markus Rabe and Sven Schewe. Optimal Time-Abstract Schedulers for CTMDPs and Markov Games. QAPL 2010. |
| Bernd Finkbeiner and Sven Schewe. SMT-Based Synthesis of Distributed Systems. AFM 2007. |
Thesis
| Sven Schewe. Synthesis of Distributed Systems. PhD Thesis. |
Invited
| Doron Peled and Sven Schewe. Practical Distributed Control Synthesis. INFINITY 2011. |
| Sven Schewe. Synthese Verteilter Systeme. it - Information Technology, 2010. |
| Sven Schewe. Software Synthesis is Hard -- and Simple. Dagstuhl Seminar 09501 on Software Synthesis, 2009. |
| Sven Schewe. Synthese Verteilter Systeme. Ausgezeichnete Informatikdissertationen, LNI, 2009. |
Invited Presentations
| Component Interfaces for System Synthesis. International Workshop on Foundations of Interface Technology (ETAPS 2008). Based on joint work with Bernd Finkbeiner. |
| Verifying Partial Designs. German Verification Day (satellite workshop of CONCUR 2006). Based on joint work with Bernd Finkbeiner. |
Ongoing Work / Technical Reports
| 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
Third International Symposium on Games, Automata, Logics and Formal
Verification (GandALF 2012), PC member. |
Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES 2012), PC member. |
Workshop on Synthesis (SYNT 2012), Co-Chair. |
Fourth International Workshop on Foundations of Interface Technologies (FIT 2012), PC member. |
Ninth International Symposium on Automated Technology (ATVA 2011), PC member. |
Annual Workshop of the ESF Networking Programme on Games for Design and Verification (GAMES 2011), Invited Tutorial. |
Administration
I serve as the Undergrad Admission Officer of the Department of Computer Science, the Widening Participation Officer of the School of Electrical Engineering, Electronics and Computer Science, and a member of our Board of Studies.
From 2009 to 2010, I was Deputy Exams and Assessment Officer.
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. |
| 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). |
Dr. Eduard Martin Preis 2008. Annual interdisciplinary award for outstanding theses of Saarland University.
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
|
|
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.