yusuke1997/dblp-id-title huggingface dataset:
A Type-Directed Approach to Program Repair
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion
Boolean Abstractions for Realizability Modulo Theories
Proving Non-termination Using Max-SMT
MOCHA: Modularity in Model Checking
SecCSL: Security Concurrent Separation Logic
Bitwuzla
PROPhESY: A PRObabilistic ParamEter SYnthesis Tool
From Cardiac Cells to Genetic Regulatory Networks
CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs
Detecting Fair Non-termination in Multithreaded Programs
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver
libalf: The Automata Learning Framework
The Mobility Workbench - A Tool for the pi-Calculus
Model Checking ømega-Regular Properties with Decoupled Search
PAPETRI: Environment for the Analysis of Petri Nets
BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks
Model-Checking for Real-Time Systems Specified in Lotos
Termination Analysis with Compositional Transition Invariants
Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations
Performance Improvement of State Space Exploration by Regular & Diffrential Hashing Functions
Proving Unrealizability for Syntax-Guided Synthesis
Automating Induction for Solving Horn Clauses
Counterexample-Guided Commutativity
Programmable Program Synthesis
Symbolic Verification with Periodic Sets
Safety Verification of Deep Neural Networks
Improving Language Containment Using Fairness Graphs
HMC: Verifying Functional Programs Using Abstract Interpreters
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems
Numerical Software Verification - 9th International Workshop, NSV 2016, Toronto, ON, Canada, July 17-18, 2016, [collocated with CAV 2016], Revised Selected Papers
jMoped: A Test Environment for Java Programs
Formal Analysis of Java Programs in JavaFAN
A Fast Linear-Arithmetic Solver for DPLL(T)
An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)
Verification of a Distributed Cache Memory by Using Abstractions
CPAchecker: A Tool for Configurable Software Verification
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification
Hybrid Acceleration Using Real Vector Automata (Extended Abstract)
Proving Termination Starting from the End
On Using Protean To Verify ISO FTAM Protocol
Temporal Property Verification as a Program Analysis Task
Space Explanations of Neural Network Classification
Heap Assumptions on Demand
EVP: Integration of FDTs for the Analysis and Verification of Communication Protocols
Distributed Explicit State Model Checking of Deadlock Freedom
Probabilistic Automated Language Learning for Configuration Files
Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification
On Synthesizing Controllers from Bounded-Response Properties
Fast and Generalized Polynomial Time Memory Consistency Verification
Model Checking the World Wide Web
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Don't Care Words with an Application to the Automata-Based Approach for Real Addition
Deterministic Automata for the (F, G)-Fragment of LTL
A Nonlinear Real Arithmetic Fragment
Root Causing Linearizability Violations
Verifying Quantitative Real-Time Properties of Synchronous Programs
Monitoring Temporal Rules Combined with Time Series
µCRL: A Toolset for Analysing Algebraic Specifications
Lazy Shape Analysis
STLmc: Robust STL Model Checking of Hybrid Systems Using SMT
Verification of Parameterized Bus Arbitration Protocol
Component-Based Construction of Real-Time Systems in BIP
Software Transactional Memory on Relaxed Memory Models
Learning a Static Analyzer from Data
Verifying Tree-Manipulating Programs via CHCs
Efficient Sensitivity Analysis for Parametric Robust Markov Chains
Automatic Datapath Abstraction In Hardware Systems
Avoiding the Shoals - A New Approach to Liveness Checking
Automated Verification of Monotonic Data Structure Traversals in C
Yices 2.2
Interpolation-Based Software Verification with Wolverine
Saturn: A SAT-Based Tool for Bug Detection
Enhanced Vacuity Detection in Linear Temporal Logic
Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings
Parametric Circuit Representation Using Inductive Boolean Functions
Ground Temporal Logic: A Logic for Hardware Verification
Compositional Model Checking for Linear-Time Temporal Logic
Abstracting C with abC
Test Coverage for Continuous and Hybrid Systems
Regular Reinforcement Learning
Model Checking Multithreaded Programs with Asynchronous Atomic Methods
Fine-Grained Caching of Verification Results
The DEEPSEC Prover
Kratos2: An SMT-Based Model Checker for Imperative Programs
Forest Automata for Verification of Heap Manipulation
Learning Abstractions for Program Synthesis
Generating Litmus Tests for Contrasting Memory Consistency Models
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
Synthesizing Programs with Constraint Solvers
Timed Control with Partial Observability
Bounded Model Checking of Concurrent Programs
Low-Level Library Analysis and Summarization
Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
soid: A Tool for Legal Accountability for Automated Decision Making
Crocos: An Integrated Environment for Interactive Verification of SDL Specifications
Fast Interpolating BMC
Manthan: A Data-Driven Approach for Boolean Function Synthesis
CSIsat: Interpolation for LA+EUF
Arithmetic Solving in Z3
Checking Robustness Against Snapshot Isolation
Distilling Constraints in Zero-Knowledge Protocols
Counter Example Guided Reactive Synthesis for LTL Modulo Theories *
Automated Analysis of an Audio Control Protocol
Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs
Ranking Functions for Linear-Constraint Loops
Towards Verified Price Oracles for Decentralized Exchange Protocols
Some Complexity Results for SystemVerilog Assertions
Unfoldings of Unbounded Petri Nets
Singularity: Designing Better Software (Invited Talk)
A Modal Logic for Message passing Processes (Extended Abstract)
Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
SPEED: Symbolic Complexity Bound Analysis
Automatic Verification of Floating-Point Accumulation Networks
THOR: A Tool for Reasoning about Shape and Arithmetic
Recent Developments in FDR
Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings
On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Guessing Winning Policies in LTL Synthesis by Semantic Learning
Modular Abstractions for Verifying Real-Time Distributed Systems
STLInspector: STL Validation with Guarantees
Correcting a Space-Efficient Simulation Algorithm
Computing Accumulated Delays in Real-time Systems
Ranking Automata and Games for Prioritized Requirements
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings
CADP - A Protocol Validation and Verification Toolbox
NuSMV 2: An OpenSource Tool for Symbolic Model Checking
JavaSMT 3: Interacting with SMT Solvers in Java
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking
Efficient Synthesis with Probabilistic Constraints
Software Model Checking for People Who Love Automata
Interpolants as Classifiers
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
Unblocking Dynamic Partial Order Reduction
Efficient Robust Monitoring for STL
Beyond Model Checking
SAL 2
Verification via Structure Simulation
Clock Bound Repair for Timed Systems
Thread Quantification for Concurrent Shape Analysis
LLMC: Verifying High-Performance Software
Model Checking and Transitive-Closure Logic
MetaVal: Witness Validation via Verification
Explaining Counterexamples Using Causality
The Temporal Logic Sugar
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems
Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper
Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications
Shared Certificates for Neural Network Verification
Partial Orders for Efficient Bounded Model Checking of Concurrent Software
Verifying Systems with Infinite but Regular State Spaces
Powerful Techniques for the Automatic Generation of Invariants
C32SAT: Checking C Expressions
Cameleer: A Deductive Verification Tool for OCaml
Learning Commutativity Specifications
A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking
Symbolic Partial-Order Execution for Testing Multi-Threaded Programs
SVA and PSL Local Variables - A Practical Approach
Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?
Decidability of Bisimulation Equivalences for Parallel Timer Processes
mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
Using Types for Software Verification
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates
TReX: A Tool for Reachability Analysis of Complex Systems
Termination of Integer Linear Programs
General Anticipatory Runtime Verification
Automatic Program Instrumentation for Automatic Verification
Lookahead Widening
Verifying PETSc Vector Components Using CIVL
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II
LTSmin: Distributed and Symbolic Reachability
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
GPUDrano: Detecting Uncoalesced Accesses in GPU Programs
A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract
Rigorous Continuous Evolution of Uncertain Systems
Effective Program Verification for Relaxed Memory Models
Detecting Errors Before Reaching Them
A Structural Linearization Principle for Processes
Certifying the Fairness of KNN in the Presence of Dataset Bias
Automated Verification of Correctness for Masked Arithmetic Programs
Symbolic Equivalence Checking
Relational Hoare Logic for Realistically Modelled Machine Code
Regression-Free Synthesis for Concurrency
From Shape Analysis to Termination Analysis in Linear Time
Towards Performance Prediction of Compositional Models in Industrial GALS Designs
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
Building Circuits from Relations
Parameterized Verification with Automatically Computed Inductive Assertions
Interactive Synthesis of Code Snippets
Automata Learning from Preference and Equivalence Queries
Synthesizing Trajectory Queries from Examples
EASN: Integrating ASN.1 and Model Checking
An Abstraction-Based Framework for Neural Network Verification
Protocol Verification by Aggregation of Distributed Transactions
A Role for Theorem Proving in Multi-Processor Design
Program Repair without Regret
Monotonic Abstraction for Programs with Dynamic Memory Heaps
Checking Data-Race Freedom of GPU Kernels, Compositionally
Infinite Games and Verification (Extended Abstract of a Tutorial)
Validating Library Usage Interactively
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation
Symbolic Bounded Synthesis
Abstraction Refinement for Bounded Model Checking
Invertibility Conditions for Floating-Point Formulas
Efficient Detection of Vacuity in ACTL Formulaas
Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation
Certifying Model Checkers
3D Environment Modeling for Falsification and Beyond with Scenic 3.0
PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
Verifying Linearizability of Intel® Software Guard Extensions
A NuSMV Extension for Graded-CTL Model Checking
Policy Synthesis and Reinforcement Learning for Discounted LTL
Transforming Undecidable Synthesis Problems into Decidable Problems
Second-Order Hyperproperties
Scaling Up Proactive Enforcement
Regression Test Selection for Distributed Software Histories
Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers
Automatic Verification of Integer Array Programs
The Use of Model Checking in ATPG for Sequential Circuits
Petruchio: From Dynamic Networks to Nets
A Discrete Strategy Improvement Algorithm for Solving Parity Games
Calculating-Confluence Compositionally
Proofgold: Blockchain for Formal Methods
Verification of Real-Time Systems by Successive Over and Under Approximation
Cardinality Abstraction for Declarative Networking Applications
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools
Incremental Determinization for Quantifier Elimination and Functional Synthesis
Quantitative Synthesis for Concurrent Programs
On Discrete Modeling and Model Checking for Nonlinear Analog Systems
Local Liveness for Compositional Modeling of Fair Reactive Systems
Rounding Meets Approximate Model Counting
Abstract Regular Model Checking
Practical, Low-Effort Equivalence Verification of Real Code
Value Iteration for Long-Run Average Reward in Markov Decision Processes
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
Faster Algorithms for Markov Decision Processes with Low Treewidth
Theorem Proving for Verification (Invited Tutorial)
Verifying Asynchronous Interactions via Communicating Session Automata
Effectively-Propositional Reasoning about Reachability in Linked Data Structures
An Experimental Evaluation of Ground Decision Procedures
Using Coverage to Deploy Formal Verification in a Simulation World
An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems
A Verification Strategy for Timing-Constrained Systems
Collective Contracts for Message-Passing Parallel Programs
Incremental, Inductive CTL Model Checking
SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks
Software Model Checking via IC3
Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation
Regular Tree Model Checking
Efficient Symbolic Detection of Global Properties in Distributed Systems
Using Compositional Preorders in the Verification of Sliding Window Protocal
SR-SFLL: Structurally Robust Stripped Functionality Logic Locking
Automated Termination Proofs for Java Programs with Cyclic Data
Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints
Cutting the Mix
Lazy Self-composition for Security Verification
OptiMathSAT: A Tool for Optimization Modulo Theories
Vacuum Cleaning CTL Formulae
Scalable Polyhedral Verification of Recurrent Neural Networks
Verifying Properties of HMS Machine Specifications of Real-Time Systems
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Methodology and System for Practical Formal Verification of Reactive Hardware
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks
Verification of Tree Updates for Optimization
Logical Aspects of Cryptographic Protocol Verification, LACPV 2001, in connection with CAV 2001, Paris, France, July 23, 2001
Certifying Optimality of State Estimation Programs
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems
Are Timed Automata Updatable?
SDLcheck: A Model Checking Tool
Verified Numerical Methods for Ordinary Differential Equations
SMT-Based Model Checking for Recursive Programs
Improving Pushdown System Model Checking
Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
Polytopic Trees for Verification of Learning-Based Controllers
Non-polynomial Worst-Case Analysis of Recursive Programs
Lock Removal for Concurrent Trace Programs
Global rebuilding of OBDDs Avoiding Memory Requirement Maxima
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
Solving Quantified Bit-Vectors Using Invertibility Conditions
Secure Programming via Visibly Pushdown Safety Games
Boosting Few-Pixel Robustness Verification via Covering Verification Designs
An Axiomatic Memory Model for POWER Multiprocessors
Minimum and Maximum Delay Problems in Real-Time Systems
VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software
A Logical Product Approach to Zonotope Intersection
Local Model Checking for Real-Time Systems (Extended Abstract)
Systematic Acceleration in Regular Model Checking
Semi-formal Bounded Model Checking
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I
Automatic Termination Proofs for Programs with Shape-Shifting Heaps
Strengthening Invariants by Symbolic Consistency Testing
Arithmetizing Shape Analysis
From Invariant Checking to Invariant Inference Using Randomized Search
An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract)
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems
Bounded-memory Algorithms for Verification On-the-fly
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
Program Verification with Constrained Horn Clauses (Invited Paper)
Combining Relational Learning with SMT Solvers Using CEGAR
Memory Management in Concurrent Algorithms
GPU Acceleration of Bounded Model Checking with ParaFROST
Leaping Loops in the Presence of Abstraction
Underapproximation for Model-Checking Based on Random Cryptographic Constructions
Stability in Weak Memory Models
Parameterized Verification of Systems with Global Synchronization and Guards
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
SPLIT: A Compositional LTL Verifier
Engineering an Efficient Probabilistic Exact Model Counter
Automated Assume-Guarantee Reasoning by Abstraction Refinement
Efficient omega -Regular Language Containment
Apron: A Library of Numerical Abstract Domains for Static Analysis
Mechanized Formal Model of Bitcoin's Blockchain Validation Procedures
Symmetry Reduction in SAT-Based Model Checking
Algorithms for Interface Synthesis
Fences in Weak Memory Models
Synthesizing Approximate Implementations for Unrealizable Specifications
JBernstein: A Validity Checker for Generalized Polynomial Constraints
Approximate Counting of Minimal Unsatisfiable Subsets
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2 m )
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II
Automated Assume-Guarantee Reasoning through Implicit Learning
The METAFrame'95 Environment
Job-Shop Scheduling Using Timed Automata
Hybrid Systems: From Verification to Falsification
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Decidability of Hybrid Systems with Rectangular Differential Inclusion
Data-Driven Synthesis of Full Probabilistic Programs
Interpolating Property Directed Reachability
Symmetry and Reduced Symmetry in Model Checking
Domain-Specific Optimization in Automata Learning
The Industrial Success of Verification Tools Based on Stålmarck's Method
Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET
Supermartingale Certificates for Quantitative Omega-Regular Verification and Control
RuleBase: Model Checking at IBM
GSTE Is Partitioned Model Checking
Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study
Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings
Stratified Abstraction of Access Control Policies
Counting Minimal Unsatisfiable Subsets
Bounded Model Construction for Monadic Second-Order Logics
Sampling-Based Verification of CTMCs with Uncertain Rates
Meta-analysis for Atomicity Violations under Nested Locking
MDG Tools for the Verification of RTL Designs
A Proof-Carrying Code Architecture for Java
Incremental and Complete Bounded Model Checking for Full PLTL
On-the-Fly Model Checking of RCTL Formulas
Gobra: Modular Specification and Verification of Go Programs
Conflict-Driven Conditional Termination
Compositional Semantics of ESTEREL and Verification by Compositional Reductions
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion
sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses
SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation
Fast and Accurate Static Data-Race Detection for Concurrent Programs
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023
Towards Verifying Nonlinear Integer Arithmetic
Overfitting in Synthesis: Theory and Practice
Affine Loop Invariant Generation via Matrix Algebra
Malware Analysis with Tree Automata Inference
PARTY Parameterized Synthesis of Token Rings
Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
Handling Global Conditions in Parameterized System Verification
Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games
Verifying Safety Properties of Differential Equations
Angelic Verification: Precise Verification Modulo Unknowns
Formal Reasoning About the Security of Amazon Web Services
Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM
Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
Thread-Modular Abstraction Refinement
Decision Tree Learning in CEGIS-Based Termination Analysis
Algebraic Program Analysis
Formal Specifications on Industrial-Strength Code-From Myth to Reality
Building trustworthy refactoring tools
Synthesizing Biological Theories
A Trusted Mechanised Specification of JavaScript: One Year On
Local Proofs for Global Safety Properties
Decision Procedures for Inductive Boolean Functions Based on Alternating Automata
Incremental Dead State Detection in Logarithmic Time
Verifying Continuous Time Markov Chains
Formalization and Automated Verification of RESTful Behavior
ObsSlice: A Timed Automata Slicer Based on Observers
Incremental Model Checking in the Modal Mu-Calculus
The Concurrency Workbench with Priorities
Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion
CEG4N: Counter-Example Guided Neural Network Quantization Refinement
The Hanoi Omega-Automata Format
Incremental, Inductive Coverability
Improved Probabilistic Models for 802.11 Protocol Verification
Formal Verification of Out-of-Order Execution Using Incremental Flushing
The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors
Reachability Analysis for AWS-Based Networks
chi-Chek: A Multi-valued Model-Checker
MEV-Freedom, in DeFi and Beyond (Invited Talk)
A Determinizable Class of Timed Automata
CVC4
An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation
Approximating Fixpoints of Approximated Functions