Debugging of Behavioural Models with CLEAR (TACAS 2019) - ETAPS 2019

Sat 6 - Thu 11 April 2019 Prague, Czech Republic

Who

Gianluca Barbon, Vincent Leroy, Gwen Salaün

Track

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 9 Apr 2019 15:45 - 16:00 at SUN I - Tool Demos Chair(s): Marius Mikucionis

Abstract

This paper presents a tool for debugging behavioural models being analysed using model checking techniques. It consists of three parts: (i) one for handling temporal formulas and behavioural models in order to compute annotated models, (ii) one for visualizing the erroneous part of the model with a specific focus on decision points that make the model to be correct or incorrect, and (iii) one for abstracting counterexamples thus providing an explanation of the source of the bug.

Link to Publication

https://link.springer.com/chapter/10.1007/978-3-030-17462-0_26

Gianluca Barbon

Universit� Grenoble Alpes, Inria, LIG

Vincent Leroy

University of Grenoble - CNRS

Gwen Salaün

University of Grenoble Alpes

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Tue 9 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	14:00 - 16:00	Tool DemosTACAS at SUN I Chair(s): Marius Mikucionis Aalborg University

	14:00 15m Talk		nonreach – A Tool for Nonreachability Analysis TACAS Florian Messner , Christian Sternagel University of Innsbruck, Austria Link to publication
	14:15 15m Talk		The Quantitative Verification Benchmark Set TACAS Arnd Hartmanns University of Twente, Michaela Klauck Saarland Informatics Campus, Saarland University, David Parker University of Birmingham, Tim Quatmann RWTH Aachen University, Enno Ruijters Link to publication
	14:30 15m Talk		ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions TACAS Bo-Yuan Huang Princeton University, USA, Hongce Zhang , Aarti Gupta Princeton University, Sharad Malik Princeton University Link to publication
	14:45 15m Talk		MetAcsl: Specification and Verification of High-Level Properties TACAS Virgile Robles , Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Pascale Le Gall Link to publication
	15:00 15m Talk		ROLL 1.0: $\omega$-Regular Language Learning Library TACAS Yu-Fang Chen Academia Sinica, Yong Li Institute of Software, Chinese Academy of Sciences, Xuechao Sun , Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Junnan Xu Link to publication
	15:15 15m Talk		Symbolic Regex Matcher TACAS Margus Veanes Microsoft Research, Olli Saarikivi , Eric Xu Microsoft, USA, Tiki Wan Link to publication
	15:30 15m Talk		COMPASS 3.0 TACAS Marco Bozzano , Harold Bruintjes , Alessandro Cimatti Fondazione Bruno Kessler, Joost-Pieter Katoen RWTH Aachen University, Thomas Noll RWTH Aachen University, Stefano Tonetta Fondazione Bruno Kessler, Italy Link to publication
	15:45 15m Talk		Debugging of Behavioural Models with CLEAR TACAS Gianluca Barbon Universit� Grenoble Alpes, Inria, LIG, Vincent Leroy University of Grenoble - CNRS, Gwen Salaün University of Grenoble Alpes Link to publication