@inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Efficient Verification of Timed Automata using BDDs}, series = {FMICS 2001, Formal methods for industrial critical systems, proceedings, International workshop on formal methods for industrial critical systems 6, 16 - 17 July 2001, Paris}, booktitle = {FMICS 2001, Formal methods for industrial critical systems, proceedings, International workshop on formal methods for industrial critical systems 6, 16 - 17 July 2001, Paris}, editor = {Ultes-Nitsche, Ulrich and Gnesi, Stefania}, publisher = {INRIA}, address = {Rocquencourt}, isbn = {2-7261-1187-4}, pages = {95 -- 113}, language = {en} } @inproceedings{BeyerLewerentzNoack, author = {Beyer, Dirk and Lewerentz, Claus and Noack, Andreas}, title = {Rabbit: A Tool for BDD-based Verification of Real-Time Systems}, series = {Computer aided verification, 15th international conference, proceedings, CAV 2003, Boulder, CO, USA, July 8 - 12, 2003}, booktitle = {Computer aided verification, 15th international conference, proceedings, CAV 2003, Boulder, CO, USA, July 8 - 12, 2003}, editor = {Hunt, Warren A.}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-40524-0}, pages = {122 -- 125}, abstract = {This paper gives a short overview of a model checking tool for real-time systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data structure BDD. Good variable orderings for the BDDs are computed from the modular structure of the model and an estimate of the BDD size. This leads to a significant performance improvement compared to the tool RED and the BDD-based version of Kronos.}, language = {en} } @techreport{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {A Comparative Study of Decision Diagrams for Real-Time Verification}, publisher = {BTU, Institut f{\"u}r Informatik}, address = {Cottbus}, pages = {13}, abstract = {In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present empirical and analytical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they explain the empirical results. Secondly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. Thirdly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-sized CDDs if they use better variable orders, as the BDD-based tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values.}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?}, series = {Formal techniques for networked and distributed systems - FORTE 2003, 23rd IFIP WG 6.1, international conference, Berlin, Germany, September 29 - October 2, 2003, proceedings}, booktitle = {Formal techniques for networked and distributed systems - FORTE 2003, 23rd IFIP WG 6.1, international conference, Berlin, Germany, September 29 - October 2, 2003, proceedings}, editor = {K{\"o}nig, Hartmut}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-20175-0}, pages = {193 -- 208}, abstract = {In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present analytical and empirical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. This is the first evidence that CDDs can grow only polynomially for models with non-trivial state space explosion. Secondly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-size CDDs if they use better variable orders, as the BDD-based tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values.}, language = {en} } @inproceedings{BeyerNoackLewerentz, author = {Beyer, Dirk and Noack, Andreas and Lewerentz, Claus}, title = {Simple and Efficient Relational Querying of Software Structures}, series = {Proceedings, 10th Working Conference on Reverse Engineering, WCRE 2003, Victoria, B.C., Canada, 13 - 16 November 2003}, booktitle = {Proceedings, 10th Working Conference on Reverse Engineering, WCRE 2003, Victoria, B.C., Canada, 13 - 16 November 2003}, publisher = {IEEE Computer Society}, address = {Los Alamitos, Calif. [u.a.]}, isbn = {0-7695-2027-8}, pages = {216 -- 225}, abstract = {Abstract. Many analyses of software systems can be formalized as relational queries, for example the detection of design patterns, of patterns of problematic design, of code clones, of dead code, and of differences between the as-built and the as-designed architecture. This paper describes the concepts of CrocoPat, a tool for querying and manipulating relations. CrocoPat is easy to use, because of its simple query and manipulation language based on predicate calculus, and its simple file format for relations. CrocoPat is efficient, because it internally represents relations as binary decision diagrams, a data structure that is well-known as a compact representation of large relations in computer-aided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but n-ary relations.}, language = {en} } @inproceedings{Noack, author = {Noack, Andreas}, title = {An Energy Model for Visual Graph Clustering}, series = {Graph Drawing, 11th International Symposium, GD 2003, Perugia, Italy, Sep. 21 - 24, 2003}, booktitle = {Graph Drawing, 11th International Symposium, GD 2003, Perugia, Italy, Sep. 21 - 24, 2003}, editor = {Liotta, Guiseppe}, publisher = {Springer Verlag}, address = {Berlin [u.a.]}, isbn = {3-540-20831-3}, pages = {425 -- 436}, abstract = {We introduce an energy model whose minimum energy drawings reveal the clusters of the drawn graph. Here a cluster is a set of nodes with many internal edges and few edges to nodes outside the set. The drawings of the best-known force and energy models do not clearly show clusters for graphs whose diameter is small relative to the number of nodes. We formally characterize the minimum energy drawings of our energy model. This characterization shows in what sense the drawings separate clusters, and how the distance of separated clusters to the other nodes can be interpreted}, language = {en} } @techreport{Noack, author = {Noack, Andreas}, title = {Energy Models for Drawing Clustered Small-World Graphs}, publisher = {Inst. of Computer Science}, address = {Cottbus}, pages = {33}, abstract = {We introduce energy models for drawing clustered small-world graphs. Clustered means that there exist (probably unknown) sets of nodes with many edges between nodes of the same set and few edges to nodes outside the set. Small-world means that the graph-theoretic distances between nodes are small relative to the number of nodes. Previous force or energy models do not produce satisfactory results for such graphs. In drawings that have minimum energy with respect to our new energy models, different clusters are clearly separated and have interpretable distances.We formally characterize the minimum energy drawings of our new energy mod\%ADels and of a class of energy models that contains among others the well-known Fruchterman-Reingold model. These characterizations show 1) in what sense the minimum energy drawings of these energy models fulfill requirements like small, uniform edge lengths, well-distributed nodes, or separated clusters, and 2) what properties of the drawn graph can be inferred from the drawings}, language = {en} } @incollection{LewerentzNoack, author = {Lewerentz, Claus and Noack, Andreas}, title = {CrocoCosmos - 3D Visualization of Large Object-Oriented Programs}, series = {Graph drawing software}, booktitle = {Graph drawing software}, editor = {J{\"u}nger, Michael and Mutzel, Petra}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-00881-0}, pages = {279 -- 297}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Clustering Software Artifacts Based on Frequent Common Changes}, series = {Proceedings, 13th International Workshop on Program Comprehension, IWPC 2005, 15 - 16 May 2005, St. Louis, Missouri}, booktitle = {Proceedings, 13th International Workshop on Program Comprehension, IWPC 2005, 15 - 16 May 2005, St. Louis, Missouri}, publisher = {IEEE Computer Society}, address = {Los Alamitos, Calif. [u.a.]}, isbn = {0-7695-2254-8}, pages = {259 -- 268}, language = {en} } @inproceedings{NoackLewerentz, author = {Noack, Andreas and Lewerentz, Claus}, title = {Energy-Based Clustering of Graphs with Nonuniform Degrees}, language = {en} } @inproceedings{NoackLewerentz, author = {Noack, Andreas and Lewerentz, Claus}, title = {A Space of Layout Styles for Hierarchical Graph Models of Software Systems}, series = {Proceedings, SoftVis '05, ACM Symposium on Software Visualization, St. Louis, Missouri, May 14 - 15, 2005}, booktitle = {Proceedings, SoftVis '05, ACM Symposium on Software Visualization, St. Louis, Missouri, May 14 - 15, 2005}, publisher = {Association for Computing Machinery}, address = {New York, NY}, isbn = {1-59593-073-6}, pages = {155 -- 213}, language = {en} } @misc{BalzerNoackDeussenetal., author = {Balzer, Michael and Noack, Andreas and Deussen, Oliver and Lewerentz, Claus}, title = {Software Landscapes: Visualizing the Structure of Large Software Systems}, series = {VisSym 2004, Symposium on Visualization, Konstanz, Germany, May 19- 21, 2004}, journal = {VisSym 2004, Symposium on Visualization, Konstanz, Germany, May 19- 21, 2004}, publisher = {Eurographics Association}, address = {Aire-la-Ville}, pages = {261 -- 266}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {BDD-basierte Verifikation von Realzeit-Systemen}, language = {de} } @article{BeyerNoackLewerentz, author = {Beyer, Dirk and Noack, Andreas and Lewerentz, Claus}, title = {Efficient Relational Calculation for Software Analysis}, language = {en} } @techreport{Noack, author = {Noack, Andreas}, title = {Visual Clustering of Graphs with Nonuniform Degrees}, publisher = {Inst. of Computer Science}, address = {Cottbus}, pages = {16 Bl.}, language = {en} } @phdthesis{Noack, author = {Noack, Andreas}, title = {Unified quality measures for clusterings, layouts, and orderings of graphs, and their application as software design criteria}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-4046}, language = {en} } @misc{Noack, author = {Noack, Andreas}, title = {Modularity clustering is force-directed layout}, series = {Physical Review : E}, volume = {79}, journal = {Physical Review : E}, issn = {1550-2376}, pages = {026102}, abstract = {Two natural and widely used representations for the community structure of networks are clusterings,which partition the vertex set into disjoint subsets, and layouts, which assign the vertices to positions in a metric space. This paper unifies prominent characterizations of layout quality and clustering quality, by showing that energy models of pairwise attraction and repulsion subsume Newman and Girvan's modularity measure. Layouts with optimal energy are relaxations of, and are thus consistent with, clusterings with optimal modularity, which isof practical relevance because both representations are complementary and often used together.}, language = {en} } @inproceedings{NoackRotta, author = {Noack, Andreas and Rotta, Randolf}, title = {Multi-level Algorithms for Modularity Clustering}, abstract = {Modularity is a widely used quality measure for graph clusterings. Its exact maximization is prohibitively expensive for large graphs. Popular heuristics progressively merge clusters starting from singletons (coarsening), and optionally improve the resulting clustering by moving vertices between clusters (refinement). This paper experimentally compares existing and new heuristics of this type with respect to their effectiveness (achieved modularity) and runtime. For coarsening, it turns out that the most widely used criterion for merging clusters (modularity increase) is outperformed by other simple criteria, and that a recent multi-step algorithm is no improvement over simple single-step coarsening for these criteria. For refinement, a new multi-level algorithm produces significantly better clusterings than conventional single-level algorithms. A comparison with published benchmark results and algorithm implementations shows that combinations of coarsening and multi-level refinement are competitive with the best algorithms in the literature.}, language = {en} } @misc{RottaNoack, author = {Rotta, Randolf and Noack, Andreas}, title = {Multilevel local search algorithms for modularity clusterin}, series = {Journal on Experimental Algorithmics}, volume = {16}, journal = {Journal on Experimental Algorithmics}, number = {2}, issn = {1084-6654}, language = {en} }