yusuke1997/dblp-id-title huggingface dataset:
Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings
Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings
An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks
Decomposition-Based Verification of Cyclic Workflows
What's Decidable about Sequences?
ForFET: A Formal Feature Evaluation Tool for Hybrid Systems
CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications
TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
Lattice-Valued Binary Decision Diagrams
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker
Introducing Dynamic Properties with Past Temporal Operators in the B Refinement
Parameter Synthesis for Markov Models: Faster Than Ever
Synthesis of Parametric Hybrid Automata from Time Series
Multi-core Nested Depth-First Search
New Optimizations and Heuristics for Determinization of Büchi Automata
Formal Specification for Deep Neural Networks
A Data Symmetry Reduction Technique for Temporal-epistemic Logic
SamaTulyata: An Efficient Path Based Equivalence Checking Tool
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints
Runtime Enforcement of Hyperproperties
The Buck Stops Here: Order, Chance, and Coordination in Distributed Control
LTL Model Checking of Time-Inhomogeneous Markov Chains
Verification of Partial-Information Probabilistic Systems Using Counterexample-Guided Refinements
Reachability as Derivability, Finite Countermodels and Verification
Compact Symbolic Execution
Don't Know for Multi-valued Systems
Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems
Improved Upper and Lower Bounds for Büchi Disambiguation
Model Checking Strategies from Synthesis over Finite Traces
An Algorithmic Framework for Synthesis of Concurrent Programs
Goanna: Syntactic Software Model Checking
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
State Space Reduction of Linear Processes Using Control Flow Reconstruction
Compositional Algorithms for LTL Synthesis
Control Flow Refinement and Symbolic Computation of Average Case Bound
Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
Exploiting Symmetries for Testing Equivalence in the Spi Calculus
Checking Scheduling-Induced Violations of Control Safety Properties
Test Case Generation of Actor Systems
Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part II
Verified Textbook Algorithms - A Biased Survey
Linear Temporal Logic - From Infinite to Finite Horizon
Efficient Verification of Program Fragments: Eager POR
Policies and Proofs for Code Auditing
AALpy: An Active Automata Learning Library
A Formal Semantics of the GraalVM Intermediate Representation
STL Model Checking of Continuous and Hybrid Systems
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond
A Dynamic Assertion-Based Verification Platform for Validation of UML Designs
A Theory for Control-Flow Graph Exploration
Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
Round-Bounded Control of Parameterized Systems
Symbolic Fault Tree Analysis for Reactive Systems
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Concurrent Program Verification with Invariant-Guided Underapproximation
Maximum Realizability for Linear Temporal Logic Specifications
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists ^*\forall ^* ∃ ∗ ∀ ∗ Fragment
Evaluation, Reduction, and Approximation of Dynamical Systems and Networks with ERODE
On the Membership Problem for Visibly Pushdown Languages
Optimal Strategy Synthesis in Request-Response Games
Symbolic Unfoldings for Networks of Timed Automata
AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization
Projected Model Counting: Beyond Independent Support
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols
The Complexity of Codiagnosability for Discrete Event and Timed Systems
Games for Formal Design and Verification of Reactive Systems
Compositional Verification for Component-Based Systems and Application
Fast Verified SCCs for Probabilistic Model Checking
Leveraging Program Structure for Test Case Generation
Termination and Invariance Analysis of Loops
Test Coverage Estimation Using Threshold Accepting
Validating the Translation of an Industrial Optimizing Compiler
Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units
Theorem Proving Languages for Verification
Automating Algebraic Specifications of Non-freely Generated Data Types
Hedge Automata Revisited: Transforming Texts to and from XML
Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points
On Detecting Regular Predicates in Distributed Systems
Verifying VLSI Circuits
Semi-automatic Distributed Synthesis
Model Checking Branching Properties on Petri Nets with Transits
CTL * Verification and Synthesis Using Existential Horn Clauses
Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing
Explainable Reactive Synthesis
Modelling and Analysis of Markov Reward Automata
Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems
Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts
Prioritizing Corners in OoD Detectors via Symbolic String Manipulation
Verifying Recurrent Neural Networks Using Invariant Inference
Games with Weighted Multiple Objectives
Better Predicates and Heuristics for Improved Commutativity Synthesis
DG: Analysis and Slicing of LLVM Bitcode
Statistically Sound Verification and Optimization for Complex Systems
Complete SAT-Based Model Checking for Context-Free Processes
Bounded Synthesis of Reactive Programs
Whodunit? Causal Analysis for Counterexamples
On-the-Fly Model Checking of Fair Non-repudiation Protocols
Game Semantic Analysis of Equivalence in IMJ
Syntactical Colored Petri Nets Reductions
MoTraS: A Tool for Modal Transition Systems and Their Extensions
Verification of a Generative Separation Kernel
On the Efficient Computation of the Minimal Coverability Set for Petri Nets
Computation Tree Regular Logic for Genetic Regulatory Networks
Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings
Truth Assignments as Conditional Autarkies
Proactive Leader Election in Asynchronous Shared Memory Systems
Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs
Maximum Resilience of Artificial Neural Networks
Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking
Optimal Repair for Omega-Regular Properties
Improved Single Pass Algorithms for Resolution Proof Reduction
First-Order LTL Model Checking Using MDGs
Typeness for omega-Regular Automata
Model Based Importance Analysis for Minimal Cut Sets
Efficient Approximate Verification of Promela Models Via Symmetry Markers
Robustness Testing of Intermediate Verifiers
Solving Parity Games in Practice
A Bounded Model Checker for SPARK Programs
On Temporal Logic and Signal Processing
Specification Sketching for Linear Temporal Logic
Proving Termination of Tree Manipulating Programs
CLP Based Static Property Checking
Impartial Anticipation in Runtime-Verification
Verification by Gambling on Program Slices
Probabilistic Hyperproperties with Nondeterminism
Automatic Verification of Hybrid Systems with Large Discrete State Space
Büchi Complementation Made Tighter
Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs
Bounded Model Checking for Probabilistic Programs
Cooperative Reactive Synthesis
Dynamic Shielding for Reinforcement Learning in Black-Box Environments
Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems
Localizing Errors in Counterexample with Iteratively Witness Searching
Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
Attacking the V: On the Resiliency of Adaptive-Horizon MPC
STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego
Manipulating LTL Formulas Using Spot 1.0
Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems
Automated Technology for Verification and Analysis - 23rd International Symposium, ATVA 2025, Bengaluru, India, October 27-31, 2025, Proceedings
Lifting CDCL to Template-Based Abstract Domains for Program Verification
Loop Quasi-Invariant Chunk Detection
Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions
Parallel and Incremental Verification of Hybrid Automata with Ray and Verse
Checking Satisfiability of Hyperproperties Using First-Order Logic
Generic Emptiness Check for Fun and Profit
On Minimal Odd Rankings for Büchi Complementation
Exploring the Scope for Partial Order Reduction
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities
Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications
Incremental Encoding and Solving of Cardinality Constraints
An Automatic Technique for Checking the Simulation of Timed Systems
Quantitative Analysis under Fairness Constraints
Controllers with Minimal Observation Power (Application to Timed Systems)
Decidability Results for Multi-objective Stochastic Games
Minimal Witnesses for Probabilistic Timed Automata
Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part I
SmacC: A Retargetable Symbolic Execution Engine
Conditional Testing - Off-the-Shelf Combination of Test-Case Generators
Formal Verification and Biology
Incremental False Path Elimination for Static Software Analysis
Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II
Non-monotonic Refinement of Control Abstraction for Concurrent Programs
Deriving Liveness Properties of Hybrid Systems from Reachable Sets and Lyapunov-Like Certificates
NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
A Novel Family of Finite Automata for Recognizing and Learning ømega-Regular Languages
Proving Cutoff Bounds for Safety Properties in First-Order Logic
Max and Sum Semantics for Alternating Weighted Automata
Hybrid System Verification Is Not a Sinecure: The Electronic Throttle Control Case Study
Accelerated Model Checking of Parametric Markov Chains
Probabilistic Automata on Infinite Words: Decidability and Undecidability Results
Approximating Deterministic Lattice Automata
Logahedra: A New Weakly Relational Domain
A Succinct Canonical Register Automaton Model
Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical Systems
An Impossibility Result in Automata-Theoretic Reinforcement Learning
A Sketching-Based Approach for Debugging Using Test Cases
Expected Termination Time in BPA Games
Using Counterexamples to Improve Robustness Verification in Neural Networks
Weighted Safety
Synthesis in pMDPs: A Tale of 1001 Parameters
Interpolants for Linear Arithmetic in SMT
Bisimilarity Distances for Approximate Differential Privacy
Quantitative Strategy Templates
Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
Model Checking Bounded Prioritized Time Petri Nets
Rabinizer: Small Deterministic Automata for LTL(F, G)
On (I/O)-Aware Good-For-Games Automata
ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems
A Decision Procedure for Separation Logic in SMT
Trace Abstraction Refinement for Timed Automata
An Experiment on Parallel Model Checking of a CTL Fragment
The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints
Some Perspectives of Infinite-State Verification
Composing Reachability Analyses of Hybrid Systems for Safety and Stability
Lazy Abstraction-Based Controller Synthesis
Precise Cost Analysis via Local Reasoning
Guiding Word Equation Solving Using Graph Neural Networks
Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems
LTL Can Be More Succinct
Bounded Verification with On-the-Fly Discrepancy Computation
Spanning the Spectrum from Safety to Liveness
A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
Equivalence-Based Abstraction Refinement for \mu HORS Model Checking
On the Satisfiability of Modular Arithmetic Formulae
Trace Diagnostics Using Temporal Implicants
DEQ: Equivalence Checker for Deterministic Register Automata
NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems
Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs
BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment
A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement
Component-Wise Instruction-Cache Behavior Prediction
Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances
RVX - A Tool for Concolic Testing of Embedded Binaries Targeting RISC-V Platforms
A Contextual Equivalence Checker for IMJ ∗
Multi-threaded Explicit State Space Exploration with State Reconstruction
COMBINE: A Tool on Combined Formal Methods for Bindingly Verification
A Game-Theoretic Approach to Simulation of Data-Parameterized Systems
Context-Aware Temporal Logic for Probabilistic Systems
Bounded Synthesis of Register Transducers
A Temporal Assertion Extension to Verilog
Development of RTOS for PLC Using Formal Methods
Probabilistic Programming: A True Verification Challenge
Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
An Efficient Algorithm for Learning Event-Recording Automata
PolyQEnt: A Polynomial Quantified Entailment Solver
A Fragment of Linear Temporal Logic for Universal Very Weak Automata
Using SMT for Solving Fragments of Parameterised Boolean Equation Systems
Fast Debugging of PRISM Models
CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers
Rabin Tree and Its Application to Group Key Distribution
Distribution of Reconfiguration Languages Maintaining Tree-Like Communication Topology
Quantitative Verification of Weighted Kripke Structures
Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
Alternating Good-for-MDPs Automata
Heuristics for Checking Liveness Properties with Partial Order Reductions
Comprehensive Verification Framework for Dependability of Self-optimizing Systems
Assembling Sessions
Parallel Assertions for Architectures with Weak Memory Models
Sigref- A Symbolic Bisimulation Tool Box
Synthesis: Words and Traces
Liquid Types for Array Invariant Synthesis
Formalization of Finite-State Discrete-Time Markov Chains in HOL
Partial-Order Reduction for GPU Model Checking
Model Checking Real Time Java Using Java PathFinder
Practical Efficient Modular Linear-Time Model-Checking
Composition of Accelerations to Verify Infinite Heterogeneous Systems
Componentwise Automata Learning for System Integration
Formal Verification for High-Assurance Behavioral Synthesis
Multi-valued Model Checking Games
Certifying DFA Bounds for Recognition and Separation
Local Search in Model Checking
Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations
First-Order Timed Runtime Verification Using BDDs
Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology
ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems
Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding
POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems
Stochastic Local Search for Falsification of Hybrid Systems
Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols
Verification of Markov Decision Processes Using Learning Algorithms
Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth
Evolution of Model Checking into the EDA Industry
Synthesizing Efficient Low-Precision Kernels
KLUZZER: Whitebox Fuzzing on Top of LLVM
Symbolic Verification and Test Generation for a Network of Communicating FSMs
Model Checking Failure-Prone Open Systems Using Probabilistic Automata
Toward Property-Driven Abstraction for Heap Manipulating Programs
Antarbhukti: Verifying Correctness of PLC Software During System Evolution
Making Software Verification Tools Really Work
Can We Trust Autonomous Systems? Boundaries and Risks
Verification of a Dynamic Management Protocol for Cloud Applications
A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings
Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives
Statistical Model Checking for Cyber-Physical Systems
ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks
Boosting Sequential Consistency Checking Using Saturation
Efficient On-the-Fly Emptiness Check for Timed Büchi Automata
What's Decidable about Weighted Automata?
Event-B Refinement for Continuous Behaviours Approximation
Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings
Learning the Language of Error
Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming
SAT-Based Verification of Safe Petri Nets
Fence Synthesis Under the C11 Memory Model
McAiT - A Timing Analyzer for Multicore Real-Time Software
Neural State Classification for Hybrid Systems
Reactive Synthesis of Smart Contract Control Flows
Memory Usage Verification Using Hip/Sleek
ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata
Modular Verification of Concurrent Programs via Sequential Model Checking
A Decremental Algorithm for Fair Büchi Games
Control Closure Certificates
Are Parametric Markov Chains Monotonic?
The Reach-Avoid Problem for Constant-Rate Multi-mode Systems
Faster Pushdown Reachability Analysis with Applications in Network Verification
Synthesis of Optimal Resilient Control Strategies
Formal Verification of Skiplists with Arbitrary Many Levels
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings
Scenario Approach for Parametric Markov Models
A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies
State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method
A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network
Providing Automated Verification in HOL Using MDGs
Learning Broadcast Protocols with LeoParDS
Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol
Mutation Coverage Estimation for Model Checking
Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications
On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies
Interpolation Properties and SAT-Based Model Checking
On the Succinctness of Nondeterminism
A New Approach to Bounded Model Checking for Branching Time Logics
Finding Polynomial Loop Invariants for Probabilistic Programs
Dynamic Observers for the Synthesis of Opaque Systems
Synchronous Products of Rewrite Systems
Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks
CELL: A Compositional Verification Framework
Temporal Causality in Reactive Systems
Branching-Time Property Preservation Between Real-Time Systems
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement
Discretizing Affine Hybrid Automata with Uncertainty
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
An Automata Theoretic Characterization of Weighted First-Order Logic
Solving Box-Pushing Games via Model Checking with Optimizations
Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets
TSO-to-TSO Linearizability Is Undecidable
Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings
A Fresh Look at Testing for Asynchronous Communication
Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata
An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
Efficient Loop Navigation for Symbolic Execution
Looking at Mean-Payoff and Total-Payoff through Windows
Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings
An EFSM-Based Intrusion Detection System for Ad Hoc Networks
Predicting Memory Demands of BDD Operations Using Maximum Graph Cuts
Distributed Synthesis for Alternating-Time Logics
Skolem Functions for DQBF
Verification of WCDMA Protocols and Implementation
SMELS: Satisfiability Modulo Equality with Lazy Superposition
Comparison of Different Semantics for Time Petri Nets
SAT Based Verification of Network Data Planes
Prompt Runtime Enforcement
Graph-Based Reductions for Parametric and Weighted MDPs
Widening with Thresholds for Programs with Complex Control Graphs
Effective Contraction of Timed STGs for Decomposition Based Timed Circuit Synthesis
Hierarchical Information Patterns and Distributed Strategy Synthesis
RTAMT: Online Robustness Monitors from STL
Functional Analysis of a Real-Time Protocol for Networked Control Systems
A Specification Logic for Exceptions and Beyond
Clause Sharing and Partitioning for Cloud-Based SMT Solving
LTL Model Checking with Neco
Integrity-Enhanced Verification Scheme for Software-Intensive Organizations
Simulation Algorithms for Symbolic Automata
Exploiting Hub States in Automatic Verification
PSense: Automatic Sensitivity Analysis for Probabilistic Programs
Proving SIFA Protection of Masked Redundant Circuits
Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
Hierarchical Counterexamples for Discrete-Time Markov Chains
Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms
Deciding Bisimilarity of Full BPA Processes Locally
Optimal Proofs for Linear Temporal Logic on Lasso Words
Probabilistic Causes in Markov Chains
Multi-head Monitoring of Metric Temporal Logic
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings
Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
Solution-Aware Vs Global ReLU Selection: Partial MILP Strikes Back for DNN Verification
Efficient Dynamic Shielding for Parametric Safety Specifications
Improved Multi-Core Nested Depth-First Search
Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach
Automatic Discovery of Fair Paths in Infinite-State Transition Systems