Software and Computational Systems Lab

Publications of year 2006

1. Dirk Beyer and Ahmed E. Hassan. Animated Visualization of Software History using Evolution Storyboards. In Proceedings of the 13th IEEE Working Conference on Reverse Engineering (WCRE 2006, Benevento, October 23-27), pages 199-208, 2006. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/WCRE.2006.14 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF
   Abstract

   The understanding of the structure of a software system can be improved by analyzing the system's evolution during development. Visualizations of software history that provide only static views do not capture the dynamic nature of software evolution. We present a new visualization technique, the Evolution Storyboard, which provides dynamic views of the evolution of a software's structure. An evolution storyboard consists of a sequence of animated panels, which highlight the structural changes in the system; one panel for each considered time period. Using storyboards, engineers can spot good design, signs of structural decay, or the spread of cross cutting concerns in the code. We implemented our concepts in a tool, which automatically extracts software dependency graphs from version control repositories and computes storyboards based on panels for different time periods. For applying our approach in practice, we provide a step by step guide that others can follow along the storyboard visualizations, in order to study the evolution of large systems. We have applied our method to several large open source software systems. In this paper, we demonstrate that our method provides additional information (compared to static views) on the ArgoUML project, an open source UML modeling tool.
   BibTeX Entry

   @inproceedings{WCRE06, author = {Dirk Beyer and Ahmed E.~Hassan}, title = {Animated Visualization of Software History using Evolution Storyboards}, booktitle = {Proceedings of the 13th IEEE Working Conference on Reverse Engineering (WCRE~2006, Benevento, October 23-27)}, pages = {199-208}, year = {2006}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {1095-1350}, doi = {10.1109/WCRE.2006.14}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2006-WCRE.Animated_Visualization_of_Software_History_using_Evolution_Storyboards.pdf}, abstract = {The understanding of the structure of a software system can be improved by analyzing the system's evolution during development. Visualizations of software history that provide only static views do not capture the dynamic nature of software evolution. We present a new visualization technique, the Evolution Storyboard, which provides dynamic views of the evolution of a software's structure. An evolution storyboard consists of a sequence of animated panels, which highlight the structural changes in the system; one panel for each considered time period. Using storyboards, engineers can spot good design, signs of structural decay, or the spread of cross cutting concerns in the code. We implemented our concepts in a tool, which automatically extracts software dependency graphs from version control repositories and computes storyboards based on panels for different time periods. For applying our approach in practice, we provide a step by step guide that others can follow along the storyboard visualizations, in order to study the evolution of large systems. We have applied our method to several large open source software systems. In this paper, we demonstrate that our method provides additional information (compared to static views) on the ArgoUML project, an open source UML modeling tool.}, keyword = {Structural Analysis and Comprehension}, annote = {}, }
2. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In T. Ball and R.B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006, Seattle, WA, August 17-20), LNCS 4144, pages 532-546, 2006. Springer-Verlag, Heidelberg. doi:10.1007/11817963_48 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.
   BibTeX Entry

   @inproceedings{CAV06, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz}, title = {Lazy Shape Analysis}, booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification (CAV~2006, Seattle, WA, August 17-20)}, editor = {T.~Ball and R.B.~Jones}, pages = {532-546}, year = {2006}, series = {LNCS~4144}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-37406-X}, doi = {10.1007/11817963_48}, sha256 = {83aadf3fff8dfe5462691e635eb3f21fda3bd09638cf78a94d71ca87efbd5390}, url = {http://www.sosy-lab.org/~dbeyer/blast_sa/}, pdf = {https://www.sosy-lab.org/research/pub/2006-CAV.Lazy_Shape_Analysis.pdf}, abstract = {Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.}, keyword = {BLAST,Software Model Checking}, annote = {An extended version of this paper appeared in Proc. Dagstuhl Seminar 06081, IBFI Schloss Dagstuhl, 2006: <BR> <a href="http://drops.dagstuhl.de/portals/06081/"> http://drops.dagstuhl.de/portals/06081/</a> <BR> Supplementary material: <a href="http://www.sosy-lab.org/~dbeyer/blast_sa/"> http://www.sosy-lab.org/~dbeyer/blast_sa/</a>}, }
   Additional Infos

   An extended version of this paper appeared in Proc. Dagstuhl Seminar 06081, IBFI Schloss Dagstuhl, 2006:
   http://drops.dagstuhl.de/portals/06081/
   Supplementary material: http://www.sosy-lab.org/~dbeyer/blast_sa/
3. Dirk Beyer and Ahmed E. Hassan. Evolution Storyboards: Visualization of Software Structure Dynamics. In Proceedings of the 14th IEEE International Conference on Program Comprehension (ICPC 2006, Athens, June 14-16), pages 248-251, 2006. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICPC.2006.21 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF
   Abstract

   Large software systems have a rich development history. Mining certain aspects of this rich history can reveal interesting insights into the system and its structure. Previous approaches to visualize the evolution of software systems provide static views. These static views often do not fully capture the dynamic nature of evolution. We introduce the Evolution Storyboard, a visualization which provides dynamic views of the evolution of a software's structure. Our tool implementation takes as input a series of software graphs, e.g., call graphs or co-change graphs, and automatically generates an evolution storyboard. To illustrate the concept, we present a storyboard for PostgreSQL, as a representative example for large open source systems. Evolution storyboards help to understand a system's structure and to reveal its possible decay over time. The storyboard highlights important changes in the structure during the lifetime of a software system, and how artifacts changed their dependencies over time.
   BibTeX Entry

   @inproceedings{ICPC06, author = {Dirk Beyer and Ahmed E.~Hassan}, title = {Evolution Storyboards: Visualization of Software Structure Dynamics}, booktitle = {Proceedings of the 14th IEEE International Conference on Program Comprehension (ICPC~2006, Athens, June 14-16)}, pages = {248-251}, year = {2006}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-2601-2}, doi = {10.1109/ICPC.2006.21}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2006-ICPC.Evolution_Storyboards_Visualization_of_Software_Structure_Dynamics.pdf}, abstract = {Large software systems have a rich development history. Mining certain aspects of this rich history can reveal interesting insights into the system and its structure. Previous approaches to visualize the evolution of software systems provide static views. These static views often do not fully capture the dynamic nature of evolution. We introduce the Evolution Storyboard, a visualization which provides dynamic views of the evolution of a software's structure. Our tool implementation takes as input a series of software graphs, e.g., call graphs or co-change graphs, and automatically generates an evolution storyboard. To illustrate the concept, we present a storyboard for PostgreSQL, as a representative example for large open source systems. Evolution storyboards help to understand a system's structure and to reveal its possible decay over time. The storyboard highlights important changes in the structure during the lifetime of a software system, and how artifacts changed their dependencies over time.}, keyword = {Structural Analysis and Comprehension}, annote = {}, }
4. Dirk Beyer. Relational Programming with CrocoPat. In Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE 2006, Shanghai, May 20-28), pages 807-810, 2006. ACM Press, New York (NY). doi:10.1145/1134285.1134420 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Supplement
   Abstract

   Many structural analyses of software systems are naturally formalized as relational queries, for example, the detection of design patterns, patterns of problematic design, code clones, dead code, and differences between the as-built and the as-designed architecture. This paper describes CrocoPat, an application-independent tool for relational programming. Through its efficiency and its expressive language, CrocoPat enables practically important analyses of real-world software systems that are not possible with other graph analysis tools, in particular analyses that involve transitive closures and the detection of patterns in graphs. The language is easy to use, because it is based on the well-known first-order predicate logic. The tool is easy to integrate into other software systems, because it is a small command-line tool that uses a simple text format for input and output of relations.
   BibTeX Entry

   @inproceedings{ICSE06b, author = {Dirk Beyer}, title = {Relational Programming with {{\sc CrocoPat}}}, booktitle = {Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE~2006, Shanghai, May 20-28)}, pages = {807-810}, year = {2006}, publisher = {ACM Press, New York~(NY)}, isbn = {1-59593-375-1}, doi = {10.1145/1134285.1134420}, url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/}, pdf = {https://www.sosy-lab.org/research/pub/2006-ICSE.Relational_Programming_with_CrocoPat.pdf}, abstract = {Many structural analyses of software systems are naturally formalized as relational queries, for example, the detection of design patterns, patterns of problematic design, code clones, dead code, and differences between the as-built and the as-designed architecture. This paper describes CrocoPat, an application-independent tool for relational programming. Through its efficiency and its expressive language, CrocoPat enables practically important analyses of real-world software systems that are not possible with other graph analysis tools, in particular analyses that involve transitive closures and the detection of patterns in graphs. The language is easy to use, because it is based on the well-known first-order predicate logic. The tool is easy to integrate into other software systems, because it is a small command-line tool that uses a simple text format for input and output of relations.}, keyword = {Structural Analysis and Comprehension}, annote = {CrocoPat is available at: <a href="http://www.sosy-lab.org/~dbeyer/CrocoPat/"> http://www.sosy-lab.org/~dbeyer/CrocoPat/</a>}, }
   Additional Infos

   CrocoPat is available at: http://www.sosy-lab.org/~dbeyer/CrocoPat/
5. Basil Becker, Dirk Beyer, Holger Giese, Florian Klein, and Daniela Schilling. Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE 2006, Shanghai, May 20-28), pages 72-81, 2006. ACM Press, New York (NY). doi:10.1145/1134285.1134297 Keyword(s): Software Model Checking Publisher's Version PDF
   Abstract

   The next generation of networked mechatronic systems will be characterized by complex coordination and structural adaptation at run-time. Crucial safety properties have to be guaranteed for all potential structural configurations. Testing cannot provide safety guarantees, while current model checking and theorem proving techniques do not scale for such systems. We present a verification technique for arbitrarily large multi-agent systems from the mechatronic domain, featuring complex coordination and structural adaptation. We overcome the limitations of existing techniques by exploiting the local character of structural safety properties. The system state is modeled as a graph, system transitions are modeled as rule applications in a graph transformation system, and safety properties of the system are encoded as inductive invariants (permitting the verification of infinite state systems). We developed a symbolic verification procedure that allows us to perform the computation on an efficient BDD-based graph manipulation engine, and we report performance results for several examples.
   BibTeX Entry

   @inproceedings{ICSE06a, author = {Basil Becker and Dirk Beyer and Holger Giese and Florian Klein and Daniela Schilling}, title = {Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation}, booktitle = {Proceedings of the 28th ACM/IEEE International Conference on Software Engineering (ICSE~2006, Shanghai, May 20-28)}, pages = {72-81}, year = {2006}, publisher = {ACM Press, New York~(NY)}, isbn = {1-59593-375-1}, doi = {10.1145/1134285.1134297}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2006-ICSE.Symbolic_Invariant_Verification_for_Systems_with_Dynamic_Structural_Adaptation.pdf}, abstract = {The next generation of networked mechatronic systems will be characterized by complex coordination and structural adaptation at run-time. Crucial safety properties have to be guaranteed for all potential structural configurations. Testing cannot provide safety guarantees, while current model checking and theorem proving techniques do not scale for such systems. We present a verification technique for arbitrarily large multi-agent systems from the mechatronic domain, featuring complex coordination and structural adaptation. We overcome the limitations of existing techniques by exploiting the local character of structural safety properties. The system state is modeled as a graph, system transitions are modeled as rule applications in a graph transformation system, and safety properties of the system are encoded as inductive invariants (permitting the verification of infinite state systems). We developed a symbolic verification procedure that allows us to perform the computation on an efficient BDD-based graph manipulation engine, and we report performance results for several examples.}, keyword = {Software Model Checking}, annote = {}, }
6. Alain Wegmann, Lam-Son Le, Lotfi Hussami, and Dirk Beyer. A Tool for Verified Design using Alloy for Specification and CrocoPat for Verification. In D. Jackson and P. Zave, editors, Proceedings of the First Alloy Workshop (ALLOY 2006, Portland, OR, November 6), 2006. Keyword(s): Structural Analysis and Comprehension PDF
   Abstract

   The context of our work is a project that focuses on methods and tools for modeling enterprise architectures. An enterprise architecture model represents the structure of an enterprise across multiple levels, from the markets in which it operates down to the implementation of the technical systems that support its operation. These models are based on an ontology that defines the model elements and their relations. In this paper, we describe an efficient method to fully automatically verify the design that our modeling tool manages. We specify the ontology in Alloy, and use the efficient interpreter for relational programs CrocoPat to verify that the design fulfills all constraints specified in the ontology. Technically, we transform all constraints from Alloy into a relational program in CrocoPat's programming language. Then, we execute the relational program and feed it with a relational representation of the design as input, in order to check that the design element instances fulfill all constraints of the Alloy representation of the ontology. We also present the current limitations of our approach and how -by overcoming these limitations- we can develop an Alloy-based parameterized modeling tool.
   BibTeX Entry

   @inproceedings{ALLOY06, author = {Alain Wegmann and Lam-Son Le and Lotfi Hussami and Dirk Beyer}, title = {A Tool for Verified Design using {Alloy} for Specification and {CrocoPat} for Verification}, booktitle = {Proceedings of the First Alloy Workshop (ALLOY~2006, Portland, OR, November 6)}, editor = {D.~Jackson and P.~Zave}, pages = {}, year = {2006}, publisher = {}, isbn = {}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2006-ALLOY.A_Tool_for_Verified_Design_using_Alloy_for_Specification_and_CrocoPat_for_Verification.pdf}, abstract = {The context of our work is a project that focuses on methods and tools for modeling enterprise architectures. An enterprise architecture model represents the structure of an enterprise across multiple levels, from the markets in which it operates down to the implementation of the technical systems that support its operation. These models are based on an ontology that defines the model elements and their relations. In this paper, we describe an efficient method to fully automatically verify the design that our modeling tool manages. We specify the ontology in Alloy, and use the efficient interpreter for relational programs CrocoPat to verify that the design fulfills all constraints specified in the ontology. Technically, we transform all constraints from Alloy into a relational program in CrocoPat's programming language. Then, we execute the relational program and feed it with a relational representation of the design as input, in order to check that the design element instances fulfill all constraints of the Alloy representation of the ontology. We also present the current limitations of our approach and how -by overcoming these limitations- we can develop an Alloy-based parameterized modeling tool.}, keyword = {Structural Analysis and Comprehension}, doinone = {DOI not available}, }
7. Dirk Beyer. Co-Change Visualization Applied to PostgreSQL and ArgoUML. In Proceedings of the Third International Workshop on Mining Software Repositories (MSR 2006, Shanghai, May 22-23), pages 165-166, 2006. ACM Press. doi:10.1145/1137983.1138023 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Supplement
   Abstract

   Co-change visualization is a method to recover the subsystem structure of a software system from the version history, based on common changes and visual clustering. This paper presents the results of applying the tool CCVisu, which implements co-change visualization, to the two open-source software systems PostgreSQL and ArgoUML. The input of the method is the co-change graph, which can be easily extracted by CCVisu from a CVS version repository. The output is a graph layout that places software artifacts that were often commonly changed at close positions, and artifacts that were rarely co-changed at distant positions. This property of the layout is due to the clustering property of the underlying energy model, which evaluates the quality of a produced layout. The layout can be displayed on the screen, or saved to a file in SVG or VRML format.
   BibTeX Entry

   @inproceedings{MSR06, author = {Dirk Beyer}, title = {Co-Change Visualization Applied to {PostgreSQL} and {ArgoUML}}, booktitle = {Proceedings of the Third International Workshop on Mining Software Repositories (MSR~2006, Shanghai, May 22-23)}, pages = {165-166}, year = {2006}, publisher = {ACM Press}, isbn = {1-59593-397-2}, doi = {10.1145/1137983.1138023}, url = {http://www.sosy-lab.org/~dbeyer/ccvisu_msr}, pdf = {https://www.sosy-lab.org/research/pub/2006-MSR.Co-Change_Visualization_Applied_to_PostgreSQL_and_ArgoUML.pdf}, abstract = {Co-change visualization is a method to recover the subsystem structure of a software system from the version history, based on common changes and visual clustering. This paper presents the results of applying the tool CCVisu, which implements co-change visualization, to the two open-source software systems PostgreSQL and ArgoUML. The input of the method is the co-change graph, which can be easily extracted by CCVisu from a CVS version repository. The output is a graph layout that places software artifacts that were often commonly changed at close positions, and artifacts that were rarely co-changed at distant positions. This property of the layout is due to the clustering property of the underlying energy model, which evaluates the quality of a produced layout. The layout can be displayed on the screen, or saved to a file in SVG or VRML format.}, keyword = {Structural Analysis and Comprehension}, annote = {}, }

1. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path Invariants. Technical report MTC-REPORT-2006-003, School of Computer and Communication Sciences (IC), Ecole Polytechnique Féd\ŕale de Lausanne (EPFL), December 2006. Keyword(s): Software Model Checking PDF Supplement
   Abstract

   The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In such schemes, the cause of a false positive is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false positive -the "spurious counterexample"- as a full-fledged program, whose control-flow graph may contain loops of the original program and represent unbounded computations. The advantages of using such path programs as counterexamples for abstraction refinement are twofold. First, we can bring the whole machinery of program analysis to bear on path programs: specifically, we use abstract interpretation in the form of constrained-based invariant generation to automatically infer invariants of path programs -so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but to remove at once all infeasible error computations that are represented by a path program. Unlike predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive invariants.
   BibTeX Entry

   @techreport{TR003-EPFL06, author = {Dirk Beyer and Thomas A.~Henzinger and Rupak Majumdar and Andrey Rybalchenko}, title = {Path Invariants}, number = {MTC-REPORT-2006-003}, year = {2006}, url = {http://infoscience.epfl.ch/search.py?recid=98452&ln=en}, pdf = {https://www.sosy-lab.org/research/pub/2006-EPFL-TR003.Path_Invariants.pdf}, abstract = {The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a new method for automated abstraction refinement, which overcomes the inherent limitations of predicate discovery schemes. In such schemes, the cause of a false positive is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false positive ---the ``spurious counterexample''--- as a full-fledged program, whose control-flow graph may contain loops of the original program and represent unbounded computations. The advantages of using such path programs as counterexamples for abstraction refinement are twofold. First, we can bring the whole machinery of program analysis to bear on path programs: specifically, we use abstract interpretation in the form of constrained-based invariant generation to automatically infer invariants of path programs ---so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but to remove at once all infeasible error computations that are represented by a path program. Unlike predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive invariants.}, keyword = {Software Model Checking}, annote = {Online: <a href="http://infoscience.epfl.ch/search.py?recid=98452&ln=en"> http://infoscience.epfl.ch/search.py?recid=98452&ln=en</a> <BR>}, institution = {School of Computer and Communication Sciences (IC), Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)}, month = {December}, }
   Additional Infos

   Online: http://infoscience.epfl.ch/search.py?recid=98452&ln=en
   
2. Dirk Beyer, Thomas A. Henzinger, and Vasu Singh. Three Algorithms for Interface Synthesis: A Comparative Study. Technical report MTC-REPORT-2006-001, School of Computer and Communication Sciences (IC), Ecole Polytechnique Féd\ŕale de Lausanne (EPFL), May 2006. Keyword(s): Interfaces for Component-Based Design, Software Model Checking PDF Supplement
   Abstract

   A temporal interface for a system component is a finite automaton that specifies the legal sequences of input events. We evaluate and compare three different algorithms for automatically extracting the temporal interface from the transition graph of a component: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the component to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant state information from the component. Since algorithms (2) and (3) have been published in different software contexts, for comparison purposes, we present the three algorithms in a uniform finite-state setting. We furthermore extend the three algorithms to construct maximally permissive interface automata, which accept all legal input sequences. While the three algorithms have similar worst-case complexities, their actual running times differ greatly depending on the component whose interface is computed. On the theoretical side, we provide families of components that exhibit exponential differences in the performance of the three algorithms. On the practical side, we evaluate the three algorithms experimentally on a variety of real world examples. Not surprisingly, the experimental evaluation confirms the theoretical expectation: learning performs best if the minimal interface automaton is small; CEGAR performs best if only few component variables are needed to prove an interface hypothesis safe and permissive; and the direct (game) algorithm outperforms both approaches if neither is the case.
   BibTeX Entry

   @techreport{TR001-EPFL06, author = {Dirk Beyer and Thomas A.~Henzinger and Vasu Singh}, title = {Three Algorithms for Interface Synthesis: A Comparative Study}, number = {MTC-REPORT-2006-001}, year = {2006}, url = {http://infoscience.epfl.ch/search.py?recid=85675&ln=en}, pdf = {https://www.sosy-lab.org/research/pub/2006-EPFL-TR001.Three_Algorithms_for_Interface_Synthesis_A_Comparative_Study.pdf}, abstract = {A temporal interface for a system component is a finite automaton that specifies the legal sequences of input events. We evaluate and compare three different algorithms for automatically extracting the temporal interface from the transition graph of a component: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the component to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant state information from the component. Since algorithms (2) and (3) have been published in different software contexts, for comparison purposes, we present the three algorithms in a uniform finite-state setting. We furthermore extend the three algorithms to construct maximally permissive interface automata, which accept all legal input sequences. While the three algorithms have similar worst-case complexities, their actual running times differ greatly depending on the component whose interface is computed. On the theoretical side, we provide families of components that exhibit exponential differences in the performance of the three algorithms. On the practical side, we evaluate the three algorithms experimentally on a variety of real world examples. Not surprisingly, the experimental evaluation confirms the theoretical expectation: learning performs best if the minimal interface automaton is small; CEGAR performs best if only few component variables are needed to prove an interface hypothesis safe and permissive; and the direct (game) algorithm outperforms both approaches if neither is the case.}, keyword = {Interfaces for Component-Based Design,Software Model Checking}, annote = {Online: <a href="http://infoscience.epfl.ch/search.py?recid=85675&ln=en"> http://infoscience.epfl.ch/search.py?recid=85675&ln=en</a> <BR>}, institution = {School of Computer and Communication Sciences (IC), Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)}, month = {May}, }
   Additional Infos

   Online: http://infoscience.epfl.ch/search.py?recid=85675&ln=en
   

1. Grégory Théoduloz. Integrating Shape Analysis into the Model Checker . Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger, 2006. Keyword(s): BLAST, Software Model Checking
   BibTeX Entry

   @misc{TheodulozShape, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Integrating Shape Analysis into the Model Checker \textsc{Blast}}, year = {2006}, pdf = {}, keyword = {BLAST,Software Model Checking}, annote = {Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize}, howpublished = {Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger}, }
   Additional Infos

   Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize