Vladimir Krsmanovic

I am a Ph.D. student at Technical University of Munich working at the CISPA Helmholtz Center for Information Security. I am also a member of the TUM Graduate School.

Most of my work focuses on bridging symbolic methods and deep learning. My work generally falls into two directions:

  • Neural Guided Symbolic Methods: How can we use deep learning to help improve formal methods?
  • Symbolically Regularized Neural Methods: How can we use formal methods to help guide deep learning methods?

I also work on applying formal methods and deep learning to real-life problems, such as law and regulations, autonomous systems, and real-world hardware.

vladimir.krsmanovic@cispa.de
+49 681 87083 2462
CISPA, Saarbrücken
E9 1 / 1.12
Vladimir Krsmanovic
Publications
    FairMon: A Tool for Monitoring and Visualizing Algorithmic Fairness
    Jan Baumeister, Bernd Finkbeiner, Vladimir Krsmanovic, Frederik Scheerer, Julian Siber and Tobias Wagenpfeil · RV 2026

    Runtime monitoring has recently been proposed as a rigorous method for analyzing algorithmic fairness of autonomous decision systems used in critical scenarios such as credit lending, job application, and the criminal justice system. Prior work has shown that runtime monitoring, in principle, can be an effective technique for establishing the kind of human oversight required by legislation such as the EU Artificial Intelligence Act. In practice, the available monitoring tools have not been developed with this application in mind and display several critical shortcomings in these scenarios. In this paper, we present FairMon, a runtime monitoring tool tailored to fairness analysis of high-stakes decision systems. FairMon uses RTLola as a flexible specification language for monitors, which we have extended with conditional probability operators that allow for concise descriptions of algorithmic fairness properties. The tool also features a real-time visualization of intermediary values, enabling human insight into the dynamics of the monitored system.

    PDF
    Details
Preprints
    Predictive Zonotope Reduction: Precise Runtime Monitoring under Uncertainty
    Vladimir Krsmanovic, Florian Kohn, Bernd Finkbeiner and Milan Simovic · arXiv preprint

    Robots operating in physical environments make control decisions based on uncertain sensor measurements, which can lead to unsafe or suboptimal actions. Runtime monitors that check their behavior against safety specifications must represent this uncertainty soundly. Zonotopes are a widely used representation, but continuously incorporating new measurements grows their order unboundedly, so monitors must periodically apply an over-approximating reduction. The choice of the reduction method substantially affects the zonotope’s precision, yet existing approaches typically utilize a fixed method throughout the run, even though the optimal choice depends on the current state. This paper presents a Predictive Zonotope Reduction (PZR) approach, which frames reducer selection as an optimal control problem and solves it using beam-search model predictive control. Policy distillation into a small neural policy further provides substantially higher execution speed than model predictive control while maintaining improved performance, enabling uncertainty-aware runtime monitoring on resource-constrained real-time systems. We implement our approach in the RLola runtime monitoring framework and evaluate it on a 5-degree-of-freedom robotic arm simulated in MuJoCo, with sensor uncertainty modeled according to ISO 5725. Experiments on a Raspberry Pi 5 show that dynamic reduction significantly lowers false-positive rates in monitoring compared with static reduction strategies.

    PDF
    Details
    Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
    Frederik Schmitt, Matthias Cosler, Niklas Metzger, Julian Siber, Vladimir Krsmanovic, Mohamed Ghanem and Bernd Finkbeiner · arXiv preprint

    Explore the results in our interactive demo here

    Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this paper, we tackle both sides of the problem. For the algorithmic side, we present a neuro-symbolic approach to reactive synthesis that couples large reasoning models with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmarks than the best dedicated tools in the annual synthesis competition and extends to constructing parameterized systems, a problem known to be undecidable. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language by introducing a hand-authored dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.

    Details
    Learning Representations Through Contrastive Neural Model Checking
    Vladimir Krsmanovic, Matthias Cosler, Mohamed Ghanem and Bernd Finkbeiner · arXiv preprint

    Model checking is a key technique for verifying safety-critical systems against formal specifications, where recent applications of deep learning have shown promise. However, while ubiquitous for vision and language domains, representation learning remains underexplored in formal verification. We introduce Contrastive Neural Model Checking (CNML), a novel method that leverages the model checking task as a guiding signal for learning aligned representations. CNML jointly embeds logical specifications and systems into a shared latent space through a self-supervised contrastive objective. On industry-inspired retrieval tasks, CNML considerably outperforms both algorithmic and neural baselines in cross-modal and intra-modal settings. We further show that the learned representations effectively transfer to downstream tasks and generalize to more complex formulas. These findings demonstrate that model checking can serve as an objective for learning representations for formal languages.

    PDF
    Details
Theses
    Contrastive Neural Model Checking
    Vladimir Krsmanovic · UdS (Master Thesis)

    Since its inception, many techniques for improving the performance of model checking have been developed: abstraction and reductions, logics and algorithms optimized for them, and statistical and bounded approaches - which have all turned model checking into a tool which is powering modern verification.

    This thesis introduces the CNML family of models, a novel approach integrating deep learning techniques with model checking. We present three models: ContrastiveEncoder, SupervisedClassifier, and CounterTrace along with their architectures and the specialized datasets developed for their training. The ContrastiveEncoder employs contrastive learning to learn vector representations of LTL formulas and AIGER circuits. Building on this, the SupervisedClassifier demonstrates the feasibility of neural model checking by building on ContrastiveEncoder. The CounterTrace model further extends this concept by framing model checking as a sequence-to-sequence problem, enabling both classification and counterexample generation tasks.

    We develop novel dataset augmentation techniques, including the transformation of SC-PAT3 and the introduction of formulaBreaking. We also present a pipeline for evaluating counterexample traces generated by the CounterTrace model.

    Our experiments demonstrate that all three models effectively perform their respective tasks, with transformer architectures successfully generalizing to the semantics of LTL, AIGER, and counterexample traces.

    Details
Advised Theses and Student Projects
Contact Data Privacy Policy Imprint
Home People Publications
More