Exact safety certification and adversarial robustness evaluation
of piecewise-linear neural networks on the German Traffic Sign
Recognition Benchmark (GTSRB). Compares standard empirical risk
minimization (ERM) against mixed adversarial training, verifying
exact output invariance within a continuous $L_\infty$
perturbation hypercube:
$$\forall x \in \mathbb{R}^d \text{ with } \|x - x_0\|_\infty
\le \epsilon, \quad \arg\max_{i} f(x)_i = y_0$$
Formal robustness specification under $L_\infty$ perturbation.
Leverages the Marabou SMT solver to establish sound verification
guarantees against gradient-based heuristic attacks (PGD),
exploring the combinatorial scalability of Reluplex and
certifying inviolability against localized physical adversarial
patches on road signs.
Investigation of deterministic chaos and bifurcation phenomena
in a continuous tri-trophic food chain ($X, Y, Z$) governed by
the Hastings-Powell ODE system with Holling type II functional
responses:
$$\begin{cases} \dot{X} = X\left(1 - \dfrac{X}{K}\right) -
\dfrac{a_1 X Y}{1 + b_1 X} - h_X X \\[8pt] \dot{Y} = \dfrac{a_1
X Y}{1 + b_1 X} - \dfrac{a_2 Y Z}{1 + b_2 Y} - d_1 Y \\[8pt]
\dot{Z} = \dfrac{a_2 Y Z}{1 + b_2 Y} - d_2 Z \end{cases}$$
Hastings-Powell differential equations.
Analyzes strange attractors, Lyapunov exponents, bifurcation
cascades under carrying capacity $K$, and chaos suppression via
linear prey harvesting ($h_X$).
A three-dimensional Minesweeper puzzle engine built in
Python/Ursina (with Marco Carmignano), featuring an automated
exact solver based on linear integer constraint satisfaction:
$$\bigwedge_{v \in V_{\text{revealed}}} \left( \sum_{u \in
\mathcal{N}_{3D}(v)} x_u = k_v \right), \quad x_u \in \{0, 1\}$$
Constraint satisfaction problem for Minesweeper3D.
ezone is a minimalist desktop music player that transforms your
local digital audio collection into an interactive,
vinyl-inspired record experience.