Dana Fisman – författare

Functional veri?cation is hard. Period. No disagreement here. But why is this so? Consider today’s design ?ow: much of it is more or less automated, from RTL to netlist to layout to silicon. But all this automation depends upon having correct RTL input to start with, and there is little or no automation to help with RTL creation. It is hard enough for a designer to decide what RTL model he wants to build, and then to describe that RTL model correctly in a hardware description language. It is even more di?cult for a veri?cation engineer, who can’t read the designer’s mind, to verify that what the designer created not only represents the RTL model he had conceived, but also that the RTL model is an appropriate one for the problem at hand. What makes RTL modeling and veri?cation di?cult is concurrency. It is easy to teach an engineer how to write procedural code that conforms to the synthesizable subset of a hardware description language. What is hard is understanding how the engineer’s procedural code interacts with other c- ponents in the design over time. In fact, until recently we lacked e?ective languages to describe concurrent behaviors. The IEEE 1850 Property Speci?cation Language (PSL) is a language for the formal speci?cation of concurrent systems. The language is particularly applicable for writing assertions about hardware designs. PSL supports m- tiple veri?cation paradigms – including formal analysis, simulation, and acc- eration/emulation.

This book constitutes the refereed proceedings of the 21st International Conference on Runtime Verification, RV 2021, held virtually during October 11-14, 2021.The 11 regular papers and 7 short/tool/benchmark papers presented in this book were carefully reviewed and selected from 40 submissions. Also included is one tutorial paper.The RV conference is concerned with all aspects of monitoring and analysis of hardware, software and more general system executions.

This book constitutes the refereed proceedings of the 21st International Conference on Runtime Verification, RV 2021, held virtually during October 11-14, 2021.

The 11 regular papers and 7 short/tool/benchmark papers presented in this book were carefully reviewed and selected from 40 submissions. Also included is one tutorial paper.

The RV conference is concerned with all aspects of monitoring and analysis of hardware, software and more general system executions.

 

This open access book constitutes the proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022, which was held during April 2-7, 2022, in Munich, Germany, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022. The 46 full papers and 4 short papers presented in this volume were carefully reviewed and selected from 159 submissions. The proceedings also contain 16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report.TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, exibility, and efficiency of tools and algorithms for building computer-controlledsystems.