Deciding Serializability in Network Systems
Abstract elided by the publisher.
14,842 papers · page 18 of 743
Concurrent Permissive Strategy Templates
Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS…
Orbitopal Fixing in SAT
Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones already explored. While symmetry handling is routine in other solving paradigms, integrating it into stat…
JLiSA: The Java Frontend of the Library for Static Analysis (Competition Contribution)
Abstract elided by the publisher.
Symbiotic 11 Predicate Abstraction Joins the Party - (Competition Contribution)
Abstract elided by the publisher.
Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
The problem of determining the (least) fixpoint of (higher-dimensional) functions over the non-negative reals frequently occurs when dealing with systems endowed with a quantitative semantics. We focus on the situation in which the functions of interest are not known precisely bu…
Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution)
Abstract elided by the publisher.
LTLf Learning Meets Boolean Set Cover
Learning formulas in Linear Temporal Logic ( $${\textbf {LTL}}_f $$ ) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and …
VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
The automated verification of Linear Temporal Logic (LTL) properties over hybrid systems is an important challenge in formal methods. While numerous tools exist for checking safety and reachability, no framework currently provides a concrete language and algorithm for the full ve…
Syntactically Convex Model-Based Projection for Linear Real Arithmetic
Quantifier elimination (QE) is a key task in formal verification algorithms, and the ability to return partial results, such as under-approximations, is beneficial for many QE clients. In Linear Real Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity…
Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution)
Abstract elided by the publisher.
A Case Study in Firmware Verification: Applying Formal Methods to Intel$^\circledR $ TDX Module
Abstract elided by the publisher.
Evaluating Software Verifiers for C, Java, and SV-LIB - (Report on SV-COMP 2026)
Abstract elided by the publisher.
Iekkë: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs (Competition Contribution)
Abstract elided by the publisher.
Hornix: From LLVM IR to Constrained Horn Clauses and Back (Competition Contribution)
Abstract elided by the publisher.
Seal: Symbolic Execution with Separation Logic - (Competition Contribution)
Abstract elided by the publisher.
AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
We present AKR , a model checking tool for an adaptative probabilistic knowing-how epistemic logic. The tool takes as input the specification of a scenario modeled via a probabilistic LTS (in PRISM notation), a collection of regular expressions acting as agent’s perception, a kno…
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
Abstract elided by the publisher.
Integrating String Reasoning in Symbolic Execution of C Programs
Abstract elided by the publisher.
Hint-Based SMT Proof Reconstruction
Abstract elided by the publisher.