Abstracts

  • Shahar Maoz and Yaniv Sa'ar. Two-Way Traceability and Conflict Debugging for AspectLTL Programs.
    2012. In Proc. 11th International Conference on Aspect Oriented Software Development, To appear.

    Abstract: Tracing program actions back to the concerns that have caused them and blaming specific code artifacts for concern interference are known challenges of AOP and related advanced modularity paradigms. In this work we address these challenges in the context of AspectLTL, a temporal- logic based language for the specification and implementation of crosscutting concerns, which has a composition and synthesis-based weaving process whose output is a correct- by-construction executable artifact. When a specification is realizable, we provide two-way traceability information that links each allowed or forbidden transition in the generated program with the aspects that have justified its presence or elimination. When a specification is unrealizable, we provide an interactive game proof that demonstrates conflicts that should be fixed. The techniques are implemented and demonstrated using running examples.

  • Shahar Maoz and Yaniv Sa'ar. AspectLTL: An Aspect Language for LTL Specifications.
    2011. In Proc. 10th International Conference on Aspect Oriented Software Development, pages 19-30, ACM.

    Abstract: We present AspectLTL, a temporal-logic based language for the specification and implementation of crosscutting concerns. AspectLTL enables the modular declarative specification of expressive concerns, covering the addition of new behaviors, as well as the specification of safety and liveness properties. Moreover, given an AspectLTL specification, consisting of a base system and a set of aspects, we provide AspectLTL with a composition and synthesis-based weaving process, whose output is a correct-by-construction executable artifact. The language is supported by a prototype tool and is demonstrated using a running example.

  • Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of Reactive(1) Designs.
    2011. Journal of Computer System and Science.

    Abstract: We address the problem of automatically synthesizing digital designs from linear- time specifications. We consider various classes of specifications that can be synthesized with effort cubic in the number of states of the reactive system, where we measure effort in symbolic steps.

    The synthesis algorithm is based on a novel type of game called General Reactivity of rank 1 (GR(1)), with a winning condition of the form
    (G F p1 /\ ... /\ G F pm) → (G F q1 /\ ... /\ G F qn)
    where each p_i and q_i is a Boolean combination of atomic propositions. We show symbolic algorithms to solve this game, to build a winning strategy and several ways to optimize the winning strategy and to extract a system from it. We also show how to use GR(1) games to solve the synthesis of LTL specifications in many interesting cases.

    As empirical evidence to the generality and efficiency of our approach we include two significant case studies. We describe the formal specifications and the synthesis process applied to a buffer controller and to a bus arbiter. Both are realistic industrial hardware specifications of modest size.

  • Ittai Balaban, Amir Pnueli, Yaniv Sa’ar, and Lenore D. Zuck. Verification of Multi-Linked Heaps.
    2011. Journal of Computer System and Science.

    Abstract: We define the class of single-parent heap systems, which rely on a singly-linked heap in order to model destructive updates on tree structures. This encoding has the advantage of relying on a relatively simple theory of linked lists in order to support abstraction computation. To facilitate the application of this encoding, we provide a program transformation that, given a program operating on a multi-linked heap without sharing, transforms it into one over a single-parent heap. It is then possible to apply shape analysis by predicate and ranking abstraction. The technique has been successfully applied on examples with lists (reversal and bubble sort) and trees with of fixed arity (balancing of, and insertion into, a binary sort tree).

  • Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar, Lenore D. Zuck , and Katya I. Kisyova. Parallelizing A Symbolic Compositional Model-Checking Algorithm.
    2010. In Proc. 6th International Haifa Verification Conference, volume 6504 of Lecture Notes in Computer Science, pages 46-59. © Springer-Verlag.

    Abstract: The central thesis explored in this paper is that parallel model checking is easily achieved through compositional methods. This may strike the reader as being self-evident. Nevertheless, it does not appear to have been considered before. The justification comes from the following observations: (1) the efficacy of a parallel program is inversely proportional to the amount of synchronization and communication across processors, and (2) compositional methods break up the analysis into nearly-independent parts; in each part, a program component is analyzed with limited knowledge of the internal state of other components. For loosely coupled programs, therefore, one may expect compositional methods to work well, and to further benefit from parallelization.

  • Ariel Cohen, Kedar S. Namjoshi, and Yaniv Sa'ar. A Dash of Fairness for Compositional Reasoning.
    2010. In Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 543-557. © Springer-Verlag.

    Abstract: Proofs of progress properties often require fairness assumptions. Directly incorporating global fairness assumptions in a compositional method is difficult, given the local flavor of such reasoning. We present a fully automated local reasoning algorithm which handles fairness assumptions through a process of iterative refinement. Refinement strengthens local proofs by the addition of auxiliary shared variables which expose internal process state; it is needed as local reasoning is inherently incomplete. Experiments demonstrate that the new algorithm shows significant improvement over standard model checking.

  • Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck. JTLV: A Framework for Developing Verification Algorithms.
    2010. In Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 171-174. © Springer-Verlag.

    Abstract: JTLV is a computer-aided verification scripting environment offering state-of-the-art Integrated Developer Environment for algorithmic verification applications. J TLV may be viewed as a new, and much enhanced TLV (A. Pnueli and E. Shahar. – CAV 1996) , with Java (rather than TLV-basic) as the scripting language. JTLV attaches its internal parsers as an Eclipse editor, and facilitates a rich, common, and abstract verification developer environment that is implemented as an Eclipse plugin.

    Through the high-level API the developer can load into the Java code several (SMV-like) modules representing programs and specification files, and directly access their components. The developer can also procedurally construct such modules and specifications, which enables loading various data structures (e.g., statecharts, LSCs, and automata) and compile them into modules.

  • Ariel Cohen, Kedar S. Namjoshi, and Yaniv Sa'ar. SPLIT: A Compositional LTL Verifier.
    2010. In Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 558-561. © Springer-Verlag.

    Abstract: SPLIT is a compositional verifier for safety and general LTL properties of shared-variable, multi-threaded programs. The foundation is a computation of compact local invariants, one for each process, which are used for constructing a proof for the property. An automatic refinement procedure gradually exposes more local information, until a decisive result (proof/disproof) is obtained.

  • Ariel Cohen, Kedar S. Namjoshi, and Yaniv Sa'ar, Lenore D. Zuck , and Katya I. Kisyova. Model Checking in Bits and Pieces.
    2010. Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2).

    Abstract: The central thesis explored in this paper is that parallel model checking is easily achieved through compositional methods. This may strike the reader as being self-evident. Nevertheless, it does not appear to have been considered before. The justification comes from the following observations: (1) the efficacy of a parallel program is inversely proportional to the amount of synchronization and communication across processors, and (2) compositional methods break up the analysis into nearly-independent parts; in each part, a program component is analyzed with limited knowledge of the internal state of other components. For loosely coupled programs, therefore, one may expect compositional methods to work well, and to further benefit from parallelization.

  • Amir Pnueli, and Yaniv Sa'ar. All You Need is Compassion.
    2008. In Proc. 9th International Conference on Verification, Model Checking and Abstract Interpretation, volume 4905 of Lecture Notes in Computer Science, pages 233-247. © Springer-Verlag.

    Abstract: The paper presents a new deductive rule for verifying response properties under the assumption of compassion (strong fairness) requirements. It improves on previous rules in that the premises of the new rule are all first order. We prove that the rule is sound, and present a constructive completeness proof for the case of finite-state systems. For the general case, we present a sketch of a relative completeness proof. We report about the implementation of the rule in PVS and illustrate its application on some simple but non-trivial examples.

  • Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of Reactive(1) Designs.
    2006. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380. © Springer-Verlag.

    Abstract: We address the problem of automatically synthesizing digital designs from linear- time specifications. We consider various classes of specifications that can be synthesized with effort cubic in the number of states of the reactive system, where we measure effort in symbolic steps.

    The synthesis algorithm is based on a novel type of game called General Reactivity of rank 1 (GR(1)), with a winning condition of the form
    (G F p1 /\ ... /\ G F pm) → (G F q1 /\ ... /\ G F qn)
    where each p_i and q_i is a Boolean combination of atomic propositions. We show symbolic algorithms to solve this game, to build a winning strategy and several ways to optimize the winning strategy and to extract a system from it. We also show how to use GR(1) games to solve the synthesis of LTL specifications in many interesting cases.

    As empirical evidence to the generality and efficiency of our approach we include two significant case studies. We describe the formal specifications and the synthesis process applied to a buffer controller and to a bus arbiter. Both are realistic industrial hardware specifications of modest size.

  • Yaniv Sa'ar. Algorithmic Methods for Formal Verification (Ph.D. Dissertation) (slides).

    Abstract: In the past several decades both industry and academic communities have developed a variety of tools and methodologies to address verification, namely whether a given program meets its specifications. Most verification tools consist of computational model that represents the system implementation, and specification language that represents the expectation from the implementation. Usually, these tools are designed to serve as verifiers where to implement all but the simplest algorithm, a developer is assumed to be intimately familiar with the internal structure and implementation details of the system.

    The work reported here focuses on the lack of an adequate environment to support the verification process. To leverage the developer's skills we present JTLV ([PSZ10]), a new state-of-the-art Integrated Developer Environment (IDE) for developing verification algorithms. We demonstrate the power of JTLV by considering several active research domains of verification; the problem of synthesis, the framework of compositional reasoning, as well as other interesting settings.

    For synthesis – the process of automatically extracting code from high-level specifications – we present a solution to the GR(1) fragment of LTL ([PPS06,BJPPS]), as well as introduce AspectLTL – a new temporal-logic based programming language ([MS11]). We conclude that the high complexity established for LTL synthesis does not necessarily identify it as intractable, and that we can use the GR(1) fragment to introduce a declarative style programming language.

    For compositional reasoning, we present a new algorithm that exploits the benefit of a multi-core system ([CNSZK10a]), a new algorithm that can handle strong fairness requirements locally ([CNS10a]), and a fully automated implementation of our compositional framework ([CNS10b]). We conclude that compositional reasoning is a promising approach to ameliorate the state explosion problem.

    Finally, we study several other interesting settings that includes automated reasoning on programs that perform destructive updating on dynamically allocated storage ([BPSZ]), an extension to support two-way traceability and conflict debugging of AspectLTL programs, and a slightly different approach in which we tackle the treatment of compassion requirements inherently by introducing a new deductive rule, rather than a mechanical solution ([PS08]). We conclude that there are many interesting research domains of verification yet to be explored.

    Thus we demonstrate the power of an advanced environment for developers by using JTLV for a variety of applications, including synthesis, program language engineering, treatment of fairness properties, heap analysis, multi-threading, and compositional reasoning.

In preparation

  • Shahar Maoz and Yaniv Sa'ar. Open Scenarios: Semantics and Synthesis.
    Submitted.

    Abstract: Reactive systems behavior is best described in an assume-guarantee style specification: a system guarantees certain prescribed behavior provided that its environment follows certain given assumptions. Scenario-based languages, such as live sequence charts (LSC), have been used to specify reactive systems behavior in a visual, modular, intuitive way. However, they have not yet provided full support for assume- guarantee style specifications.

    In this paper we extend LSC syntax and semantics with support for environment assumptions. Moreover, the semantics of the extended language is given in the form of a GR(1) formula, and thus enables the efficient synthesis of a correct- by-construction controller. The work is implemented inside the PlayGo IDE, developed at the Weizmann Institute of Science, and is demonstrated in this paper using running examples.

  • Shahar Maoz and Yaniv Sa'ar. Counter Play-Out: Debugging Conflicts in Scenario-Based Specifications.
    Submitted.

    Abstract: The scenario-based approach to the specification and execution of reactive systems has attracted much research efforts in recent years. Specifically, we focus on the language of live sequence charts (LSC) and its play-out mechanisms. While the problem of synthesizing a controller from a scenario-based specification given in LSC has been studied extensively, no work has yet addressed the case where the specification is unrealizable and a controller cannot be synthesized.

    In this paper we present counter play-out, an interactive debugging method to handle conflicts in scenario-based specifications. When an unrealizable specification is identified, we generate a controller that plays the role of the environment and lets the engineer play the role of the system; during execution, the former chooses environment’s moves such that the latter is forced to eventually fail in satisfying the system’s requirements. Counter play-out is based on counter strategies, computed by solving a Rabin game. We have implemented counter play-out and demonstrate it in this paper using a running example.