yusuke1997/dblp-id-title huggingface dataset:
Simulation-Equivalent Reachability of Large Linear Systems with Inputs
Efficient Reachability Analysis of Hierarchical Reactive Machines
Deciding Separation Formulas with SAT
Deadlock Checking Using Net Unfoldings
Action-Based Model Checking: Logic, Automata, and Reduction
Policy Monitoring in First-Order Temporal Logic
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Safety-Aware Apprenticeship Learning
Verifying Global Two-Safety Properties in Neural Networks with Confidence
Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference
QEBVerif: Quantization Error Bound Verification of Neural Networks
Applying SAT Methods in Unbounded Symbolic Model Checking
The Vampire Diary
Dense Counter Machines and Verification Problems
The BINCOA Framework for Binary Code Analysis
Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings
Bounded Cycle Synthesis
A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Lower-Bound Synthesis Using Loop Specialization and Max-SMT
Fast Numerical Program Analysis with Reinforcement Learning
Regular Model Checking
Probabilistic CEGAR
Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software
Verification Across Intellectual Property Boundaries
PRISM 4.0: Verification of Probabilistic Real-Time Systems
PARAM: A Model Checker for Parametric Markov Models
Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings
Specification-Guided Learning of Nash Equilibria with High Social Welfare
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
Relative Equivalence in the Presence of Ambiguity
Symbolic Model Checking of Non-regular Properties
Real-Time Verification of Statemate Designs
Better Quality in Synthesis through Quantitative Objectives
Multiple Counters Automata, Safety Analysis and Presburger Arithmetic
Empirical Software Metrics for Benchmarking of Verification Tools
Classification and Coverage-Based Falsification for Embedded Control Systems
Network-Wide Configuration Synthesis
Even Faster Conflicts and Lazier Reductions for String Solvers
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
Android Stack Machine
Measuring and Synthesizing Systems in Probabilistic Environments
Verifying Systems with Replicated Components in Mur phi
Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
A Dash of Fairness for Compositional Reasoning
Local Search for SMT on Linear Integer Arithmetic
Efficient Algorithms for Model Checking Pushdown Systems
Some Progress in the Symbolic Verification of Timed Automata
Automatic Abstraction for Verification of Timed Circuits and Systems
Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Optimizing Symbolic Model Checking for Constraint-Rich Models
ProbReach: A Tool for Guaranteed Reachability Analysis of Stochastic Hybrid Systems
PVSio-web 2.0: Joining PVS to HCI
Slugs: Extensible GR(1) Synthesis
XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Systems
Symbolic Bisimulation Minimisation
Hardware Verification using Monadic Second-Order Logic
Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses
Timing Verification by Successive Approximation
Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives
Starling: Lightweight Concurrency Verification with Views
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits
Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification
Stochastic Omega-Regular Verification and Control with Supermartingales
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion
TTP: Tool for Tumor Progression
Efficient Parallel Strategy Improvement for Parity Games
Automatic Generation of Attacker Contracts in Solidity
prod 3.2: An Advanced Tool for Efficient Reachability Analysis
Approximate Relational Reasoning for Quantum Programs
Model Checking Boot Code from AWS Data Centers
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability
CEGAR for Qualitative Analysis of Probabilistic Systems
Linear Functional Fixed-points
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B
Proving Linearizability Using Forward Simulations
Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
State-Space Caching Revisited
Safraless Synthesis for Epistemic Temporal Specifications
F-Soft: Software Verification Platform
State/Event-Based LTL Model Checking under Parametric Generalized Fairness
Mechanically Checked Proofs of Kernel Specification
Methods for Mu-calculus Model Checking: A Tutorial (Abstract)
Comparing Generic State Machines
Interpolating Strong Induction
Verifying Neural Networks Against Backdoor Attacks
Symbolic Localization Reduction with Reconstruction Layering and Backtracking
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting
Parallelizing the Mur phi Verifier
Model-Checking for Hybrid Systems by Quotienting and Constraints Solving
VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization
Automatically Proving Program Termination
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis
Deciding Equality Formulas by Small Domains Instantiations
Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
Lexicographic Ranking Supermartingales with Lazy Lower Bounds
STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors
Fast LTL to Büchi Automata Translation
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
Ivy: A Multi-modal Verification Tool for Distributed Algorithms
A Modular Checker for Multithreaded Programs
Quantifier Elimination via Functional Composition
Automated Assume-Guarantee Reasoning for Simulation Conformance
Formalizing a JVML Verifier for Initialization in a Theorem Prover
Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings
The Inez Mathematical Programming Modulo Theories Framework
The UCLID Decision Procedure
There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
A Formally Verified Robustness Certifier for Neural Networks
Temporal Verification by Diagram Transformations
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
Btor2 , BtorMC and Boolector 3.0
Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking
JNuke: Efficient Dynamic Analysis for Java
An ACL2 Proof of Write Invalidate Cache Coherence
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement
Merit: An Interpolating Model-Checker
Automated Deduction and Formal Methods
A Conference Management System with Verified Document Confidentiality
Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists
Testing the Migration from Analog to Software-Based Railway Interlocking Systems
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
Contessa: Concurrency Testing Augmented with Symbolic Analysis
Model Checking LTL Using Net Unforldings
nekton: A Linearizability Proof Checker
Toward Liveness Proofs at Scale
End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
Cryptographic Protocol Verification via Supercompilation (A Case Study)
On Automatically Explaining Bisimulation Inequivalence
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
Safraless Compositional Synthesis
Maximum Satisfiability in Software Analysis: Applications and Techniques
Efficient Generation of Small Interpolants in CNF
Scaling GR(1) Synthesis via a Compositional Frameworkfor LTL Discrete Event Control
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I
Rewriting for Symbolic Execution of State Machine Models
Eager Abstraction for Symbolic Model Checking
Foundations of Fine-Grained Explainability
PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time
Timed Relational Abstractions for Sampled Data Control Systems
Model Checking Continuous-Time Markov Chains by Transient Analysis
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking
Effectively Propositional Interpolants
Regex Decision Procedures in Extended RE#
Model Checking Quantitative Hyperproperties
Joogie: Infeasible Code Detection for Java
Studying the Numerical Quality of an Industrial Computing Code: A Case Study on Code_aster
Theorem Proving Using Lazy Proof Explication
Abstraction for Shape Analysis with Fast and Precise Transformers
Reasoning over Permissions Regions in Concurrent Separation Logic
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT
STMC: Statistical Model Checker with Stratified and Antithetic Sampling
Temporal-Safety Proofs for Systems Code
Importance Splitting for Statistical Model Checking Rare Properties
Measuring with Timed Patterns
Self-correcting Neural Networks for Safe Classification
Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios
Reachability Analysis of Planar Multi-limear Systems
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Ticc: A Tool for Interface Compatibility and Composition
Finite-State Analysis of Security Protocols
Minimizing Running Costs in Consumption Systems
Automated Assumption Generation for Compositional Verification
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks
Constraint-Based Synthesis of Coupling Proofs
Elementary Microarchitecture Algebra
Formal Verification of Genetic Circuits
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets
Symbolic Optimal Reachability in Weighted Timed Automata
Symbolic Visibly Pushdown Automata
An Automata-Theoretic Approach to Fair Realizability and Synthesis
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
Recursive Data Structures in SPARK
BDD-Based Debugging Of Design Using Language Containment and Fair CTL
Compositional Value Iteration with Pareto Caching
All from One, One for All: on Model Checking Using Representatives
Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings
A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers
The NCSU Concurrency Workbench
A Work-Efficient Distributed Algorithm for Reachability Analysis
A Toolbox for the Analysis of Discrete Event Dynamic Systems
Falsification of Dynamical Systems - An Industrial Perspective
Decision Procedures for Sequence Theories
Shape Analysis via Second-Order Bi-Abduction
Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings
Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
Automatic Verification of Parameterized Synchronous Systems (Extended Abstract)
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java
Another Look at LTL Model Checking
Model Checking of macro Processes
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
Formal Methods for Conformance Testing: Theory Can Be Practical
Generating BDDs for Symbolic Model Checking in CCS
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Symbolic-Numeric Reachability Analysis of Hybrid Systems
Synthesizing Probabilistic Invariants via Doob's Decomposition
Check It Out: On the Efficient Formal Verification of Live Sequence Charts
A Tutorial on Satisfiability Modulo Theories
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols
Proving Termination of Probabilistic Programs Using Patterns
Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
Trust, Resilience and Interpretability of AI Models
Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Introducing Certificates to the Hardware Model Checking Competition
Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I
Searching for i-Good Lemmas to Accelerate Safety Model Checking
Protocol Verification in Nuprl
JayHorn: A Framework for Verifying Java programs
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party Computation
Learning Universally Quantified Invariants of Linear Data Structures
Complementing Büchi Automata with Ranker
Alternating RQ Timed Automata
CVC: A Cooperating Validity Checker
TRIM: A Tool for Triggered Message Sequence Charts
Structural Symmetry and Model Checking
An Evaluation of Monte-Carlo Tree Search for Property Falsification on Hybrid Flight Control Laws
Differentiable Logics for Neural Network Training and Verification
An Intermediate Program Representation for Optimizing Stream-Based Languages
Invited Tutorial: Verification of Infinite-State and Parameterized Systems
AGVI - Automatic Generation, Verification, and Implementation of Security Protocols
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
WSAT: A Tool for Formal Analysis of Web Services
Abstract Interpretation with Unfoldings
Randomized Algorithms for Program Analysis and Verification
POPACheck: A Model Checker for Probabilistic Pushdown Automata
PSI: Exact Symbolic Inference for Probabilistic Programs
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis
Efficient Verification with BDDs using Implicitly Conjoined Invariants
Verifying Hyperliveness
Conformance Checking for Models of Asynchronous Message Passing Software
Structural Abstraction of Software Verification Conditions
Property Directed Self Composition
Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms
Minimizing Generalized Büchi Automata
CSolve: Verifying C with Liquid Types
Alchemist: Learning Guarded Affine Functions
Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Haifa, Israel, July 31 - August 1, and August 11, 2022, Proceedings
Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings
Automatic Verification of Abstract State Machines
Minimal Multi-Layer Modifications of Deep Neural Networks
On the Automatic Computation of Network Invariants
Realizability and Synthesis of Reactive Modules
Automated Verification of Consistency in Zero-Knowledge Proof Circuits
Boosting k-Induction with Continuously-Refined Invariants
A Tool for Estimating Information Leakage
Populating the Peephole Optimizer of a Smart Contract Compiler
Disjunctive Interpolants for Horn-Clause Verification
Reactive Control Improvisation
Exploiting Symmetry In Temporal Logic Model Checking
Quantitative Information Flow: From Theory to Practice?
Verified Compilation of Space-Efficient Reversible Circuits
2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, Los Angeles, California, USA (Virtual Conference), July 20-21, 2020
Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving
The Verifiacation Problem for Safe Replaceability
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination
The PEP Tool
Deeply Optimizing the SAT Solver for the IC3 Algorithm
Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems
Functional Dependency for Verification Reduction
Adaptive Symmetry Reduction
Combining Model Checking and Theorem Proving to Verify Parallel Processes
Efficient Timing Analysis of a Class of Petri Nets
Generation of Reduced Models for Checking Fragments of CTL
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
Synthesis of Temporal Causality
SMT-Based Modular Analysis of Sequential Systems Code
Algorithmic Analysis of Nonlinear Hybrid Systems
Temporal Stream Logic: Synthesis Beyond the Bools
Verification Algorithms for Automated Separation Logic Verifiers
Software Verification in the Google App-Engine Cloud
Formal Verification - Applications & Case Studies
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations
G4LTL-ST: Automatic Generation of PLC Programs
Efficient Model Checking Via Büchi Tableau Automata
SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions
Monitoring Atomicity in Concurrent Programs
Lazy Annotation Revisited
Revamping TVLA: Making Parametric Shape Analysis Competitive
Formal Design and Safety Analysis of AIR6110 Wheel Brake System
Data-Driven Verification of Procedural Programs with Integer Arrays
Property Checking via Structural Analysis
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking
A Linear Time Process Algebra
Verification of Imperative Programs through Transformation of Constraint Logic Programs
The Spirit of Ghost Code
VPN: Verification of Poisoning in Neural Networks
Experience with Predicate Abstraction
Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models
Optimistic Value Iteration
TIPPtool: Compositional Specification and Analysis of Markovian Performance Models
Saving Space by Fully Exploiting Invisible Transitions
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
Microarchitecture Verification by Compositional Model Checking
Model Checking with Formula-Dependent Abstract Models
On Expansion and Resolution in CEGAR Based QBF Solving
Predictive Monitoring with Strong Trace Prefixes
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing
A Temporal Logic for Asynchronous Hyperproperties
Verification of Timed Systems Using POSETs
Model Checking Parameterized Asynchronous Shared-Memory Systems
Rigorous Reachability Analysis and Domain Decomposition of Taylor Models
Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop
TarTar: A Timed Automata Repair Tool
On Automation of CTL* Verification for Infinite-State Systems
Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study
Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract)
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL
Retrofitting Legacy Code for Security
Verification of a Multiplier: 64 Bits and Beyond
Automata vs Linear-Programming Discounted-Sum Inclusion
Monadic Decomposition
Action Language Verifier, Extended
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Gillian, Part II: Real-World Verification for JavaScript and C
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games
Reducing Test Inputs Using Information Partitions
Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems
Symbolic Resource Bound Inference for Functional Programs
Efficient Image Computation in Infinite State Model Checking
On Statistical Model Checking of Stochastic Systems
Synthesizing Number Transformations from Input-Output Examples
Proceedings of the Workshop on Games in Design and Verification, GDV@CAV 2004, Boston, MA, USA, June 18, 2004
Computing Differential Invariants of Hybrid Systems as Fixedpoints
The Top-Down Solver Verified: Building Confidence in Static Analyzers
Abstraction Refinement via Inductive Learning
A Decision Procedure for Bit-Vectors and Arrays
Synthesis of Super-Optimized Smart Contracts Using Max-SMT
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
Abstraction-Based Satisfiability Solving of Presburger Arithmetic
Model Checking Partial State Spaces with 3-Valued Temporal Logics
Scalable Bit-Blasting with Abstractions
A Case Study in Safety-Critical Design
Logical Clustering and Learning for Time-Series Data
Fast Computation of Strong Control Dependencies
Verification of Context-Free Timed Systems Using Linear Hybrid Observers
StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
The Real-Time Graphical Interval Logic Toolset
Repairing Decision-Making Programs Under Uncertainty
Exploiting Adjoints in Property Directed Reachability Analysis
Faster Than Uppaal?
Time-Aware Abstractions in HybridSal
Synthesis Through Unification
Minimum Satisfying Assignments for SMT
Centaur Technology Media Unit Verification
NNrepair: Constraint-Based Repair of Neural Network Classifiers
Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM
Syntactic Program Transformations for Automatic Abstraction
sfGPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
Verification by Behaviour Abstraction - A Case Study of Service Interaction Detection in Intelligent Telephone Networks
Requirements Validation for Hybrid Systems
Reasoning About Data Trees Using CHCs
Abstraction Based Model-Checking of Stability of Hybrid Systems
Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values
Deductive Program Repair
Abstract Analysis of Symbolic Executions
Canonical Prefixes of Petri Net Unfoldings
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
Lengths May Break Privacy - Or How to Check for Equivalences with Length
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
PET: An Interactive Software Testing Tool
FAST: Fast Acceleration of Symbolikc Transition Systems
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks
Supporting Standardization of Neural Networks Verification with VNNLIB and CoCoNet
Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms