yusuke1997/dblp-id-title huggingface dataset:
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints
Efficient Probabilistic Model Checking for Relational Reachability
Montre: A Tool for Monitoring Timed Regular Expressions
Using a Theorem Prover for Reasoning about Concurrent Algorithms
A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Towards Verifying the Bitcoin-S Library (Short Paper)
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Proving Conditional Termination
Constrained Dynamic Partial Order Reduction
A Simple Algorithm for Solving Qualitative Probabilistic Parity Games
Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints
A Practical Approach to Word Level Model Checking of Industrial Netlists
SAW: A Tool for Safety Analysis of Weakly-Hard Systems
SPT: Storyboard Programming Tool
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
Sound Approximation of Programs with Elementary Functions
cascade: C Assertion Checker and Deductive Engine
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
An Experiment in Parallelizing an Application Using Formal Methods
Getting Rid of Store-Buffers in TSO Analysis
Software Verification of Hyperproperties Beyond k-Safety
Formal Verification of VLIW Microprocessors with Speculative Execution
System Level Formal Verification via Model Checking Driven Simulation
Partial-Order Reduction in Symbolic State Space Exploration
Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods
Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors
Achieving Distributed Control through Model Checking
Model Checking Multi-Agent Programs with CASP
Decidable Synthesis of Programs with Uninterpreted Functions
Software Analysis and Model Checking
A Summary of Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels
Termination of Triangular Integer Loops is Decidable
Gist: A Solver for Probabilistic Games
Automating Separation Logic with Trees and Data
A Top Down Approach to the Formal Specification of SCI Cache Coherence
Homer: A Higher-Order Observational Equivalence Model checkER
ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification
Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics
Model Checking Conformance with Scenario-Based Specifications
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings
Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees
Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings
Synchronous and Bidirectional Component Interfaces
Refinement for Structured Concurrent Programs
Program Analysis Is Harder Than Verification: A Computability Perspective
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier
Markov Chains and Unambiguous Büchi Automata
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings
Loop Summarization with Rational Vector Addition Systems
TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems
Polyregular Model Checking
Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings
Verifying General Safety and Liveness Propterties with Integer Programming
The Mec 5 Model-Checker
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
Multi-solver Support in Symbolic Execution
Linear Completeness Thresholds for Bounded Model Checking
Formally Verified Switching Logic for Recoverability of Aircraft Controller
Transforming Event B Models into Verified C# Implementations
Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design
Delay Analysis in Synchronous Programs
CVC3
Liveness and Acceleration in Parameterized Verification
Practical Challenges for Industrial Formal Verification Tools
Linear Invariant Generation Using Non-linear Constraint Solving
Under-Approximating Loops in C Programs for Fast Counterexample Detection
Verification of an Audio Protocol with Bus Collision Using UPPAAL
Computing Bottom SCCs Symbolically Using Transition Guided Reduction
Efficient Monitoring of omega-Languages
Verifying Mobile Processes in the HAL Environment
RAT: A Tool for the Formal Analysis of Requirements
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification
An Antichain Algorithm for LTL Realizability
Mechanical Verification of an Ideal Incremental ABR Conformance
A Solver for Reachability Modulo Theories
CAVEAT: Technique and Tool for Computer Aided VErification And Transformation
Languages of Nested Trees
Inferring Congruence Equations Using SAT
Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings
AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Deriving Small Unsatisfiable Cores with Dominators
Generating Diagnostic Information for Behavioral Preorders
Ownership Guided C to Rust Translation
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
Automatic Generation and Validation of Instruction Encoders and Decoders
Data Structure Specifications via Local Equality Axioms
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata
A Semantic Driven Method to Check the Finiteness of CCS Processes
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
Verification of Floating-Point Adders
Temporal-Locig Queries
Satisfiability Modulo Finite Fields
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods
GenMC: A Model Checker for Weak Memory Models
Automatic Verification of Timed Circuits
Diagnosing Abstraction Failure for Separation Logic-Based Analyses
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs
Intra-module Inference
Structural Symbolic CTL Model Checking of Asynchronous Systems
An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic
Termination of Linear Programs
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
RV-Match: Practical Semantics-Based Program Analysis
BDD-Based Boolean Functional Synthesis
Inner and Outer Approximating Flowpipes for Delay Differential Equations
Norn: An SMT Solver for String Constraints
Nagini: A Static Verifier for Python
RATSY - A New Requirements Analysis Tool with Synthesis
Symmetry and Model Checking
Bounded Synthesis for Streett, Rabin, and \text CTL^*
Wolf - Bug Hunter for Concurrent Software Using Formal Methods
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
Alternative Approaches to Hardware Verification (abstract)
Strided Difference Bound Matrices
Complexity Results for POMSET Languages
Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)
Mutant Accuracy Testing for Assessing the Implementation of Numerical Algorithms
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties
Formal Verification of a Lazy Concurrent List-Based Set Algorithm
ParCoSS: Efficient Parallelized Compiled Symbolic Simulation
Compositional Abstraction for Timed Systems with Broadcast Synchronization
Robustness Verification of Quantum Classifiers
Finding Instability in Biological Models
Limit-Deterministic Büchi Automata for Linear Temporal Logic
Functional Extension of Symbolic Model Checking
Models and Proofs of Protocol Security: A Progress Report
Realizing ømega-regular Hyperproperties
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II
Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Benefits of Bounded Model Checking at an Industrial Setting
Verifying Global Neural Network Specifications using Hyperproperties
KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs
Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement
Using Optimal Simulations to Reduce Reachability Graphs
Symmetry Reduction for Probabilistic Model Checking
PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
Induction in Compositional Model Checking
Concrete Model Checking with Abstract Matching and Refinement
Termination Analysis with Calling Context Graphs
Adam: Causality-Based Synthesis of Distributed Systems
Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning
Inferring Inductive Invariants from Phase Structures
Cogent: Accurate Theorem Proving for Program Verification
µcke - Efficient µ-Calculus Model Checking
Time Robustness in MTL and Expressivity in Hybrid System Falsification
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Example Guided Synthesis of Linear Approximations for Neural Network Verification
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
Boolean Abstraction for Temporal Logic Satisfiability
Symbolic Model Checking Using Algebraic Geometry
Adaptive Concretization for Parallel Program Synthesis
Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings
Algorithmic Verification of Invalidation-Based Protocols
Exploiting Synchrony and Symmetry in Relational Verification
Quantitative Temporal Reasoning
The MathSAT 4SMT Solver
Priority Scheduling of Distributed Systems Based on Model Checking
To Store or Not to Store
SAFARI: SMT-Based Abstraction for Arrays with Interpolants
Automatic Translation of Natural Language System Specifications
A Fast Bisimulation Algorithm
TASS: Timing Analyzer of Scenario-Based Specifications
From Programs to Interpretable Deep Models and Back
Extension of the Karp and Miller Procedure to Lotos Specifications
Compressing Transitions for Model Checking
VPT 2014. Second International Workshop on Verification and Program Transformation, July 17-18, 2014, Vienna, Austria, The workshop is an event of the Vienna Summer of Logic 2014 and it is co-located with the 26th International Conference on Computer Aided Verification CAV 2014
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs
Quantifier Elimination by Lazy Model Enumeration
Automated Inductive Verification of Parameterized Protocols
Distributing Timed Model Checking - How the Search Order Matters
Producing Short Counterexamples Using "Crucial Events"
Marella: A Tool for Simulation and Verification
Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic
A Storm is Coming: A Modern Probabilistic Model Checker
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle
Functional Verification of Power Gated Designs by Compositional Reasoning
Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems
The Algebraic Feedback Product of Automata
Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs
Parameterized Verification of Infinite-State Processes with Global Conditions
Verification of timing Properties of VHDL
Mechanically Verifying a Family of Multiplier Circuits
A Method for Symbolic Computation of Abstract Operations
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation
Avoiding State Exposion by Composition of Minimal Covering Graphs
SAT-Based Compositional Verification Using Lazy Learning
DPLL( T): Fast Decision Procedures
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework
SMT-COMP: Satisfiability Modulo Theories Competition
Small Decision Trees for MDPs with Deductive Synthesis
Quantifying Conformance Using the Skorokhod Metric
Verification of Parameterized Systems by Dynamic Induction on Diagrams
Computer Assistance for Program Refinement
Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS
Solving Existentially Quantified Horn Clauses
Efficient Model Checking Using Tabled Resolution
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
A Toolset for Message Sequence Charts
AVATAR: The Architecture for First-Order Theorem Provers
On the Termination of Positive Supercompilation
Abstraction for Falsification
Fifteen Years of Viper
Programs with Lists Are Counter Automata
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
On Decidability of Prebisimulation for Timed Automata
Towards Distributed Software Model-Checking Using Decision Diagrams
Automated Analyses of IOT Event Monitoring Systems
APEX: An Analyzer for Open Probabilistic Programs
Exercises in Nonstandard Static Analysis of Hybrid Systems
Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
A Hybrid Model for Reasoning about Composed Hardware Systems
Layering Techniques for Development of Parallel Systems
Certifying Certainty and Uncertainty in Approximate Membership Query Structures
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
You Assume, We Guarantee: Methodology and Case Studies
MaxSMT-Based Type Inference for Python 3
Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks
On Checking Model Checkers
On Model-Checking for Fragments of µ-Calculus
The Zonotope Abstract Domain Taylor1+
Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking
Reasoning About TSO Programs Using Reduction and Abstraction
Counterexample-Guided Abstraction Refinement
Synthesis with Abstract Examples
SMC: A Symmetry Based Model Checker for Verification of Liveness Properties
Automata-Based Model Counting for String Constraints
A Scalable Shannon Entropy Estimator
Inter-Blockchain Protocols with the Isabelle Infrastructure Framework
Automating Most Parts of Hardware Proofs in HOL
Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution
Transactional Memory: Glimmer of a Theory
Discriminative Model Checking
Reflections on Termination of Linear Loops
Finite Model Finding in SMT
How to Prove Algorithms Linearisable
Bounded Model Checking for Weak Alternating Büchi Automata
A SAT-Based Counterexample Guided Method for Unbounded Synthesis
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II
Fast Acceleration of Ultimately Periodic Relations
An Automata-Theoretic Approach to Reasoning about Infinite-State Systems
Model Generation for Quantified Formulas: A Taint-Based Approach
A Model Checker for Hierarchical Probabilistic Real-Time Systems
Decomposing the Proof of Correctness of pipelined Microprocessors
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving
Model Based Automatic Code Generation for Nonlinear Model Predictive Control
Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Beautiful Interpolants
Reachability Analysis Using Message Passing over Tree Decompositions
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis
INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
Guiding Enumerative Program Synthesis with Large Language Models
Sound Numerical Computations in Abstract Acceleration
Engineering a Static Verification Tool for GPU Kernels
FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
A Concurrent Portfolio Approach to SMT Solving
From Data Structure to Process Structure
T(O)RMC: A Tool for (omega)-Regular Model Checking
From LTL to Deterministic Automata: A Safraless Compositional Approach
Model Checking Linear Properties of Prefix-Recognizable Systems
LEVER: A Tool for Learning Based Verification
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
Robust Probabilistic Bisimilarity for Labelled Markov Chains
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
Mechanizing Proofs of Computation Equivalence
First International Workshop on Verification and Program Transformation, VPT 2013, Saint Petersburg, Russia, July 12-13, 2013
Branching Bisimulation Learning
Systematic Generation of Diverse Benchmarks for DNN Verification
Code2Inv: A Deep Learning Framework for Program Verification
Using On-The-Fly Verification Techniques for the Generation of test Suites
A Complete Finite Prefix for Process Algebra
A Practical Approach to Coverage in Model Checking
Normed Simulations
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
Systematic Asynchrony Bug Exploration for Android Apps
Verification of Deep Convolutional Neural Networks Using ImageStars
MGSyn: Automatic Synthesis for Industrial Automation
Verifying the Safety of a Practical Concurrent Garbage Collector
3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, Los Angeles, California, USA (Virtual Conference), July 18-19, 2021
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
Compositional Model Checking with Incremental Counter-Example Construction
Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
Abstraction and BDDs Complement SAT-Based BMC in DiVer
Fast Termination and Workflow Nets
The Static Driver Verifier Research Platform
On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes
I/O Efficient Accepting Cycle Detection
BoSy: An Experimentation Framework for Bounded Synthesis
Three-Valued Abstraction for Continuous-Time Markov Chains
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic
HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment
Towards Contract Modules for the Tezos Blockchain (Short Paper)
Bridging the Gap between Fair Simulation and Trace Inclusion
QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols
Automatic verification of Pipelined Microprocessor Control
Authenticated Data Structures as Functors in Isabelle/HOL
Diffy: Inductive Reasoning of Array Programs Using Difference Invariants
Vac - Verifier of Administrative Role-Based Access Control Policies
ILP Modulo Theories
Proving Properties on PWA Systems Using Copositive and Semidefinite Programming
Learning Union of Integer Hypercubes with Queries - (with Applications to Monadic Decomposition)
Layered Concurrent Programs
Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis
Verifying Advanced Microarchitectures that Support Speculation and Exceptions
On the Almost-Sure Termination of Probabilistic Counter Programs
Proof-Guided Underapproximation Widening for Bounded Model Checking
Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
AIGEN: Random Generation of Symbolic Transition Systems
Symbolic Counter Abstraction for Concurrent Software
Shape Analysis for Composite Data Structures
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
Validation of Abstract Side-Channel Models for Computer Architectures
SLAyer: Memory Safety for Systems-Level Code
Split Gröbner Bases for Satisfiability Modulo Finite Fields
Automated Parameterized Verification of CRDTs
Full LTL Synthesis over Infinite-State Arenas
MCK: Model Checking the Logic of Knowledge
A Verifier and Timing Analyser for Simple Imperative Programs (Abstract)
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems
Workshop on Software Model Checking 2001, in connection with CAV 2001, Paris, France, July 23, 2001
Efficient Local Correctness Checking
Fair Simulation Minimization
Automatic Abstraction Using Generalized Model Checking
A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties
Localized Attractor Computations for Infinite-State Games
The Proof Complexity of SMT Solvers
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games
From Duration Calculus To Linear Hybrid Automata
Monitorability of Stochastic Dynamical Systems
Supervisory Control of Finite State Machines
Efficient Büchi Automata from LTL Formulae
Approximately Bisimilar Symbolic Models for Digital Control Systems
Iterating Transducers in the Large (Extended Abstract)
Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form
An Automata Theoretic Approach to Temporal Logic
A Direct Encoding for NNC Polyhedra
Software Documentation and the Verification Process
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
Sliding Window Abstraction for Infinite Markov Chains
Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols)
Predicting a Correct Program in Programming by Example
Model Checking Race-Freedom When "Sequential Consistency for Data-Race-Free Programs" is Guaranteed
Verifying the SRT Division Algorithm Using Theorem Proving Techniques
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT
Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
On Extending Bounded Proofs to Inductive Proofs
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded
SpaceEx: Scalable Verification of Hybrid Systems
Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach
Termination Analysis of Probabilistic Programs Through Positivstellensatz's
Efficient Verification of Parallel Real-Time Systems
Computing Abstractions of Infinite State Systems Compositionally and Automatically
Gradual Consistency Checking
Model-Free Reinforcement Learning for Branching Markov Decision Processes
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Proving More Properties with Bounded Model Checking
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I
Automated Unbounded Verification of Security Protocols
Verifying Timed Behavior Automata with Nonbinary Delay Constraints
Automated Resource Analysis with Coq Proof Objects
Foundations and Tools for the Static Analysis of Ethereum Smart Contracts
Summing up Smart Transitions
Predicate Abstraction via Symbolic Decision Procedures
Automating Separation Logic Using SMT
Alternate and Learn: Finding Witnesses without Looking All over
Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior
SCR*: A Toolset for Specifying and Analyzing Software Requirements
Recursive Program Synthesis
Computing Distinguishing Formulas for Branching Bisimulation
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement
Soufflé: On Synthesis of Program Analyzers