yusuke1997/dblp-id-title huggingface dataset:
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I
AutoQ: An Automata-Based Quantum Circuit Verifier
Structural Synthesis for GXW Specifications
Relaxed Visibility Enhances Partial Order Reduction
The MoXI Model Exchange Tool Suite
Evidence Explorer: A Tool for Exploring Model-Checking Proofs
Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers
UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis
Application of Formal Word-Level Analysis to Constrained Random Simulation
Automatic Verification of Stability and Safety for Delay Differential Equations
Process Equivalence Problems as Energy Games
Semantic Adversarial Deep Learning
Regular Model Checking for LTL(MSO)
Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
GOAL for Games, Omega-Automata, and Logics
Online Causation Monitoring of Signal Temporal Logic
Modular Verification of SRT Division
Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations
Panini: An Efficient and Flexible Knowledge Compiler
Constraint-Based Relational Verification
Program Verification Under Weak Memory Consistency Using Separation Logic
Accelerating Automated Program Verifiers by Automatic Proof Localization
An Improved Algorithm for the Evaluation of Fixpoint Expressions
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
Duet: Static Analysis for Unbounded Parallelism
HybridSAL Relational Abstracter
Iterating Transducers
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II
Causal Atomicity
Algorithmic Improvements in Regular Model Checking
Synthesizing JIT Compilers for In-Kernel DSLs
Models Whose Checks Don't Explode
The Power of Hybrid Acceleration
Why Model Checking Can Improve WCET Analysis
On-the-Fly Verification with Stubborn Sets
Branching Processes of Conservative Nested Petri Nets
State Space Reduction by Proving Confluence
Synthia: Verification and Synthesis for Timed Automata
The Barcelogic SMT Solver
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing
An Abstraction Algorithm for the Verification of Generalized C-Slow Designs
The VerCors Verifier: A Progress Report
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I
Verification of Real-Time Systems Using PVS
Dsolve: Safety Verification via Liquid Types
Model Counting for Recursively-Defined Strings
Ymer: A Statistical Model Checker
Synthesis with Asymptotic Resource Bounds
Quantitative Supermartingale Certificates
Higher-Level Specification and Verification with BDDs
Local Verification of Global Invariants in Concurrent Programs
OpenNWA: A Nested-Word Automaton Library
Synthesizing Reactive Systems from Hyperproperties
Analysis of Timed Systems Based on Time-Abstracting Bisimulation
Verification of Arithmetic Circuits by Comparing Two Similar Circuits
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
BigraphER: Rewriting and Analysis Engine for Bigraphs
Qlose: Program Repair with Quantitative Objectives
Parametric and Sliced Causality
Progressive Reasoning over Recursively-Defined Strings
Acacia+, a Tool for LTL Synthesis
Reduce the Complexity of the Polyhedron Minimization Using the Max Plus Pruning Method
Enforcing Almost-Sure Reachability in POMDPs
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony
Local Proofs for Linear-Time Properties of Concurrent Programs
Symbolic Liveness Analysis of Real-World Software
Abstraction Modulo Stability for Reverse Engineering
Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach
Toupie = µ-Calculus + Constraints
A Two-Level Formal Verification Methodology using HOL and COSMOS
Integrating WS1S with PVS
Terminator: Beyond Safety
Probabilistic Access Policies with Automated Reasoning Support
Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Indexed Predicate Discovery for Unbounded System Verification
Rob Tristan Gerth: 1956?2003
Practical Methods for Proving Program Termination
A Scalable and Nearly Uniform Generator of SAT Witnesses
Interactive Theorem Proving Modulo Fuzzing
Neural Networks in Imandra: Matrix Representation as a Verification Choice
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement
Simplifying Loop Invariant Generation Using Splitter Predicates
Processor Verification with Precise Exeptions and Speculative Execution
Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling
A Proof Assistant for Symbolic Model-Checking
Translation Validation: From Simulink to C
Verifying omega-Regular Properties of Markov Chains
A Graphical Interval Logic Toolset for Verifying Concurrent Systems
Delay-Bounded Scheduling Without Delay!
Efficient Anytime Techniques for Model-Based Safety Analysis
Ten Years of Partial Order Reduction
Verifying Fault-Tolerance of Quantum Error Correction Codes
PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols
Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Java Bytecode Verification: An Overview
A Cascade of Checkers for Run-time Certification of Local Robustness
Synthesis of Asynchronous Reactive Programs from Temporal Specifications
Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
Program Sketching by Automatically Generating Mocks from Tests
Algorithmic Algebraic Model Checking I: Challenges from Systems Biology
Efficient Scenario Verification for Hybrid Automata
Dynamic Cutoff Detection in Parameterized Concurrent Programs
Causal Termination of Multi-threaded Programs
Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic
Repair of Boolean Programs with an Application to C
An Algebra of Boolean Processes
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
TLQSolver: A Temporal Logic Query Checker
The State of SPIN
Formally Verified EVM Block-Optimizations
Counterexamples with Loops for Predicate Abstraction
Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations
Tuning SAT Checkers for Bounded Model Checking
Range Allocation for Separation Logic
Quantified Invariants via Syntax-Guided Synthesis
DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs
Romeo: A Tool for Analyzing Time Petri Nets
Interface Compatibility Checking for Software Modules
Stutter-Invariant Languages, omega-Automata, and Temporal Logic
Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II
Enhancing Program Verification with Lemmas
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems
Compositional Checking of Satisfaction
Modular Deductive Verification of Multiprocessor Hardware Designs
Monitoring Weak Consistency
Fast Approximations of Quantifier Elimination
FoCs: Automatic Generation of Simulation Checkers from Formal Specifications
SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability
Symbolic Model Checking with Rich ssertional Languages
Assume-Guarantee Refinement Between Different Time Scales
Widening Arithmetic Automata
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Automated Parameterized Verification of a Railway Protection System with Dafny
AliveInLean: A Verified LLVM Peephole Optimization Verifier
On Unfolding for Programs Using Strings as a Data Type
IF-2.0: A Validation Environment for Component-Based Real-Time Systems
Monitoring CTMCs by Multi-clock Timed Automata
Hitting Families of Schedules for Asynchronous Programs
CVC Lite: A New Implementation of the Cooperating Validity Checker Category B
FORQ-Based Language Inclusion Formal Testing
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Semi-external LTL Model Checking
Partial-Order Model Checking: A Guide for the Perplexed
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries
Poling: SMT Aided Linearizability Proofs
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings
Numerical Software Verification - 12th International Workshop, NSV@CAV 2019, New York City, NY, USA, July 13-14, 2019, Proceedings
Programs from Proofs - A PCC Alternative
Verification of a Chemical Process Leak Test Procedure
Mechanical Mathematical Methods for Microprocessor Verification
Veil: A Framework for Automated and Interactive Verification of Transition Systems
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems
Communication-Closed Asynchronous Protocols
An Automated Proof Technique for Finite-State Machine Equivalence
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
PathFinder: A Tool for Design Exploration
Quantitative Assume Guarantee Synthesis
Efficient Analysis of Cyclic Definitions
Model Checking of Linearizability of Concurrent List Implementations
μZ - An Efficient Engine for Fixed Points with Constraints
Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned
Solving Parity Games via Priority Promotion
Abstraction-Refinement for Hierarchical Probabilistic Models
Efficient Model Checking by Automated Ordering of Transition Relation Partitions
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
Verification of Certifying Computations
Generating BDD Models for Process Algebra Terms
Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Bounded Underapproximations
The rIC3 Hardware Model Checker
Bug-Assist: Assisting Fault Localization in ANSI-C Programs
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Towards Model Checking Real-World Software-Defined Networks
Rely-Guarantee Reasoning for Causally Consistent Shared Memory
Computer Aided Verification, 6th International Conference, CAV '94, Stanford, California, USA, June 21-23, 1994, Proceedings
Comparison Under Abstraction for Verifying Linearizability
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Termination Analysis with Algorithmic Learning
Parallelising Symbolic State-Space Generators
On Polynomial-Size Programs Winning Finite-State Games
Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata
Leveraging Interpolant Strength in Model Checking
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking
Fast Algorithms for Handling Diagonal Constraints in Timed Automata
Hierarchical Representations of Discrete Functions, with Application to Model Checking
Trace Table Based Approach for Pipeline Microprocessor Verification
ACTL ∩ LTL Synthesis
STARI: A Case Study in Compositional and Hierarchical Timing Verification
Runtime Monitoring with Recovery of the SENT Communication Protocol
DNNV: A Framework for Deep Neural Network Verification
Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Array Abstractions from Proofs
The nuXmv Symbolic Model Checker
Run-Time Optimization for Learned Controllers Through Quantitative Games
Symbolic Monitoring Against Specifications Parametric in Time and Data
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
Efficient Timed Reachability Analysis Using Clock Difference Diagrams
Verification of an Advanced mips-Type Out-of-Order Execution Algorithm
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper)
Hector: An Equivalence Checker for a Higher-Order Fragment of ML
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
Prediction and Control of Stochastic Agents Using Formal Methods
Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract)
SPeeDI - A Verification Tool for Polygonal Hybrid Systems
Verifying Fairness in Quantum Machine Learning
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types
Permission Inference for Array Programs
InVeST: A Tool for the Verification of Invariants
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
Incremental Instance Generation in Local Reasoning
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Transformation-Based Verification Using Generalized Retiming
Compositional Synthesis of Reactive Controllers for Multi-agent Systems
The Concurrency Factory: A Development Environment for Concurrent Systems
Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic
A Study of Model-Order Reduction Techniques for Verification
Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification
Porous Invariants
The Completeness of a Hardware Inference System
Abstraction and Counterexample-Guided Construction of omega -Automata for Model Checking of Step-Discrete Linear Hybrid Models
Must Fault Localization for Program Repair
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract)
The Open-Source LearnLib - A Framework for Active Automata Learning
A Misconception-Driven Adaptive Tutor for Linear Temporal Logic
Automatic Abstraction Techniques for Propositional µ-calculus Model Checking
Shrinktech: A Tool for the Robustness Analysis of Timed Automata
ICS: Integrated Canonizer and Solver
Formally Certified Approximate Model Counting
Compositional Analysis of Floating-Point Linear Numerical Filters
Hector: Software Model Checking with Cooperating Analysis Plugins
LTL Learning on GPUs
Verifying Timed Behavior Automata with Input/Output Critical Races
Resolution Proofs and Skolem Functions in QBF Evaluation and Applications
Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability
An Iterative Approach to Language Containment
Suspension Automata: A Decidable Class of Hybrid Automata
Stepwise CTL Model Checking of State/Event Systems
InvGen: An Efficient Invariant Generator
Verification of Fair Transisiton Systems
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
INFAMY: An Infinite-State Markov Model Checker
Finite Instantiations in Equivalence Logic with Uninterpreted Functions
QUAIL: A Quantitative Security Analyzer for Imperative Code
Local and Compositional Reasoning for Optimized Reactive Systems
A Partition Refinement Algorithm for the pi -Calculus (Extended Abstract)
R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software
Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Mixed-Signal System Verification: A High-Speed Link Example
Scaling Model Checking for Neural Network Analysis via State-Space Reduction and Input Segmentation
Improved Automata Generation for Linear Temporal Logic
Raven: An SMT-Based Concurrency Verifier
Compositional Specification and Model Checking in GSTE
A Compositional Rule for Hardware Design Refinement
Extrapolating Tree Transformations
Construction of Abstract State Graphs with PVS
Automated Safety Verification of Programs Invoking Neural Networks
A Theory of Restrictions for Logics and Automata
Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
Automatic Temporal Verification of Buffer Systems
The Compositional Specification of Timed Systems - A Tutorial
Neural Network Precision Tuning Using Stochastic Arithmetic
From Liveness to Promptness
Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP
Tableau Recycling
PESSOA: A Tool for Embedded Controller Synthesis
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
A BDD-Based Model Checker for Recursive Programs
Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic
Time for Statistical Model Checking of Real-Time Systems
Program Repair as a Game
First-Order Theorem Proving and Vampire
Stateless Model Checking for POWER
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
Under-Approximating Backward Reachable Sets by Polytopes
End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT
What's Wrong with On-the-Fly Partial Order Reduction
Formally Validating a Practical Verification Condition Generator
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Certified Private Inference on Neural Networks via Lipschitz-Guided Abstraction Refinement
Early Verification of Legal Compliance via Bounded Satisfiability Checking
Learning Boolean Functions Incrementally
Expand, Enlarge and Check... Made Efficient
Validating a Modern Microprocessor
Model Checking Recursive Programs with Numeric Data Types
IF: A Validation Environment for Timed Asynchronous Systems
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
Reachability and Recurrence in Extended Finite State Machines: Modular Vector Addition Systems
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
Synchronous Programming of Reactive Systems
Jakstab: A Static Analysis Platform for Binaries
JVer: A Java Verifier
Global Model-Checking of Infinite-State Systems
Real-Time System Verification using P/T Nets
Deductive Verification of Advanced Out-of-Order Microprocessors
Maximum Causal Entropy Specification Inference from Demonstrations
RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
CacBDD: A BDD Package with Dynamic Cache Management
Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract)
Temporal Precondition Verification of Design Transformations
2003 Workshop on Software Model Checking, SoftMC 2003, Boulder, Colorado, USA, July 14, 2003
Jtlv: A Framework for Developing Verification Algorithms
Formal Replay of Translation Validation for Highly Optimised C
From Pre -historic to Post -modern Symbolic Model Checking
Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis
The d/dt Tool for Verification of Hybrid Systems
Formula-Dependent Equivalence for Compositional CTL Model Checking
Partial Order Aware Concurrency Sampling
Debugging Network Reachability with Blocked Paths
Design Constraints in Symbolic Model Checking
When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-agent Protocol
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Linear Arithmetic with Stars
TVOC: A Translation Validator for Optimizing Compilers
A Verification Procedure via Invariant for Extended Communicating Finite-State Machines
Word-Level Symbolic Trajectory Evaluation
The JKind Model Checker
Automated Synthesis of Secure Platform Mappings
Automatic Verification of Combinatorial and Pipelined FFT
Distributed Symbolic Model Checking for µ-Calculus
Security-Aware Synthesis Using Delayed-Action Games
Synthesis of Masking Countermeasures against Side Channel Attacks
Using Interface Refinement to Integrate Formal Verification into the Design Cycle
STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis
QMC: A Model Checker for Quantum Systems
Pushdown Processes: Games and Model Checking
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I
$\mathbf{{\textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis
Model Checking Based on Sequential ATPG
Synthesis and Some of Its Challenges
Satisfiability Checking for Mission-Time LTL
Interpolant-Based Transition Relation Approximation
A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal?
An SMT-Based Approach to Coverability Analysis
AMC: An Adaptive Model Checker
Complete Formal Hardware Verification of Interfaces for a FlexRay-Like Bus
Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings
String Constraints for Verification
Synthesizing Fair Decision Trees via Iterative Constraint Solving
Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits
Latency Insensitive Protocols
Introduction to the IEEE 1788-2015 Standard for Interval Arithmetic
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants
StringFuzz: A Fuzzer for String Solvers
Tree Buffers
Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings
Verified Computations Using Taylor Models and Their Applications
TRACER: A Symbolic Execution Tool for Verification
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
D-Finder: A Tool for Compositional Deadlock Detection and Verification
Lazy Abstraction with Interpolants
Linear Ranking with Reachability
Smoothing a Program Soundly and Robustly
Spade: Verification of Multithreaded Dynamic and Recursive Programs
LearnLib: 10 years later
Efficient Modeling of Embedded Memories in Bounded Model Checking
What's Hard About Boolean Functional Synthesis?
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I
Robustness in the Presence of Liveness
PrIC3: Property Directed Reachability for MDPs
Module Checking Revisited
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I
Equivalence of Extended Symbolic Finite Transducers
Verifying Low-Level Implementations of High-Level Datatypes
Games through Nested Fixpoints
Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
Model-Checking Structured Context-Free Languages
Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems
Coping with Outside-the-Box Attacks
HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols
The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach
Kratos - A Software Model Checker for SystemC
A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract)
On the Formal Verification of the Stellar Consensus Protocol
Violat: Generating Tests of Observational Refinement for Concurrent Objects
Constraint-Based Approach for Analysis of Hybrid Systems
Automated and Modular Refinement Reasoning for Concurrent Programs
Deciding Local Theory Extensions via E-matching
Delta-Decision Procedures for Exists-Forall Problems over the Reals
On the Competeness of Compositional Reasoning
Bit-Vector Rewriting with Automatic Rule Generation
A Practical Verification Framework for Preemptive OS Kernels
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Sound Automation of Magic Wands
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II
Automatic Completion of Distributed Protocols with Symmetry