Density-based spatial clustering of applications with noise (DBSCAN) is the most commonly used density-based clustering algorithm, where it can discover multiple clusters with arbitrary shapes. DBSCAN works properly when the input data type is homogeneous, but the DBSCAN's approach may not be sufficient when the input dataset has textual heterogeneity (e.g., when we intend to find clusters from geo-tagged posts on social media relevant to a certain point-of-interest (POI)), thus leading to poor performance. In this paper, we present DBSTexC, a new density-based clustering algorithm using spatio--textual information on Twitter. We first define POI-relevant and POI-irrelevant tweets as the records that contain and do not contain a POI name or its coherent variations, respectively. By taking into account the fractions of POI-relevant and POI-irrelevant tweets, our DBSTexC algorithm shows a much higher clustering quality than the DBSCAN case in terms of the F1 score and its variants. DBSTexC can be thought of as a generalized version of DBSCAN due to the findings that it performs identically as DBSCAN when the inputs are homogeneous and far outperforms DBSCAN when the heterogeneous input data type is given.

Ensuring functional correctness of hardware and software is a bottleneck in every design process of Embedded Systems. This paper proposes an approach to formally verify low-level software in conjunction with the hardware. The proposed approach is based on Interval Property Checking (IPC) that has proved successful on large industrial hardware designs. In this paper, IPC is extended by a specific abstraction technique that makes it tractable for hardware/software co-verification on realistic industrial designs. In the proposed methodology sets of finite state sequences of the system are abstracted by interval properties. This allows us to handle long sequences of state transitions in the hardware as they occur when running programs. We demonstrate the feasibility of our approach using the example of an industrial LIN software running on a public domain microprocessor platform.

This paper proposes enhancements to SAT-based property checking with the goal to increase the spectrum of applications where a proof of unbounded validity of a safety property can be provided. For this purpose, invariants are computed by reachability analysis on an abstract model. The main idea of the paper consists in a BDD-based analysis of k-step-induction on the abstract model and its use to guide a step-wise refinement process of the initial abstraction. The property is then proven on a bounded model of the original design using the computed invariant. The new approach has been applied to formally verify industrial SoC modules. In our experiments, we consider particularly difficult verification tasks occurring in the context of protocol compliance verification using generic, transaction-style verification IPs. In our experiments, numerous properties are proven which either required substantial manual interaction in previous approaches, or cannot be proven at all by other methods available to us.

We propose a methodology to formally prove protocol compliance for communication blocks in System-on-Chip (SoC) designs. In this methodology, a set of operational properties is specified with respect to the states of a central finite state machine (FSM). This central FSM is called main FSM and controls the overall behavior of the design. In order to prove a set of compliance properties, we developed an approach that combines property checking on a bounded circuit model with an approximate reachability analysis. The property checker determines whether a property is valid for an arbitrary state of the design regardless of its reachability. In order to avoid false negatives, reachability constraints are added to the property, which are generated by an approximate FSM traversal algorithm. We show how the existence of a main FSM can be exploited systematically in the reachability analysis and how to partition both the transition relation and the state space such that the computational complexity is reduced drastically. This makes formal verification of protocol compliance tractable even for large designs with several thousand state variables. Our approach has been applied successfully to verify several industrial designs.

In bounded model checking (BMC)-based verification flows lack of reachability constraints often leads to false negatives. At present, it is daily practice of a verification engineer to identify the missing reachability constraints by manually inspecting the design code and by analyzing counterexamples. This, unfortunately, requires a lot of effort and is prone to errors. We propose an algorithm to determine reachability constraints automatically. The proposed approach applies to a design style where the operation of the design is controlled by a main FSM which can easily be extracted from the RTL description of the circuit. The algorithm decomposes and analyzes the state space of the circuit by considering transitions of the main FSM. Experimental results show that the proposed method can considerably reduce the manual work of verification engineers.