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
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

tacas-2019-papers
14:00 - 16:00: TACAS 2019 - Tool Demos at SUN I
Chair(s): Marius MikucionisAalborg University
tacas-2019-papers14:00 - 14:15
Talk
Florian Messner, Christian SternagelUniversity of Innsbruck, Austria
Link to publication
tacas-2019-papers14:15 - 14:30
Talk
Arnd HartmannsUniversity of Twente, Michaela KlauckSaarland Informatics Campus, Saarland University, David ParkerUniversity of Birmingham, Tim QuatmannRWTH Aachen University, Enno Ruijters
Link to publication
tacas-2019-papers14:30 - 14:45
Talk
Bo-Yuan HuangPrinceton University, USA, Hongce Zhang, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
Link to publication
tacas-2019-papers14:45 - 15:00
Talk
Link to publication
tacas-2019-papers15:00 - 15:15
Talk
Yu-Fang ChenAcademia Sinica, Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao Sun, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Junnan Xu
Link to publication
tacas-2019-papers15:15 - 15:30
Talk
Margus VeanesMicrosoft Research, Olli Saarikivi, Eric XuMicrosoft, USA, Tiki Wan
Link to publication
tacas-2019-papers15:30 - 15:45
Talk
Marco Bozzano, Harold Bruintjes, Alessandro CimattiFondazione Bruno Kessler, Joost-Pieter KatoenRWTH Aachen University, Thomas NollRWTH Aachen University, Stefano TonettaFondazione Bruno Kessler, Italy
Link to publication
tacas-2019-papers15:45 - 16:00
Talk
Gianluca BarbonUniversit� Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaünUniversity of Grenoble Alpes
Link to publication