Hafiz ul Asad

City University London

Phase-locked loopElectronic engineeringLock (computer science)Computer scienceExplained sum of squares

5Publications

1H-index

2Citations

What is this?

Publications 5

Newest

#1Hafiz ul Asad (City University London)H-Index: 1

#2Ilir Gashi (City University London)H-Index: 10

We present an analysis of the diversity that exists in the rules and blacklisted IP addresses of the Snort and Suricata Intrusion Detection Systems (IDSs). We analysed the evolution of the rulesets and blacklisted IP addresses of these two IDSs over a 5-month period between May and October 2017. We used three different off-the-shelf default configurations of the Snort IDS and the Emerging Threats (ET) configuration of the Suricata IDS. Analysing the differences in these systems allows us to get ...

#1Hafiz ul Asad (City University London)H-Index: 1

#2Kevin D. Jones (PSU: Plymouth State University)H-Index: 6

This article presents a deductive numeric-symbolic approach, using sum of squares (SOS) programming and quantifier elimination (QE). The authors take ring oscillator as an example to verify that it can start oscillating from all possible initial voltages.

Verifying inevitability of phase-locking in a charge pump phase lock loop using sum of squares programming

Jun 7, 2015 in DAC (Design Automation Conference)

#1Hafiz ul Asad (City University London)H-Index: 1

#2Kevin D. Jones (PSU: Plymouth State University)H-Index: 6

Phase-locking in a charge pump (CP) phase lock loop (PLL) is said to be inevitable if all possible states of the CP PLL eventually converge to the equilibrium where the input and output phases are in lock. We verify this property for a CP PLL using a mixed deductive and bounded verification methodology. This involves a positivity check of polynomial inequalities (which is an NP-Hard problem) so we use the sound but incomplete Sum of Squares (SOS) relaxation algorithm to provide a numerical solut...

May 20, 2015 in GLSVLSI (Great Lakes Symposium on VLSI)

#1Hafiz ul Asad (City University London)H-Index: 1

#2Kevin D. Jones (PSU: Plymouth State University)H-Index: 6

Phase-locking in a charge pump (CP) phase lock loop (PLL) is said to be inevitable if all possible states of the CP PLL eventually converge to the equilibrium, where the input and output phases are in lock and the node voltages vanish. We verify this property for a CP PLL using deductive verification. We split this complex property into two sub-properties defined in two disjoint subsets of the state space. We deductively verify the first property using multiple Lyapunov certificates for hybrid s...

Apr 23, 2014 in DDECS (Design and Diagnostics of Electronic Circuits and Systems)

#1Hafiz ul Asad (City University London)H-Index: 1

#2Kevin D. Jones (City University London)H-Index: 6

Last. Frederic Surre (City University London)H-Index: 9

view all 3 authors...

We present a novel mixed time and frequency domain approach to the formal verification of oscillators properties which are specified in the frequency domain. We use robust periodogram specification to specify the oscillator behaviour in the close vicinity of the limit cycle. Using SAT modulo ODE (SMO) for Bounded Model Checking (BMC) of the non-linear hybrid automata, we show that the oscillator hybrid timed traces satisfy frequency domain specifications.

1