Description
Book Synopsis.- Program Verification.
.- Safeguarding Neural Network-Controlled Systems via Formal Methods: From Safety-by-Design to Runtime Assurance (Invited Talk) .
.- Testing-Based Formal Verification with Program Slicing on Functional Soundness and Completeness.
.- Dependent Assertion Logic for Modular Software Verification.
.- A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms.
.- Machine-Checked Compositional Specification and Proofs for Embedded Systems.
.- Verification and Concurrency.
.- Failure divergence refinement for Event-B
.- Mining Diamonds in labeled Transition Systems.
.- Portability of Optimizations from SC to TSO.
.- SAT and SMT Solving.
.- Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification.
.- SNRWLS: Improve (W)PMS Solver with Weighting Strategies Related to Number of Soft Clauses.
.- Trustworthy AI and System Software.
.- Robust Deep Reinforcement Learning Using Formal Verification.
.- A Formally Verified Neural Network Converter for the Interactive Theorem Prover Coq.
.- COMPASS: An Agent for MLIR Compilation Pass Pipeline Generation.
.- Stable Ranges: Shared Dichotomy in Large Version-Controlled Repositories.
.- Program Analysis using Machine Learning.
.- CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection.
.- FAMiT: Mitigating False Alarms for Program Analysis Using Large Language Models.
.- Security.
.- A Cross-domain Data Sharing Scheme Based on Federated Blockchain.
.- Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs.
.- Detecting speculative data flow vulnerabilities using weakest precondition reasoning.
.- Dynamic Analysis.
.- Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation.
.- State Significance-Guided Fuzzing for Stateful Protocol Program.
.- Unleash the Hidden Power of CAR-based Model Checking through Dynamic Traversal.
