ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 14:45 - 15:00 at SUN I - Tool Demos Chair(s): Marius Mikucionis

Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its specified contract. However, not all high-level (e.g. security-related) properties of a software module can be easily expressed through function contracts. To address this issue, this tool demo paper proposes a new specification mechanism, called meta-properties, able to express a rich set of high-level properties. A meta-property can be seen as an enhanced global invariant specified for all or a subset of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can then be proved by deductive verification tools in a usual way. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove several safety- and security-related meta-properties in two illustrative case studies.

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
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