Tag
The article discusses the possibility of expressing reachability properties in TLA⁺, referencing Leslie Lamport's work and the limitations of the TLC model checker.
This paper presents the revised analysis engine for Verifpal, a symbolic protocol verifier, detailing its formal specification, proofs, and evaluation against other tools like ProVerif and Tamarin.
Geoffrey Irving highlights the NDIST report on formal methods for security, noting that the scale-up problem has shifted to market coordination among hardware and software makers.
The article explores a search for a compositional theory of self-stabilization in distributed systems, critiquing recent papers on metastable failures and formal methods like rely-guarantee contracts.
Introduces PetriBench, a scalable benchmark using Petri nets to evaluate LLM reasoning over dynamic state spaces, demonstrating that accuracy decreases with difficulty and reveals task-specific capabilities across models.
The paper proposes an independence-graded audit protocol for agentic AI systems, grading independence along principal, substrate, and evidence axes, and provides a formal basis with analysis.
This paper presents ContrAgent, a contract-based framework for symbolic temporal supervision of LLM agents that ensures deterministic safety checks both online and offline with low latency.
The article addresses the challenges of scaling human oversight for AI agents and demonstrates using formal methods with the Z3 library to verify that agent policy changes stay within approved permissions.
The paper proposes Generalized Agent Iteration (GAI) as a formal framework unifying iterative policy improvement and recursive self-improvement, defining agents as modifiable components and distinguishing cases based on external evaluation and internal improvement.
The article explains program synthesis techniques, specifically counterexample-guided iterative synthesis for loop-free programs, and provides an implementation in Rust using the Z3 solver.
The article discusses a scientific paper that formally proves the boundaries of verification in systems, arguing that trust decisions must be explicit and managed beyond a certain point.
The article distinguishes between two types of abstraction in system design: modularity abstraction, which hides internals, and modeling abstraction, which reduces systems to essential behaviors for formal reasoning.
The article discusses the absence of formal specifications for complex software systems, using hypothetical scenarios to highlight the challenges and importance of formal methods in computer science.
An article examining the evolving role of finite-state model checking in computer science and software verification.
This article explores programming language semantics and its critical role in memory safety, explaining operational, denotational, and axiomatic approaches in an educational context.
PANDA is a scalable system using zero-knowledge proofs to verify the robustness and fairness of neural networks without revealing model parameters, enabling certification for large networks with polynomial complexity.
The paper introduces a minimal-core-guided repair method for neuro-symbolic constraint solving, where language models use proofs from unsatisfiable cores to correct translation errors, reducing fabrication in solutions.
This paper formalizes a programming paradigm for spatiotemporal composability by unifying effects and coeffects, enabling dynamic component composition through the Cordis meta-framework.
Introduces 'Training Under Challenge', an executable-certificate framework that uses architecture-valid procedures to construct alternative models and estimate the empirical global-optimality gap of neural network checkpoints, with theoretical guarantees and experiments on ResNet-18 distillation and quantized denoising.
John Regehr describes using tis-interpreter to search for undefined behavior in SQLite, finding bugs like dangling pointer uses and uninitialized reads that other tools missed.