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

We present ILAng, a platform for modeling and verification of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean separation of concerns between software and hardware through a unified formal model for heterogeneous processors and accelerators. Top-down it provides a specification for functional verification of hardware, and bottom-up it provides an abstraction for software/hardware co-verification. The ILAng platform provides a programming interface for (i) constructing ILA models (ii) synthesizing ILA models from templates using program synthesis techniques (iii) verifying properties on ILA models (iv) behavioral equivalence checking between different ILA models and ILA specifications and their implementation. It also provides for translating models and properties into various languages (e.g., Verilog and SMT LIB2) for different verification settings and use of third-party verification tools. This paper demonstrates utilities of the platform through case studies.

Tue 9 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Tool DemosTACAS at SUN I
Chair(s): Marius MikucionisAalborg University
14:00
15m
Talk
nonreach – A Tool for Nonreachability Analysis
TACAS
Florian Messner, Christian SternagelUniversity of Innsbruck, Austria
Link to publication
14:15
15m
Talk
The Quantitative Verification Benchmark Set
TACAS
Arnd HartmannsUniversity of Twente, Michaela KlauckSaarland Informatics Campus, Saarland University, David ParkerUniversity of Birmingham, Tim QuatmannRWTH 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 HuangPrinceton University, USA, Hongce Zhang, Aarti GuptaPrinceton University, Sharad MalikPrinceton 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 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
15:15
15m
Talk
Symbolic Regex Matcher
TACAS
Margus VeanesMicrosoft Research, Olli Saarikivi, Eric XuMicrosoft, USA, Tiki Wan
Link to publication
15:30
15m
Talk
COMPASS 3.0
TACAS
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
15:45
15m
Talk
Debugging of Behavioural Models with CLEAR
TACAS
Gianluca BarbonUniversit� Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaünUniversity of Grenoble Alpes
Link to publication