Abstract: Verifying highly concurrent pointer-linked data structures requires reasoning about properties of unbounded collections of dynamically allocated objects manipulated by an unbounded number of threads. This form of reasoning is challenging because the high degree of inter-thread interference leads to scenarios which defy human intuition. This talk presents an approach which aims to simplify the reasoning by exposing hidden programming idioms which govern the interference. The idioms are formalized as temporal invariants in separation logic. Hence, in the talk I will present a high level overview of separation logic and its usages for concurrent verification.

Dr. Noam Rinetzky has graduated from Tel Aviv University in 2008, where he completed his PhD under the supervision of Mooly Sagiv. After his graduation, he was a post-doctoral researcher at Queen Mary University of London in the group of Peter O'Hearn, where he received a Royal Academy of Engineering/EPSRC research fellowship. He joins the School of Computer Science at Tel Aviv University as a senior lecturer in October 2012. Prior to his doctoral studies, Noam worked for three years in IBM Haifa Research Laboratory on storage systems.

Abstract: Model checking is an automated technique for checking whether a given system model fulfills a desired property, described as a temporal logic formula. As real models tend to be very big, model checking encounters the state-explosion problem, which refers to its high space requirements.
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.

Dr. Sharon Shoham Buchbinder received a B.A. degree in Computer Science (summa cum laude) in 2001, a M.Sc. degree (cum laude) in 2004, and a Ph.D. degree in 2009, all from the Computer science department of the Technion-Israel Institute of Technology. She is currently a senior lecturer at the school of Computer Science at the Academic college of Tel Aviv-Yaffo.
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.

Abstract: The term Cyber-Physical System (CPS) refers to the integration of computation with physical processes. An embedded computerized system is controlling and monitoring physical processes where the processes affect the computations and vice versa. Designing such systems requires a multidisciplinary approach combining software engineering, electro-mechanical engineering, networks and physics. Therefore designing complex CPS, such as aerospace and automotive systems, requires systems engineering to analyze the requirements and design the overall solution. In addition, advanced numerical simulation tools, such as MATLAB Simulink or tools implementing the Modelica language, are commonly used to validate requirements, describe continuous algorithms and simulate physical processes along with their interaction with the system. The SysML language, which is considered the standard modeling language for model-based systems engineering, is well suited for requirements analysis, architectural design and discrete behavior specification, however it lacks the strengths of the numerical tools to specify and simulate continuous behaviors. In this tutorial we will show several techniques on how to combine SysML and Numerical models that can be used for simulating the overall system. We will examine a "hosted simulation" approach in which implementation auto generated from the numerical tool is imported (along with the interface specification) into the SysML model and a "plant simulation approach" in which parts of the SysML model is exported to the numerical tool for simulation. This will be based on an example case study using IBM Rational Rhapsody as the SysML tool and MATLAB Simulink as the numerical tool.

Eldad Palachi is a software architect leading the systems engineering features development for the IBM Rational Rhapsody development team in Rehovot Israel. His main field of expertise is Model-Based Systems and Software Engineering using executable models. Eldad is representing IBM in the definition of the SysML language at the OMG and has been involved in the definition of SysML since its inception.He is also involved in other standardization activities such as the definition of the UML Testing Profile. In the past, Eldad coordinated the development of Rhapsody Test Conductor and Rhapsody ATG and led the development of Rhapsody model simulation capabilities. He has been working in the Rhapsody development team since 1999. He holds an M.Sc. from Tel-Aviv university in Chemical Physics.

Abstract: Simulation-based functional verification involves a multitude of tests that together constitute a regression suite for a given design under test (DUT). Each simulation test-run often involves a DUT start-up phase responsible for performing initialization functions that bring the DUT into a state from which specific operations can be executed. For example, reset, link training, and/or register configuration can be performed to bring the DUT into a state in which traffic can be sent. Though the initialization process is often applicable to large subsets of the regression suite, existing verification practices do not take advantage of the commonality between runs. Thus, the same start-up phases are executed over and over for every test. This consumes valuable time and resources while contributing little, if anything, towards coverage. Moreover, when a test fails during a regression, the debug session must go through the same start-up process yet again, with significant impact on debug cycle efficiency.
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.

Marat Teplitsky is a member of Specman R&D at Cadence since 2005. He leads the development of the IntelliGen constraint solver and in 2011 also assumed the responsibility on the Specman Advanced Option package. He holds a B.Sc. in computer engineering from Bar-Ilan University and nowadays is completing his M.Sc. in Electrical Engineering in Tel-Aviv University, where he focuses on distributed algorithms research.