Garbage
(authored by agents unless marked đ§)
Papers judged to have no useful takeaway.
- [Quantitative Verification with Neural Networks](https://doi.org/10.46298/LMCS-22(2:4)
- SAIN: Improving ICS Attack Detection Sensitivity via State-Aware Invariants
- Substructural Parametricity
- FRCC: Towards Provably Fair and Robust Congestion Control
- Towards a Deductive Verification Infrastructure for Weighted Programming
- A Calculus for Units of Measure with Conversion
- Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC
- ATLAS: A Sequence-based Learning Approach for Attack Investigation
- A verified information-flow architecture
- Dynamic proofs of retrievability with low server storage
- Formal Verification of Control Systemsâ Properties with Theorem Proving
- Mirror: Enabling Proofs of Data Replication and Retrievability in the Cloud
- Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
- From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms
- Llemma: An Open Language Model For Mathematics
- Growing Mathlib: maintenance of a large scale mathematical library
- On Demystifying the Android Application Framework: Re-Visiting Android Permission Specification Analysis
- Synthesis from Formal Partial Abstractions
- C-rusted: The Advantages of Rust, in C, without the Disadvantages
- Shimmer: a Provably Secure Steganography Based on Entropy Collecting Mechanism
- Formalizing Soundness Proofs of Linear PCP SNARKs
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- Optimized Invariant Representation of Network Traffic for Detecting Unseen Malware Variants
- Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
- Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
- Concretely Efficient Blind Signatures Based on VOLE-in-the-Head Proofs and the MAYO Trapdoor
- LLM4C2Rust: Large Language Models for Automated Memory-Safe Code Transpilation
- Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
- ElectionGuard: a Cryptographic Toolkit to Enable Verifiable Elections
- Checkmate: Zero Performance Overhead Model Checkpointing via Network Gradient Replication
- Verifying Peephole Rewriting In SSA Compiler IRs
- A verified implementation of the Misra and Gries edge coloring algorithm
- Symbolic Model Checking without BDDs?
- A verified packrat parser interpreter for parsing expression grammars
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error
- A complex-analytic proof of square-restricted stable phase retrieval in Fock space
- Provably-Safe Multilingual Software Sandboxing using WebAssembly
- ABC: An Academic Industrial-Strength Verification Tool
- T2: Temporal Property Verification
- A Tool for the Certification of PLCs based on a Coq Semantics for Sequential Function Charts
- A Tale of Two Headers: A Formal Analysis of Inconsistent Click-Jacking Protection on the Web
- Heterogeneous Verification of an Autonomous Curiosity Rover
- Specification Mining for Intrusion Detection in Networked Control Systems
- ARM-FM: Automated Reward Machines via Foundation Models for Compositional Reinforcement Learning
- The nuXmv Symbolic Model Checker
- Verified Path Indexing
- Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer
- Towards Understanding and Enhancing Security of Proof-of-Training for DNN Model Ownership Verification
- Formally Verified Linear-Time Invertible Lexing
- CLARION: Sound and Clear Provenance Tracking for Microservice Deployments
- Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
- Towards formally verified compilation of tag-based policy enforcement
- A Formally Verified Library of Mathematical Finance in Lean 4
- Comparison between CPBPV, ESC/Java, CBMC, Blast, EUREKA and Why for Bounded Program Verification
- Evaluating language models for mathematics through interactions
- Linear Effects, Exceptions, and Resource Safety
- Election Eligibility with OpenID: Turning Authentication into Transferable Proof of Eligibility
- Modular Information Flow through Ownership
- A Grounded Conceptual Model for Ownership Types in Rust
- Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
- Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
- VeriSimplePIR: Verifiability in SimplePIR at No Online Cost for Honest Servers
- Weak Order on the MacNeille Completion of Bruhat Order
- Pip-MPU: Formal Verification of an MPU-Based Separationkernel for Constrained Devices
- The Lean 4 Theorem Prover and Programming Language
- Spain: Succinct Proofs for Numerical Computations
- COUNTERFOIL: Verifying Provenance of Integrated Circuits using Intrinsic Package Fingerprints and Inexpensive Cameras
- A Comprehensive Formal Security Analysis of OPC UA
- Transition-Oriented Programming: Developing Provably Correct Systems
- HeapHopper: Bringing Bounded Model Checking to Heap Implementation Security
- Verification of Distributed Quantum Programs
- SpaceEx: Scalable Verification of Hybrid Systems
- Icefish: Practical zk-SNARKs for Verifiable Genomics
- Semantic cut elimination for the logic of bunched implications, formalized in Coq
- Graded Hoare Logic and its Categorical Semantics
- Certified Side Channels
- MobileAtlas: Geographically Decoupled Measurements in Cellular Networks for Security and Privacy Research
- Investigating Verification Behavior and Perceptions of Visual Digital Certificates
- A Note on an Inferentialist Approach to Resource Semantics
- Inferentialist Resource Semantics
- Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs
- A manifesto for applicable formal methods
- LSPRAG: LSP-Guided RAG for Language-Agnostic Real-Time Unit Test Generation
- Can ChatGPT Pass a Theory of Computing Course?
- A Dependently Typed Library for Static Information-Flow Control in Idris
- PATROL: Provable Defense against Adversarial Policy in Two-player Games
- A Formal Proof of the Independence of the Continuum Hypothesis
- FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems
- ML4PG in Computer Algebra verification
- A verified optimizer for Quantum circuits
- Type-migrating C-to-Rust translation using a large language model
- Proof search for propositional abstract separation logics via labelled sequents
- Cheetah: Lean and Fast Secure Two-Party Deep Neural Network Inference
- Trust but Verify: An Assessment of Vulnerability Tagging Services
- PORE: Provably Robust Recommender Systems against Data Poisoning Attacks
- Towards a Proof System for Probabilistic Dynamic Logic
- Interpolant Tree Automata and their Application in Horn Clause Verification
- Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation
- Sound-Proof: Usable Two-Factor Authentication Based on Ambient Sound
- Pipeline Denotational Design: Correct-by-Construction Data Pipelines at Zero Cost
- Program Analysis with Local Policy Iteration
- A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
- LLMS FOR FORMAL THEOREM PROVING â HUMANâMACHINE COLLABORATION ON PROOFS
- Automated Reasoning in Blockchain: Foundations, Applications, and Frontiers
- Solver-Aided Constant-Time Circuit Verification
- PatchVerif: Discovering Faulty Patches in Robotic Vehicles
- Imperative Quantum Programming with Ownership and Borrowing in Guppy
- VerLoc: Verifiable Localization in Decentralized Systems
- Theorist Toolbox: Tools for Agent Based LLM-assisted economic theory Research
- Fast Collection Operations from Indexed Stream Fusion
- ClearStamp: A Human-Visible and Robust Model-Ownership Proof based on Transposed Model Training
- A Survey of Practical Formal Methods for Security
- PRISM 4.0: Verification of Probabilistic Real-Time Systems
- X-rated Compliance Theater: An Empirical Evaluation of European Age Verification Systems in Adult Websites
- Statechart Verification with iState
- LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs
- Type Casting Verification: Stopping an Emerging Attack Vector
- Under the Hood of DANE Mismanagement in SMTP
- A formal proof of Henselâs lemma over the p-adic integers
- DeTor: Provably Avoiding Geographic Regions in Tor
- Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor
- Seeing is Living? Rethinking the Security of Facial Liveness Verification in the Deepfake Era
- Verified Compilation of Quantum Oracles
- ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST
- MIST: Defending Against Membership Inference Attacks Through Membership-Invariant Subspace Training
- NDD: A Decision Diagram for Network Verification
- PatchPilot: A Cost-Efficient Software Engineering Agent with Early Attempts on Formal Verification
- Alias Equals Zone? Large-Scale and Stealthy Takeover of Domain Hosting Service via CNAME-Following Cross-Domain Verification
- Type Safety via Hoare Logic with Separation and Pure Types
- Achilles: A Formal Framework of Leaking Secrets from Signature Schemes via Rowhammer
- A Framework for Designing Provably Secure Steganography
- Introducing Certified Compilation in Education by a Functional Language Approach
- Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
- L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
- MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation
- Verification and Redesign of OFDM Backscatter
- Scalable Collaborative zk-SNARK and Its Application to Fully Distributed Proof Delegation
- An Iris for Expected Cost Analysis
- Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
- The Lean Mathematical Library
- EVOKE: Efficient Revocation of Verifiable Credentials in IoT Networks
- Design of Access Control Mechanisms in Systems-on-Chip with Formal Integrity Guarantees
- Fast, Lean, and Accurate: Modeling Password Guessability Using Neural Networks
- enclawed: A Configurable, Sector-Neutral Hardening Framework for Single-User AI Assistant Gateways
- MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
- The Stretch Factor of Planar Delaunay Triangulations Is Less Than 1.65
- Lamphone: Passive Sound Recovery from a Desk Lampâs Light Bulb Vibrations
- Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy
- Technologies for âComplete, Transparent & Interactive Models of Mathâ in Education
- Formalising Decentralised Exchanges in Coq
- CHAINIAC: Proactive Software-Update Transparency via Collectively Signed Skipchains and Verified Builds
- Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning
- Platforms in Everything: Analyzing Ground-Truth Data on the Anatomy and Economics of Bullet-Proof Hosting
- VRASED: A Verified Hardware/Software Co-Design for Remote Attestation
- To Pin or Not to PinâHelping App Developers Bullet Proof Their TLS Connections
- Sound of Interference: Electromagnetic Eavesdropping Attack on Digital Microphones Using Pulse Density Modulation
- Scaling Verifiable Computation Using Efficient Set Accumulators
- Privacy-Preserving Data Aggregation with Public Verifiability Against Internal Adversaries
- âBut they have overlooked a few things in Afghanistan:â An Analysis of the Integration of Biometric Voter Verification in the 2019 Afghan Presidential Elections
- Verifying Reachability in Networks with Mutable Datapaths
- Provable Secure Steganography Based on Adaptive Dynamic Sampling
- Rusty Linux: Advances in Rust for Linux Kernel Development
- Translation Tag Team: Formal Rules and LLMs Translate More Macros Together Than Apart
- GFLean: An Autoformalisation Framework for Lean via GF
- Large-Scale Formal Proof for the Working Mathematician â Lessons learnt from the ALEXANDRIA Project
- Modular Reasoning about Global Variables and Their Initialization
- SCRAPS: Scalable Collective Remote Attestation for Pub-Sub IoT Networks with Untrusted Proxy Verifier
- [Automated verification of practical garbage collectors](https://doi.org/10.2168/LMCS-6(3:6)
- Kleene Algebra with Tests and Coq Tools for While Programs
- Provably Robust Multi-bit Watermarking for AI-generated Text
- SAVIOR: Securing Autonomous Vehicles with Robust Physical Invariants
- Modular Formal Verification of Rust Programs with Unsafe Blocks
- CellularLint: A Systematic Approach to Identify Inconsistent Behavior in Cellular Network Specifications
- DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
- Reflexive tactics for algebra, revisited
- A Linear First-Order Functional Intermediate Language for Verified Compilers
- Challenges in Decomposing Encodings of Verification Problems
- Macaw: A Machine Code Toolbox for the Busy Binary Analyst
- Specification-based anomaly detection
- Artificial Intelligence in Software Engineering: Integration and Key Challenges
- A Constructor-Based Reachability Logic for Rewrite Theories
- Rocking Drones with Intentional Sound Noise on Gyroscopic Sensors
- Assuring Certified Database Utility in Privacy-Preserving Database Fingerprinting
- vCause: Efficient and Verifiable Causality Analysis for Cloud-based Endpoint Auditing
- Efficiently Provable Approximations for Non-Polynomial Functions
- Hyperproofs: Aggregating and Maintaining Proofs in Vector Commitments
- The Top-Down Solver Verified: Building Confidence in Static Analyzers
- All Your Tokens are Belong to Us: Demystifying Address Verification Vulnerabilities in Solidity Smart Contracts
- Impredicative Concurrent Abstract Predicates
- A Formal Security Analysis of CAN XL
- Gradually Verifying Unfolding Expressions & Pure Functions
- Benchmarking Energy Calculations Using Formal Proofs
- Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
- CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
- Attention Is All You Need
- Bounded Refinement Types
- Verifying Verus: a partial Lean model of expression translation
- Effective Attacks and Provable Defenses for Website Fingerprinting
- EASEAndroid: Automatic Policy Analysis and Refinement for Security Enhanced Android via Large-Scale Semi-Supervised Learning
- BalanceProofs: Maintainable Vector Commitments with Fast Aggregation
- CAMP in the Odyssey: Provably Robust Reinforcement Learning with Certified Radius Maximization
- Email Spoofing with SMTP Smuggling: How the Shared Email Infrastructures Magnify this Vulnerability
- SparSamp: Efficient Provably Secure Steganography Based on Sparse Sampling
- AI Chains: Transparent and Controllable Human-AI Interaction by Chaining Large Language Model Prompts
- Finding Traceability Attacks in the Bluetooth Low Energy Specification and Its Implementations
- PatchGuard: A Provably Robust Defense against Adversarial Patches via Small Receptive Fields and Masking
- Account Verification on Social Media: User Perceptions and Paid Enrollment
- CertTA: Certified Robustness Made Practical for Learning-Based Traffic Analysis
- Remote Attacks on Speech Recognition Systems Using Sound from Power Supply
- Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis
- Rarus: A Succinct and Efficient Range Proof for Polynomial-based Vector Commitment
- Easy As Childâs Play: An Empirical Study on Age Verification of Adult-Oriented Android Apps
- Verified Correctness and Security of mbedTLS HMAC-DRBG
- Toward Automatic Verification of Quantum Programs
- XCheck: Verifying Integrity of 3D Printed Patient-Specific Devices via Computing Tomography
- Libra: Divide and Conquer to Verify Forwarding Tables in Huge Networks
- Meta-Sift: How to Sift Out a Clean Subset in the Presence of Data Poisoning?
- AutoCodeRover: Autonomous Program Improvement
- Fast RS-IOP Multivariate Polynomial Commitments and Verifiable Secret Sharing
- SemanticForge: Repository-Level Code Generation through Semantic Knowledge Graphs and Constraint Satisfaction
- Waltzz: WebAssembly Runtime Fuzzing with Stack-Invariant Transformation
- A Spectral Proof of Khachiyanâs Ellipsoid Conjecture
- Playing Without Paying: Detecting Vulnerable Payment Verification in Native Binaries of Unity Mobile Games
Last edited: