5,204 Result(s)
within
Chapter
**e **an
Algorithm Analysis and Problem Complexity
Artificial Intelligence
-
Chapter and Conference Paper
Computing the Edge Expansion of a Graph Using Semidefinite Programming
Computing the edge expansion of a graph is a famously hard combinatorial problem for which there have been many approximation studies. We present two versions of an exact algorithm using semidefinite programmi...
-
Chapter and Conference Paper
Correction to: Anti-Money Laundering in Cryptocurrency via Multi-Relational Graph Neural Network
-
Chapter
Correction to: Deriving Priorities from Incomplete Fuzzy Reciprocal Preference Relations
-
Chapter and Conference Paper
CoqCryptoLine: A Verified Model Checker with Certified Results
We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine verification algorithm consists of two reductions. The algebraic reduction tra...
-
Chapter and Conference Paper
Words Can Be Confusing: Stereotype Bias Removal in Text Classification at the Word Level
Text classification is a widely used task in natural language processing. However, the presence of stereotype bias in text classification can lead to unfair and inaccurate predictions. Stereotype bias is parti...
-
Chapter and Conference Paper
Dynamic Multi-View Fusion Mechanism for Chinese Relation Extraction
Recently, many studies incorporate external knowledge into character-level feature based models to improve the performance of Chinese relation extraction. However, these methods tend to ignore the internal inf...
-
Chapter and Conference Paper
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is...
-
Chapter and Conference Paper
Correction to: CoqCryptoLine: A Verified Model Checker with Certified Results
-
Chapter and Conference Paper
3D Environment Modeling for Falsification and Beyond with Scenic 3.0
We present a major new version of Scenic, a probabilistic programming language for writing formal models of the environments of cyber-physical systems. Scenic has been successfully used for the design and anal...
-
Chapter and Conference Paper
cPNN: Continuous Progressive Neural Networks for Evolving Streaming Time Series
Dealing with an unbounded data stream involves overcoming the assumption that data is identically distributed and independent. A data stream can, in fact, exhibit temporal dependencies (i.e., be a time series)...
-
Chapter and Conference Paper
Automatic Program Instrumentation for Automatic Verification
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theo...
-
Chapter and Conference Paper
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
We present an algorithm to learn a deterministic timed automaton (DTA) via membership and equivalence queries. Our algorithm is an extension of the L* algorithm with a Myhill-Nerode style characterization of r...
-
Chapter and Conference Paper
Certified Verification for Algebraic Abstraction
We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. ...
-
Chapter and Conference Paper
Kratos2: An SMT-Based Model Checker for Imperative Programs
This paper describes Kratos2, a tool for the verification of imperative programs. Kratos2 operates on an intermediate verification language called K2, with a formally-specified semantics based on smt, allowing th...
-
Chapter and Conference Paper
Learning Assumptions for Compositional Verification of Timed Automata
Compositional verification, such as the technique of assume-guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion ...
-
Chapter and Conference Paper
Road Network Representation Learning with Vehicle Trajectories
Spatio-temporal traffic patterns reflecting the mobility behavior of road users are essential for learning effective general-purpose road representations. Such patterns are largely neglected in state-of-the-ar...
-
Chapter and Conference Paper
Early Verification of Legal Compliance via Bounded Satisfiability Checking
Legal properties involve reasoning about data values and time. Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties. While MFOTL has been successfully used for ve...
-
Chapter and Conference Paper
Ownership Guided C to Rust Translation
Dubbed a safer C, Rust is a modern programming language that combines memory safety and low-level control. This interesting combination has made Rust very popular among developers and there is a growing trend ...
-
Chapter and Conference Paper
Process Equivalence Problems as Energy Games
We characterize all common notions of behavioral equivalence by one 6-dimensional energy game, where energies bound capabilities of an attacker trying to tell processes apart. The defender-winning initial credits...
-
Chapter and Conference Paper
Fast Termination and Workflow Nets
Petri nets are an established model of concurrency. A Petri net is terminating if for every initial marking there is a uniform bound on the length of all possible runs. Recent work on the termination of Petri ...
