The tutorials day of HVC 2012 will be held on November 4. Like the main conference, the tutorials day will also take place at IBM Research – Haifa, located on the University of Haifa campus, Mount Carmel in Haifa, Israel.
09:15 Opening Remarks,
Itai Segall, IBM Research – Haifa
09:30 Tutorial 1: Idiom-based Verification of Highly Concurrent Data Structures Using Temporal Separation Logic,
Dr. Noam Rinetzky, Tel Aviv University
11:30 Tutorial 2: Three-Valued Abstraction-Refinement,
Dr. Sharon Shoham Buchbinder, Academic college of Tel Aviv-Yaffo
One of the most successful approaches to fighting the state-explosion problem in model checking is abstraction. Abstractions hide certain details of the system in order to result in a smaller model. In some cases the abstraction is too coarse, resulting in an inconclusive model checking result. Thus, the abstract model is refined by adding more details into it, making it more similar to the concrete model. Iterating this process is called abstraction-refinement.
Typically, abstractions are designed such that `true' results are preserved from an abstract model to the concrete model, but `false' results may be spurious. Such abstractions usually handle only the universal fragments of temporal logics and are based on a 2-valued semantics. 3-valued abstractions, on the other hand, are based on a 3-valued semantics in which a property can be evaluated to `true', `false', or `unknown'. Both `true' and `false' results are preserved from an abstract model to the concrete one, leaving only the `unknown' result inconclusive. 3-valued abstractions are powerful since they can be used for both verification and refutation of properties. Further, they can handle full branching temporal logic (e.g. CTL, CTL*, mu-calculus) and not just their universal fragment.
In this talk we will present 3-valued abstraction and refinement. We will describe several 3-valued models, and their use as abstract models. We will then discuss model checking and refinement techniques for such models.
Her research interests lie in the area of formal verification and program analysis, including model checking, abstraction-refinement, 3-valued semantics, compositional reasoning, SAT-based techniques, specification mining and more.
14:15 Tutorial 3: Simulating Cyber-Physical Systems Using SysML and Numerical Simulation Tools,
Eldad Palachi, IBM Rational
16:00 Tutorial 4: Improving Verification Productivity with the Dynamic Load and Reseed Methodology,
Marat Teplitsky, Cadence
It should be clear that reusing commonalities from the different runs can dramatically reduce verification time. This can be done using the following flow: First, save the simulation state after the shared run. Then, restore that saved simulation state multiple times, each time modifying various post-restore capabilities. Examples of such modifications are: changing the random seed, changing functionality by loading new code at the restore point, and switching to debug mode.
Most simulation engines support the save and restore of the simulation state; and the Universal Verification Methodology (UVM) standard allows these capabilities. However, as of today, only Specman 'e' language has these capabilities implemented, as part of Specman Advanced Option.
17:30 End of tutorial day
As in previous years, the post-conference proceedings will be published in Springer's Lecture Notes in Computer Science series (LNCS).