Satisfiability-based verification techniques relying on Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers have proven effective for program analysis. Nevertheless, SMT solvers often struggle with non-linear arithmetic, particularly when floating-point (FP) computations are involved, which is especially problematic for safety-critical systems. A further challenge arises from loops with variable bounds: in bounded model checking (BMC), such loops must be unrolled to a fixed depth, risking under-approximation or state-space explosion.This paper explores an alternative formulation of satisfiability checking as a global optimization (GO) problem. We provide formal transformation rules to convert SMT formulas in both FP and bit-vector (BV) theories into equivalent GO problems, with proofs of property preservation. Built on these foundations, we present and extend parSAT, a portfolio-based semi-decision procedure for reasoning about FP constraints. In an empirical evaluation, parSAT identifies satisfying solutions for up to 102 out of 214 SMT instances from the Griggio benchmark suite with an average runtime of 0.1 seconds per satisfiable equation – substantially faster than state-of-the-art SMT solvers – and demonstrates strong performance on real-world verification benchmarks. Combining parSAT with a conventional SMT solver in a hybrid strategy reduces average solving time by more than 60% and increases resolved instances compared to the SMT solver alone.We further present goLoop, which applies the same GO-based transformation to encode variable-bounded loops without explicit unrolling, addressing a key BMC limitation. We also propose SMT-LIB2 language extensions for direct imperative loop encoding and demonstrate successful verification of loop-based programs where conventional BMC encounters limitations.
Matching logic is a general formal framework for reasoning about a wide range of theories, with particular emphasis on programming language semantics. Notably, the intermediate language of the K semantics framework is an extension of matching mu -logic, a sorted, polyadic variant of the logic. Metatheoretic reasoning requires the logic to be expressed within a foundational theory; opting for a dependently typed one enables well-sortedness in the object theory to correspond directly to well-typedness in the host theory. In this paper, we present the first dependently typed definition of matching mu -logic, ensuring well-sortedness via sorted contexts encoded in type indices. As a result, ill-sorted syntax elements are unrepresentable, and the semantics of well-sorted elements are guaranteed to lie within the domain of their associated sort.
Threat detection systems rely on rule-based logic to identify adversarial behaviors, yet the conformance of these rules to high-level threat models is rarely verified formally. We present a formal verification framework that models both detection logic and attack trees as labeled transition systems (LTSs), enabling automated conformance checking via bisimulation and weak trace inclusion. Detection rules specified in the Generic Threat Detection Language (GTDL, a general-purpose detection language we formalize in this work) are assigned a compositional operational semantics, and threat models expressed as attack trees are interpreted as LTSs through a structural trace semantics. Both representations are translated to LNT, a modeling language supported by the CADP toolbox. This common semantic domain enables systematic and automated verification of detection coverage. We evaluate our approach on real-world malware scenarios such as LokiBot and Emotet and provide scalability analysis through parametric synthetic models. Results confirm that our methodology identifies semantic mismatches between threat models and detection rules, supports iterative refinement, and scales to realistic threat landscapes.
Cybersecurity threats continue to become more sophisticated and diverse in their artifacts, boosting both their volume and complexity. To overcome those challenges, we present GView, an open-source forensic analysis framework with visual and AI-enhanced reasoning. It started with focus on the practical cybersecurity industry. It has evolved significantly, incorporating large language models (LLMs) to dynamically enhance reasoning and ease the forensic workflows. This paper surveys both the current state of GView with its published papers and work that is currently under review. It also includes its innovative use of logical inference through predicates and inference rules for both the analyzed documents and the user's actions for better suggestions. We highlight the extensible architecture, showcasing its potential as a bridge between the practical forensics world with the academic research.
The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that can formally or empirically prove the presence of defects. This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, LLMs, Kontrol, and Forge. Our approach is designed to reliably detect defects and generate proofs. We currently perform experiments with promising results for seven types of critical defects. We demonstrate the pipeline's efficacy by presenting our findings for three vulnerabilities – Reentrancy, Complex Fallback, and Faulty Access Control Policies – that are challenging for current verification solutions, which often generate false alarms or fail to detect them entirely. We highlight the potential of either symbolic or concrete execution in correctly classifying such code faults. By chaining these instruments, our method effectively validates true positives, significantly reducing the manual verification burden. Although we identify potential limitations, such as the inconsistency and the cost of LLMs, our findings establish a robust framework for combining heuristic analysis with formal verification to achieve more reliable and automated smart contract auditing.
Even with the increase of popularity of functional programming, imperative programming remains a key programming paradigm, especially for programs operating at lower levels of abstraction. When such software offers key components of a Trusted Computing Base (TCB), e.g. an operating system kernel, it becomes desirable to provide mathematical correctness proofs. However, current real-world imperative programming languages possess "expressive", i.e. overly permissive, semantics. Thus, producing correctness proofs of such programs becomes tedious and error-prone, requiring to take care of numerous "administrative" details. Ideally, a proof-oriented imperative language should feature well-behaved semantics while allowing imperative idioms. To obtain a high-degree of confidence in the correctness of such a language, its tools should be developed inside a proof-assistant such that program proofs are machine checked. We present GallinaC, a shallow embedding of a Turing-complete imperative language directly inside the functional programming language of the Rocq proof assistant, Gallina. In particular, it features a truly generic and unbounded while loop. Having a functional core means proofs about GallinaC programs may use the same tactics as proofs about pure functional ones. Work on GallinaC is still under progress, but we present first promising results. A prototype implementation has shown the viability of GallinaC with the correctness proof of a list reversal procedure for linked-lists of unknown size. We currently focus on the forward simulation between the GallinaC intermediate representation (IR) and Cminor, the entry language of the CompCert back-end.
Python's typing system has evolved pragmatically into a powerful but theoretically fragmented system, with scattered specifications. This paper proposes a formalization to address this fragmentation. The central contribution is a formal foundation that uses concepts from type theory to demonstrate that Python's type system can be elegantly described. This work aims to serve as a crucial first step toward the future development of type inference tools.
Based on the already known connection between multilayer perceptrons and Lukasiewicz logic with rational coefficients, we take a step forward in analyzing its training process using a three-sorted hybrid modal logic: a multilayer perceptron is a logical formula; the actions of the training process are modal operators; the training process is a sequence of logical deductions. Using the proof assistant and the programming language Lean 4, the algorithmic implementation of the training process is certified by logical proofs.
Strong functors and monads are ubiquitous in Computer Science. More recently, comonads have demonstrated their use in structuring context-dependent notions of computation. However, the dualisation of "being strong" property passed somehow unobserved so far. We argue that "being costrong" gives a different understanding of how functors can interact with monoidal structures. This work in progress aims to explore costrong functors and their natural properties, with an eye towards the semantics of computations.
To cater to the needs of (Zero Knowledge) proofs for (mathematical) proofs, we describe a method to transform formal sentences in 2 x 2 - matrices over multivariate polynomials with integer coefficients, such that usual proof-steps like modus-ponens or the substitution are easy to compute from the matrices corresponding to the terms or formulas used as arguments. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to the axioms have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. On such sequences, various Zero Knowledge methods can be applied.
Pointers are a powerful, but dangerous feature provided by the C and C++ programming languages, and incorrect use of pointers is a common source of bugs and security vulnerabilities. Making secure software is crucial, as vulnerabilities exploited by malicious actors not only lead to monetary losses, but possibly loss of human lives. Fixing these vulnerabilities is costly if they are found at the end of development, and the cost will be even higher if found after deployment. That is why it is desirable to find the bugs as early in the development process as possible. We propose a framework that can statically find use-after-free bugs at compile-time and report the errors to the users. It works by tracking the lifetime of objects and memory locations pointers might point to and, using this information, a possibly invalid dereferencing of a pointer can be detected. The framework was tested on over 100 handwritten small tests, as well as 5 real-world projects, and has shown good results detecting errors, while at the same time highlighting some scenarios where false positive reports may occur. Based on the results, it was concluded that our framework achieved its goals, as it is able to detect multiple patterns of use-after-free bugs, and correctly report the errors to the programmer.
Software Defined Networking (SDN) has become a new paradigm in computer networking, introducing a decoupled architecture that separates the network into the data plane and the control plane. The control plane acts as the centralized brain, managing configuration updates and network management tasks, while the data plane handles traffic based on the configurations provided by the control plane. Given its asynchronous distributed nature, SDN can experience data races due to message passing between the control and data planes. This paper presents Tracer, a tool designed to automatically detect and explain the occurrence of data races in DyNetKAT SDN models. DyNetKAT is a formal framework for modeling and analyzing SDN behaviors, with robust operational semantics and a complete axiomatization implemented in Maude. Built on NetKAT, a language leveraging Kleene Algebra with Tests to express data plane forwarding behavior, DyNetKAT extends these capabilities by adding primitives for communication between the control and data planes. Tracer exploits the DyNetKAT axiomatization and enables race detection in SDNs based on Lamport vector clocks. Tracer is a publicly available tool.
Even though much progress has been made in identifying and mitigating smart contract vulnerabilities, we often hear about coding or design issues leading to great financial losses. This paper presents our progress toward finding defects that are sometimes not detected or completely detected by state-of-the-art analysis tools. Although it is still in its incipient phase, we developed a working solution built on top of Slither that uses interval analysis to evaluate the contract state during the execution of each instruction. To improve the accuracy of our results, we extend interval analysis by also considering the constraints imposed by specific instructions. We present the current solution architecture in detail and show how it could be extended to other static analysis techniques, including how it can be integrated with other third-party tools. Our current benchmarks contain examples of smart contracts that highlight the potential of this approach to detect certain code defects.
In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.
Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.
We define two kinds of geometry-preserving reductions between constraint satisfaction problems and other NP-search problems. We give a couple of examples and counterexamples for these reductions.
The ecosystem of Privacy Calculus is a formal framework for privacy comprising (a) the Privacy Calculus, a Turing-complete language of message-exchanging processes based on the pi-calculus, (b) a privacy policy language, and (c) a type checker that checks adherence of Privacy Calculus terms to privacy policies. BPMN is a standard for the graphical description of business processes which aims to be understandable by all business users, from those with no technical background to those implementing software. This paper presents how (a subset of) BPMN diagrams can be converted to Privacy Calculus terms, in the hope that it will serve as a small piece of larger workflows for building privacy-preserving software. The conversion is described mathematically in the paper, but has also been implemented as a software tool.
Petri Nets (PN) are extensively used as a robust formalism to model concurrent and distributed systems; however, they encounter difficulties in accurately modeling adaptive systems. To address this issue, we defined rewritable PT nets (RwPT) using Maude, a declarative language that ensures consistent rewriting logic semantics. Recently, we proposed a modular approach that employs algebraic operators to build extensive RwPT models. This methodology uses composite node labeling to maintain hierarchical organization through net rewrites and has been shown to be effective. Once stochastic parameters are integrated into the formalism, we introduce an automated procedure to derive a lumped CTMC from the quotient graph generated by a modular RwPT model. To demonstrate the effectiveness of our method, we present a fault-tolerant manufacturing system as a case study.
ReScript is a strongly typed language that targets JavaScript, as an alternative to gradually typed languages, such as TypeScript. In this paper, we present a sound type system for data-flow analysis for a subset of the ReScript language, more specifically for a lambda-calculus with mutability and pattern matching. The type system is a local analysis that collects information about variables that are used at each program point as well as alias information.
We employ the mathematical methodology of metric semantics in designing the continuation-based denotational and operational semantics for two process calculi recently investigated in the literature based on well-known Milner's CCS. We prove that our denotational models are weakly abstract with respect to their corresponding operational models.
