BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//HiPEDS – EPSRC Centre for Doctoral Training - ECPv6.15.11//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://wp.doc.ic.ac.uk/hipeds
X-WR-CALDESC:Events for HiPEDS – EPSRC Centre for Doctoral Training
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20180101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20190215T140000
DTEND;TZID=UTC:20190215T150000
DTSTAMP:20260418T061252
CREATED:20190214T155203Z
LAST-MODIFIED:20190214T155203Z
UID:2016-1550239200-1550242800@wp.doc.ic.ac.uk
SUMMARY:HiPEDS Seminar: Symbolic Repairs for GR(1) Specifications
DESCRIPTION:Title: Symbolic Repairs for GR(1) Specifications \nSpeaker: Jan Oliver Ringert\, Lecturer in Model-Based Software Development in the Department of Informatics at the University of Leicester \nAbstract: Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. Examples include GR(1)\, an expressive assume-guarantee fragment of LTL\, that enables efficient synthesis of the software controllers of robotic systems. \nUnrealizability is a major challenge for synthesis. Some works attempt to help engineers deal with unrealizability by generating counter-strategies or computing an unrealizable core. Other works propose to repair the unrealizable specification by suggesting repairs in the form of automatically generated assumptions. \nWe present two novel symbolic algorithms for repairing unrealizable GR(1) specifications. The first algorithm infers new assumptions based on the recently introduced JVTS. The second algorithm infers new assumptions directly from the specification. Both algorithms are sound. The first is incomplete but can be used to suggest many different repairs. The second is complete but suggests a single repair. Both are symbolic and therefore efficient. \nJoint work with Shahar Maoz and Rafi Shalom within the ERC StG SYNTECH project that addresses challenges related to the change from writing code to writing specifications\, and the development of tools to support a specification-centric rather than a code-centric development process. http://smlab.cs.tau.ac.il/syntech/ \nBiography: Jan Oliver Ringert joined the Department of Informatics of the University of Leicester\, Leicester\, UK in February 2018 as a Lecturer in Model-Based Software Development. Previously\, he was a PostDoc in the Software Modeling group of Shahar Maoz at the School of Computer Science\, Tel Aviv University\, Israel (12/2013-01/2018). Before\, he worked in the Software Engineering group of Bernhard Rumpe at RWTH Aachen University\, Germany (10/2008-11/2013). He received his Computer Science diploma (Dipl.-Inform.) from TU Braunschweig\, Germany (2003-2008). \nHis research interests include model-based software engineering with a focus on software evolution and the software engineering aspects of synthesis of reactive systems.
URL:https://wp.doc.ic.ac.uk/hipeds/event/hipeds-seminar-symbolic-repairs-for-gr1-specifications/
LOCATION:Huxley Building\, Room 217/218\, Imperial College London\, London\, SW7 2AZ\, United Kingdom
END:VEVENT
END:VCALENDAR