RiSE workshop is a 3 1/2 days event on the topics of formal verification, games, synthesis, and decision procedures.
The format is: two invited talks per day, followed by discussion tables, and poster sessions.
The goal is to increase fruitful collaboration within RiSE and with our dear invited speakers.
The workshop is organized by RiSE and LogiCS students.
The round-table discussions will be moderated by invited speakers and based on their tutorials. They will be held in small groups of participants who are either working in or are curious about the particular tutorial topic. The goal of the workshop is to engage students in discussions on the current state of the art and open problems in the area of formal methods.
Students are encouraged to present their ongoing research on a poster or a flipchart.
Hotel rate for bed and breakfast is to be paid upon arrival.
1 night incl. breakfast: Eur 108.
Invited speakers, for you the ticket is free! Please contact us if you haven’t yet received the discount code.
Christoph M. Wintersteiger
Sven Schewe, Synthesis of Reactive Systems (synthesis.pdf and games.pdf)
Synthesis of reactive systems is a research direction inspired by Church’s realisability problem. It focuses on systems that receive a constant stream of inputs from an environment, and must, for each input, produce some output. Specifically, we are given a logical specification that dictates how the system must react to the inputs, and we must construct a system that satisfies the specification for all possible inputs that the environment could provide. While the verification problem (the validation or refutation of the correctness of such a system) has gained many algorithmic solutions and various successful tools, the synthesis problem has had fewer results. We focus on the classical approach by Pnueli and Rosner, which links synthesis to emptiness games of automata and the treatment of incomplete information. We will discuss why these approaches require determinisation and how the resulting automata can be simplified with respect to their acceptance mechanism. For pleasure, we might look into a connection between complexity classes and the existence of succinct control strategies.
Christoph Wintersteiger, Decision Procedures (pdf, pptx)
This talk reviews the basic background on decision procedures with a focus on applications in verification. Thereafter we will see two examples of recently developed decision procedures for the (SMT) theories of floating-point numbers and bit-vectors. Finally, future work and a number of open problems in the area will be discussed.
Luca Bortolussi, Mean-field Approximation for Stochastic Verification (pdf)
In this talk we will consider the problem of verifying properties of stochastic models of large systems of interacting agents. Examples span from systems biology to epidemiology, from ecology to performance evaluation and smart cities design. These systems are typically made of a large number of entities, resulting in very large state spaces, beyond the reach of current stochastic model checkers. We will explore an alternative approach, based on ideas of stochastic approximation, like mean-field and liner noise. Basically, we approximate the original model with a simpler one, on a continuous state space, and check the properties on this approximation. Some classes of properties can be checked extremely efficiently in this way, with a good accuracy, improving with the size of the model. This talk will be a gentle introduction to these ideas, providing an overview of verification based on stochastic approximation.
Wilfried Steiner, Formal Verification of Clock Synchronisation Algorithm (pdf)
Formal Verification of Clock Synchronization Algorithm: First time by means of Model Checking (sal-inf-bmc + k-induction).
Incremental Formal Verification of Diagnosis and Clock-Rate Correction for Clock Synchronization Algorithms: Model Checking (sal-inf-bmc + k-induction).
SMT-Solvers as core tooling for Cyber-Physical Systems Configuration: Use of SMT-solvers to generate and verify configuration for distributed systems.
Formal Verification of TTA and PALS:
- Verification of key properties of the time-triggered architecture (TTA) and the physically-asynchronous logically synchronous (PALS) design pattern
- Formal verification by means of theorem proving (PVS)
Ruediger Ehlers, Reactive Synthesis for Cyber-Physical System Control (pdf)
In a cyber-physical system (CPS), a discrete controller influences its physical environment in a way such that some specified property is enforced.
Due to the continuous dynamics of the environment and the often complex specifications of the desired system behavior, constructing such a controller is difficult. The process of reactive synthesis, where a controller is synthesized automatically from its specification, helps with the development process of such a controller. Rather than writing the controller by hand, the system engineer can focus on ensuring the correctness of the specification that is the input to the synthesis process.
The synthesis process for CPS controllers is however quite different from traditional reactive synthesis. The controllers need to be implemented in a robust way, i.e., such that small deviations from the specified environment conditions can be tolerated by the controller. Similarly, the controller should not make it unnecessarily difficult for the environment to satisfy its own specification. If a cost function for the controller’s actions is given (which, for instance, could model the energy consumption of control actions), we are also interested in obtaining efficient controllers. In this talk, we will discuss such aspects of CPS controller synthesis. Live demonstrations will exemplify the main ideas, and an outlook onto future unified frameworks for scalable CPS controller synthesis will be given.
Javier Esparza, Keeping a Crowd Safe: Parameterized Verification (pdf)
We survey some results on the automatic verification of parameterized programs without identities. These are systems composed of arbitrarily many components, all of them running exactly the same finite-state program. We discuss the complexity of deciding that no component reaches an unsafe state.
We would like to invite you to the RiSE Workshop 2016 Dates: 26-29 September 2016 Venue: Hotel Retter, Pöllauberg, Austria The workshop is hosted and organised by the students of the Austrian Society for Rigorous Systems Engineering (RiSE). The workshop is targeted at doctoral students in Computer Science and Mathematics with a strong interest in Logic and Automated Verification. We particularly encourage members of the RiSE research network, LogiCS doctoral college, PUMA and ExCape research networks, but the event is open to all interested students. The goal of the workshop is to engage students in discussions on the current state of the art and open problems in the area of formal methods. The workshop will feature: + Invited talks from academia and industry + Interactive discussion sessions + Poster sessions + Social events We encourage all participating students to take part in the poster sessions to present their ongoing research using a poster or a flipchart. More info at: http://arise.or.at/rise-workshop-2016/