Testing constraints for real-time systems are usually verified through the satisfiability of propositional formulae. In this paper, we propose an alternative where the verification of timing constraints can be done by counting the number of truth assignments instead of boolean satisfiability. This number can also tell us how “far away” is a given specification from satisfying its safety assertion. Furthermore, specifications and safety assertions are often modified in an incremental fashion, where problematic bugs are fixed one at a time. To support this development, we propose an incremental algorithm for counting satisfiability. Our proposed incremental algorithm is optimal as no unnecessary nodes are created during each counting. This works for the class of path RTL. To illustrate this application, we show how incremental satisfiability counting can be applied to a well-known rail-road crossing example, particularly when its specification is still being refined. / Singapore-MIT Alliance (SMA)

Draft and proof of an algorithm computing incremental changes within a labeled layouted concept lattice upon insertion or removal of an attribute column in the underlying formal context. Furthermore some implementational details and mathematical background knowledge are presented. / Entwurf und Beweis eines Algorithmus zur Berechnung inkrementeller Änderungen in einem beschrifteten dargestellten Begriffsverband beim Einfügen oder Entfernen einer Merkmalsspalte im zugrundeliegenden formalen Kontext. Weiterhin sind einige Details zur Implementation sowie zum mathematischen Hintergrundwissen dargestellt.

Query systems were recently introduced as an architecture for constructing compilers, and have shown to enable fast and efficient incremental compilation, where results from previous builds is reused to accelerate future builds. With this architecture, a compiler is composed of several queries, each of which extracts a small piece of information about the source program. For example, one query might determine the type of a variable, and another the list of functions defined in some file. The dependencies of a query, which includes other queries or files on disk, are automatically recorded at runtime. With these dependencies, query systems can detect changes in their inputs and incorporate them into the final output, while reusing old results from queries which have not changed. This reduces the amount of work needed to recompile code, which saves both time and energy. We present a new parallel execution model for query systems using work-stealing, which dynamically balances the workload across multiple threads. This is facilitated by various augmentations to existing algorithms to allow concurrent operations. Furthermore, we introduce a novel data structure that accelerates incremental compilation for common use cases. We evaluated the impact of these augmentations by implementing a compiler frontend capable of parsing and type-checking the Go programming language. We demonstrate a 10x reduction in compile times using the parallel execution mode. Finally, under certain common conditions, we show a 5x reduction in incremental compile times compared to the state-of-the-art. / Query-system är en ny arkitektur som har använts för att implementera kompilatorer för programspråk och har ett fokus på att möjliggöra snabb och effektiv inkrementell kompilering. Med denna arkitektur består en kompilator flera olika mindre funktioner, som var och en svarar på en liten fråga om källprogrammet, såsom typen av en variabel eller listan över funktioner i en fil. Genom att spåra hur dessa funktioner anropar varandra, och den data de läser, kan kompilatorer upptäcka förändringar i sina indata och utföra den minimala mängd arbete som krävs för att sammanställa dessa förändringar i utdata. Detta minskar mängden arbete som behövs för att kompilera om kod, vilket sparar både tid och energi. I denna rapport presenterar vi en ny exekveringsmodell för Query-system som möjliggör parallellism med hjälp av work-stealing. Detta underlättas av flera tillägg till befintliga algoritmer som gör det möjligt att utföra alla operationer parallellt. Utöver detta introducerar vi även en ny datastruktur som gör inkrementell kompilering snabbare för många vanliga användningsområden. Vi utvärderade effekten av dessa förändringar genom att implementera ett kompilatorgränssnitt som kan analysera och verifiera korrekthet av typer Go-programmeringsspråket. Resultaten visar en 10x reduktion i kompileringstider med hjälp av parallellkörningsläget. Vi demonstrerar även 5 gånger lägre kompileringstider vid inkrementella ändringar än vad som tidigare varit möjligt.

Draft and proof of an algorithm computing incremental changes within a labeled layouted concept lattice upon insertion or removal of an attribute column in the underlying formal context. Furthermore some implementational details and mathematical background knowledge are presented.:1 Introduction 1.1 Acknowledgements 1.2 Supporting University: TU Dresden, Institute for Algebra 1.3 Supporting Corporation: SAP AG, Research Center Dresden 1.4 Research Project: CUBIST 1.5 Task Description und Structure of the Diploma Thesis I Mathematical Details 2 Fundamentals of Formal Concept Analysis 2.1 Concepts and Concept Lattice 2.2 Visualizations of Concept Lattices 2.2.1 Transitive Closure and Transitive Reduction 2.2.2 Neighborhood Relation 2.2.3 Line Diagram 2.2.4 Concept Diagram 2.2.5 Vertical Hybridization 2.2.6 Omitting the top and bottom concept node 2.2.7 Actions on Concept Diagrams 2.2.8 Metrics on Concept Diagrams 2.2.9 Heatmaps for Concept Diagrams 2.2.10 Biplots of Concept Diagrams 2.2.11 Seeds Selection 2.3 Apposition of Contexts 3 Incremental Updates for Concept Diagrams 3.1 Insertion & Removal of a single Attribute Column 3.1.1 Updating the Concepts 3.1.2 Structural Remarks 3.1.3 Updating the Order 3.1.4 Updating the Neighborhood 3.1.5 Updating the Concept Labels 3.1.6 Updating the Reducibility 3.1.7 Updating the Arrows 3.1.8 Updating the Seed Vectors 3.1.9 Complete IFOX Algorithm 3.1.10 An Example: Stepwise Construction of FCD(3) 3.2 Setting & Deleting a single cross 4 Iterative Exploration of Concept Lattices 4.1 Iceberg Lattices 4.2 Alpha Iceberg Lattices 4.3 Partly selections 4.3.1 Example with EMAGE data 4.4 Overview on Pruning & Interaction Techniques II Implementation Details 5 Requirement Analysis 5.1 Introduction 5.2 User-Level Requirements for Graphs 5.2.1 Select 5.2.2 Explore 5.2.3 Reconfigure 5.2.4 Encode 5.2.5 Abstract/Elaborate 5.2.6 Filter 5.2.7 Connect 5.2.8 Animate 5.3 Low-Level Requirements for Graphs 5.3.1 Panel 5.3.2 Node and Edge 5.3.3 Interface 5.3.4 Algorithm 5.4 Mapping of Low-Level Requirements to User-Level Requirements 5.5 Specific Visualization Requirements for Lattices 5.5.1 Lattice Zoom/Recursive Lattices/Partly Nested Lattices 5.5.2 Planarity 5.5.3 Labels 5.5.4 Selection of Ideals, Filters and Intervalls 5.5.5 Restricted Moving of Elements 5.5.6 Layout Algorithms 5.5.7 Additional Feature: Three Dimensions and Rotation 5.5.8 Additional Feature: Nesting 6 FCAFOX Framework for Formal Concept Analysis in JAVA 6.1 Architecture A Appendix A.1 Synonym Lexicon A.2 Galois Connections & Galois Lattices A.3 Fault Tolerance Extensions to Formal Concept Analysis / Entwurf und Beweis eines Algorithmus zur Berechnung inkrementeller Änderungen in einem beschrifteten dargestellten Begriffsverband beim Einfügen oder Entfernen einer Merkmalsspalte im zugrundeliegenden formalen Kontext. Weiterhin sind einige Details zur Implementation sowie zum mathematischen Hintergrundwissen dargestellt.:1 Introduction 1.1 Acknowledgements 1.2 Supporting University: TU Dresden, Institute for Algebra 1.3 Supporting Corporation: SAP AG, Research Center Dresden 1.4 Research Project: CUBIST 1.5 Task Description und Structure of the Diploma Thesis I Mathematical Details 2 Fundamentals of Formal Concept Analysis 2.1 Concepts and Concept Lattice 2.2 Visualizations of Concept Lattices 2.2.1 Transitive Closure and Transitive Reduction 2.2.2 Neighborhood Relation 2.2.3 Line Diagram 2.2.4 Concept Diagram 2.2.5 Vertical Hybridization 2.2.6 Omitting the top and bottom concept node 2.2.7 Actions on Concept Diagrams 2.2.8 Metrics on Concept Diagrams 2.2.9 Heatmaps for Concept Diagrams 2.2.10 Biplots of Concept Diagrams 2.2.11 Seeds Selection 2.3 Apposition of Contexts 3 Incremental Updates for Concept Diagrams 3.1 Insertion & Removal of a single Attribute Column 3.1.1 Updating the Concepts 3.1.2 Structural Remarks 3.1.3 Updating the Order 3.1.4 Updating the Neighborhood 3.1.5 Updating the Concept Labels 3.1.6 Updating the Reducibility 3.1.7 Updating the Arrows 3.1.8 Updating the Seed Vectors 3.1.9 Complete IFOX Algorithm 3.1.10 An Example: Stepwise Construction of FCD(3) 3.2 Setting & Deleting a single cross 4 Iterative Exploration of Concept Lattices 4.1 Iceberg Lattices 4.2 Alpha Iceberg Lattices 4.3 Partly selections 4.3.1 Example with EMAGE data 4.4 Overview on Pruning & Interaction Techniques II Implementation Details 5 Requirement Analysis 5.1 Introduction 5.2 User-Level Requirements for Graphs 5.2.1 Select 5.2.2 Explore 5.2.3 Reconfigure 5.2.4 Encode 5.2.5 Abstract/Elaborate 5.2.6 Filter 5.2.7 Connect 5.2.8 Animate 5.3 Low-Level Requirements for Graphs 5.3.1 Panel 5.3.2 Node and Edge 5.3.3 Interface 5.3.4 Algorithm 5.4 Mapping of Low-Level Requirements to User-Level Requirements 5.5 Specific Visualization Requirements for Lattices 5.5.1 Lattice Zoom/Recursive Lattices/Partly Nested Lattices 5.5.2 Planarity 5.5.3 Labels 5.5.4 Selection of Ideals, Filters and Intervalls 5.5.5 Restricted Moving of Elements 5.5.6 Layout Algorithms 5.5.7 Additional Feature: Three Dimensions and Rotation 5.5.8 Additional Feature: Nesting 6 FCAFOX Framework for Formal Concept Analysis in JAVA 6.1 Architecture A Appendix A.1 Synonym Lexicon A.2 Galois Connections & Galois Lattices A.3 Fault Tolerance Extensions to Formal Concept Analysis