This research programme investigates how behavioral models, formal logic, automated reasoning, and explainable diagnostics can support the analysis, verification, and understanding of software systems developed with AI assistance.

The long-term objective is to establish foundations for Explainable Behavioral Engineering (EBE), enabling the transformation of requirements and behavioral artifacts into formally analyzable representations supporting verification, diagnosis, and explainability.

Requirements
    ↓
Behavioral Models
    ↓
Logical Specifications
    ↓
Verification
    ↓
Diagnostic Explainability
    ↓
Behavioral Accountability

This level contains peer-reviewed results forming the published scientific foundation of the programme. The complete list of publications is available in the author's publication profile and related project materials and is therefore not repeated here. The published foundations establish the feasibility of:

• transforming behavioral models into logical specifications,
• applying automated reasoning and theorem proving,
• integrating behavioral modeling with software engineering workflows,
• supporting AI-assisted software engineering through formal methods.

[Kli 25 FSE-AI-IDE], [Kli Sem 25 EASE], [Kli Wit 25 EMSE], [Kli 25 PACIS], [Kli 24 IS], [Kli Wit 24 ASE-RENE], [Kli 24 ASE-ASYDE], [Kli 24 ISD], [Kli 23 ISD], [Kli 19 LAMP], [Kli 18 Access], [Kli 14 AMCS]

This level documents current research directions extending the published foundations toward a coherent programme of explainable and verifiable behavioral engineering.

Behavioral Modeling and Elicitation

[Kli 26d] Radoslaw Klimek „AI-Assisted Behavioural Modelling from Logical Squares”. Workshop conference paper, Rank A, 140 pkt, under review, available https://drive.google.com/file/d/16Jv_s1as1nyTmG_fGRpZIMyQD0ZCEXJd/view?usp=sharing

Behavioral Verification

[Kli Wit 25 EMSE] Radosław Klimek, Julia Witek “Logic Mining from Process Logs: Towards Automated Specification and Verification” The extended version of the conference paper has been submitted to the JCR journal with Q2 quartiles, under review, and a pre-print version available at https://arxiv.org/abs/2506.08628

[Kli et at 26] Natania Dyczek, Jagoda Flejmer „Why Formal Constraints Fail on Real-World Execution Logs: The Dead-End Phenomenon”. Conference paper, Rank A, 140 pkt, under review, available at: https://drive.google.com/file/d/1BPOiJOxaOxiZXbeJBofehkj7kp5c-2fk/view?usp=sharing.

Diagnostic Explainability

[Kli Bla 26] Radosław Klimek, Jakub Blazowski “Towards Diagnostic Explainability inWorkflow Verification via Shapley Attribution”. Flagship conference Core Rank A*, under review, or pre-print version available at https://arxiv.org/abs/2512.09562

[Kli 26] Radoslaw Klimek „Toward Defensible System Behavior in AI-Assisted Software Engineering”. Conference paper, Rank A, 140 pkt, under review, available at: https://drive.google.com/file/d/1Kd27tbguuhNDsPEkscktOx6oEAAwgMJi/view?usp=sharing.

[Klo Kli 26] Michał Klos, Radoslaw Klimek „Learning System Behavior from Logs: Graph-Based Anomaly Detection Using Attribute-Aware Autoencoders”. Conference paper, Rank A, 140 pkt, under review, available at: https://drive.google.com/file/d/1FEitqDCgZxdCjjI4pXMdOEoLzQSU2cMQ/view?usp=sharing.

AI-Assisted Software Engineering

[Kli 26b] Radoslaw Klimek „What Fails in Empirical SE and AI4SE? A Study of Evaluation Fragility”. Conference paper, Rank A, 140 pkt, under review, available at: https://drive.google.com/file/d/1rjYP3S3yKVl0RNMSl3Ft5rxyP2uoyd2N/view?usp=sharing and also https://drive.google.com/file/d/1qkMWiD381YzMZrXgdPyGwyBBfZcaf-Z-/view?usp=sharing

[Kli 26c] Radoslaw Klimek „A Workflow-Based LLM Assistant for Iterative and Verified Requirements Engineering”. Workshop conference paper, Rank A, 140 pkt, under review, available at: https://drive.google.com/file/d/1QgdzVxNvLCtg3BBg6fElI0x_rLc-jIRt/view?usp=sharing.

Others / Adjacent Research

[Kli 26e] Radoslaw Klimek „Context-Aware Orchestration of Adaptive Decisions in Intelligent Environments”. Journal JCR/IF paper, Q1 quartile, 200 pkt, under review, , available at: https://drive.google.com/file/d/1Jv_oO5OFf8t2cbTlOfYDvOcDNYHHHnUT/view?usp=sharing.

[Kli Ole 26] Radoslaw Klimek, Arkadiusz Olesek „A prole-based framework for the generation of synthetic tourist mobility trajectories in urban decision support”. Journal JCR/IF paper, Q1 quartile, 200 pkt, under review, available at: https://drive.google.com/file/d/1n5uMnilJrz0yGkkBc4aRcXy8pgZ8Aee1/view?usp=sharing.

This level contains experimental environments, benchmarks, datasets, and prototypes used to validate research hypotheses and demonstrate technical feasibility. This level comprises experimental environments, benchmark collections, datasets, and prototype systems developed to validate research hypotheses and demonstrate the technical feasibility of the proposed methods.

LIGIMINE

A central component is LOGIMINE (Logic Mining and Verification Environment), a research platform supporting the complete pipeline from event logs to formal behavioral analysis. The platform integrates workflow discovery from execution traces, behavioral modeling using workflows and process trees, automatic generation of logical specifications, formal verification through automated theorem proving, process comparison, compliance checking, what-if analysis, and visual analytics for exploring behavioral structures and verification outcomes.

LOFT

Another key component is LOFT (Logical Framework and Testbench), a benchmark generation and experimentation environment for automated reasoning in software engineering. LOFT supports the generation and management of logical verification problems, including satisfiability, consistency, implication, redundancy, conflict detection, behavioral constraints, and theorem-proving tasks. The framework enables the construction of benchmark families with controllable structural properties, facilitating systematic evaluation of theorem provers, SAT/SMT solvers, and logic-based verification methods.

ATP Benchmark Collection

The infrastructure further includes the ATP Benchmark Collection, a benchmark suite of automated theorem proving problems derived from software-engineering-oriented behavioral verification tasks, and the Logical Problem Catalog, a curated repository of logical verification problems involving behavioral models, workflow specifications, consistency checking, satisfiability analysis, property validation, implication reasoning, and behavioral diagnostics. Together, these platforms and resources provide an experimental foundation for advancing explainable and verifiable behavioral engineering through reproducible evaluation, benchmark-driven research, and prototype validation.

RE-IDE

Workflow-driven requirements engineering environment supporting structured model generation, clarification, validation, and preparation of artifacts for formal verification.

The programme integrates software engineering, requirements engineering, formal methods, process mining, automated reasoning, and AI-assisted development. Its central objective is to move from artifact-level correctness toward explainable and verifiable reasoning about system behavior.