yusuke1997/dblp-id-title huggingface dataset:
CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis - (Competition Contribution)
Encoding Redundancy for Satisfaction-Driven Clause Learning
Commutativity of Reducers
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts
Hierarchical Set Decision Diagrams and Regular Models
Model Repair for Probabilistic Systems
Fairness for Dynamic Control
Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
Finding Recurrent Sets with Backward Analysis and Trace Partitioning
Modelling and Verification of Web Services Business Activity Protocol
Automatic Verification of Parameterized Data Structures
Satisfiability Checking Using Boolean Expression Diagrams
The Static Analyzer Frama-C in SV-COMP (Competition Contribution)
RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems
Automated Analysis of AODV Using UPPAAL
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution)
Reachability under Contextual Locking
Learning Realtime One-Counter Automata
Automated Termination Analysis for Programs with Second-Order Recursion
The Quantitative Verification Benchmark Set
Multi-cost Bounded Reachability in MDP
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver
Value Iteration with Guessing for Markov Chains and Markov Decision Processes
Dependent Types for Program Understanding
Scheduling System Verification
EVA: a Tool for the Compositional Verification of AUTOSAR Models
From Time Petri Nets to Timed Automata: An Untimed Approach
Approximating Predicate Images for Bit-Vector Logic
Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II
On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)
KReach: A Tool for Reachability in Petri Nets
PTIME Computation of Transitive Closures of Octagonal Relations
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Simulation-Based Graph Similarity
A Temporal Logic Based Theory of Test Coverage and Generation
SDSIrep: A Reputation System Based on SDSI
Modeling and Verification of SC++ Applications
CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker - (Competition Contribution)
HQSpre - An Effective Preprocessor for QBF and DQBF
Automated Module Composition
Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
Formal Verification of SDL Systems at the Siemens Mobile Phone Department
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
PhASAR: An Inter-procedural Static Analysis Framework for C/C++
AVR: Abstractly Verifying Reachability
ESBMC 1.22 - (Competition Contribution)
State of the Union: Type Inference Via Craig Interpolation
Practical Model-Checking Using Games
Implicit Rankings for Verifying Liveness Properties in First-Order Logic
Efficient Guiding Towards Cost-Optimality in UPPAAL
Model Checking Support for the ASM High-Level Language
Timed Condition/Event Systems: A Framework for Modular Discrete Models of Chemical Plants and Verification of Their Real-Time Discrete Control
Saturation Unbound
Compositional Invariant Generation for Timed Systems
Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities
Bounds2: A Tool for Compositional Multi-parametrised Verification
v2c - A Verilog to C Translator
Automatic Testing of Real-Time Graphics Systems
Inferring Synchronization under Limited Observability
Finitary Winning in omega-Regular Games
Falsification of LTL Safety Properties in Hybrid Systems
Verification and Improvement of the Sliding Window Protocol
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation
Reactive EFSMs - Reactive Promela/RSPIN
Mechanically Verified Self-Stabilizing Hierarchical Algorithms
EmergenTheta: Variations on Symbolic Transition Systems (Competition Contribution)
Efficient Syntax-Driven Lumping of Differential Equations
Probabilistic CTL * : The Deductive Way
Efficient Model Checking for LTL with Partial Order Snapshots
A New Knowledge Representation Strategy for Cryptographic Protocol Analysis
Synthesizing Piece-Wise Functions by Learning Classifiers
A Generic Theorem Prover of CSP Refinement
Multi-agent Safety Verification Using Symmetry Transformations
PEP - More than a Petri Net Tool
A Note on On-the-Fly Verification Algorithms
Interpolation-Based GR(1) Assumptions Refinement
History-Aware Data Structure Repair Using SAT
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution)
EMME: A Formal Tool for ECMAScript Memory Model Evaluation
Fully Local and Efficient Evaluation of Alternating Fixed Points (Extended Abstract)
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement
Model Checking Large-Scale and Parameterized Resource Allocation Systems
SVISS: Symbolic Verification of Symmetric Systems
LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution)
Proving Nontermination via Safety
The Concurrency Factory Software Development Environment
Property Directed Reachability for Generalized Petri Nets
Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings
VerifyThis - Verification Competition with a Human Factor
Multiparty Session Typing in Java, Deductively
Faster Algorithms for Finitary Games
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
Permutation Games for the Weakly Aconjunctive \mu μ -Calculus
AlPiNA: An Algebraic Petri Net Analyzer
Synthesis for Human-in-the-Loop Control Systems
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions - (Competition Contribution)
Parametric Runtime Verification of C Programs
Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification
Hardware/Software Co-Design Using Functional Languages
HaliVer: Deductive Verification and Scheduling Languages Join Forces
Combining Abstraction Refinement and SAT-Based Model Checking
A Study of Symmetry Breaking Predicates and Model Counting
Test Generation for Intelligent Networks Using Model Checking
Parameterized Verification of pi-Calculus Systems
Symbiotic 7: Integration of Predator and More - (Competition Contribution)
PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution)
Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution)
Monotonic Abstraction-Refinement for CTL
Coverage Metrics for Temporal Logic Model Checking
Detecting Unrealizable Specifications of Distributed Systems
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
Next Generation LearnLib
Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems
Improved Algorithms for the Automata-Based Approach to Model-Checking
Computation and Visualisation of Phase Portraits for Model Checking SPDIs
Competition on Software Verification and Witness Validation: SV-COMP 2023
Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)
Verified Reachability Analysis of Continuous Systems
JayHorn: A Java Model Checker - (Competition Contribution)
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors
Exploring Very Large State Spaces Using Genetic Algorithms
Training for Verification: Increasing Neuron Stability to Scale DNN Verification
Model Checking Discounted Temporal Properties
Improving the Verification of Timed Systems Using Influence Information
Automating Deductive Verification for Weak-Memory Programs
The xSAP Safety Analysis Platform
Finding Provably Optimal Markov Chains
BUBAAK: Dynamic Cooperative Verification - (Competition Contribution)
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
On Parallel Scalable Uniform SAT Witness Generation
CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation - (Competition Contribution)
Abstract Dependency Graphs and Their Application to Model Checking
The ForSpec Temporal Logic: A New Temporal Property-Specification Language
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
A New Approach for Active Automata Learning Based on Apartness
Model Checking SDL with Spin
Variations on Safety
Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)
DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
DiVer : SAT-Based Model Checking Platform for Verifying Large Scale Systems
Timed Automata Relaxation for Reachability
Analytic and Locally Approximate Solutions to Properties of Probabilistic Processes
Asynchronous Subtyping by Trace Relaxation
Towards String Support in JayHorn (Competition Contribution)
RWset: Attacking Path Explosion in Constraint-Based Test Generation
Compositional Model Extraction for Higher-Order Concurrent Programs
Applications of Craig Interpolants in Model Checking
Accelerating Syntax-Guided Invariant Synthesis
Hoare Logics for Time Bounds - A Study in Meta Theory
A SAT-Based Approach to Size Change Termination with Global Ranking Functions
Happy Ending: An Empty Hexagon in Every Set of 30 Points
Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning
SATABS: SAT-Based Predicate Abstraction for ANSI-C
Verification under TSO with an infinite Data Domain
Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond
Structural Counter Abstraction
Small Test Suites for Active Automata Learning
Verified reductions for optimization
AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution)
Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
Bounded Model Checking for Hyperproperties
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Semantic Fault Localization and Suspiciousness Ranking
Formal Design and Analysis of a Gear Controller
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs
On the Benefits of Using the Up-To Techniques for Bisimulation Verification
Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution)
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
Adaptive Model Checking
Predator Hunting Party (Competition Contribution)
A Region Graph Based Approach to Termination Proofs
Verifying Concurrent Programs by Memory Unwinding
Constraint-Based Monitoring of Hyperproperties
Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings
HLola: a Very Functional Tool for Extensible Stream Runtime Verification
Accelerating Interpolation-Based Model-Checking
A Local Shape Analysis Based on Separation Logic
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
cake_lpr: Verified Propagation Redundancy Checking in CakeML
Liveness with Incomprehensible Ranking
On the Construction of Automata from Linear Arithmetic Constraints
Model Checking on Trees with Path Equivalences
Hierarchical Adaptive State Space Caching Based on Level Sampling
Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS '96, Passau, Germany, March 27-29, 1996, Proceedings
CoVeriTeam: On-Demand Composition of Cooperative Verification Systems
Automata-Based Verification of Programs with Tree Updates
Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
Automatic Verification of Time Sensitive Cryptographic Protocols
CoPS - Checker of Persistent Security
JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution)
LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution)
A Prototype for Data Race Detection in CSeq 3 - (Competition Contribution)
Optimal Translation of LTL to Limit Deterministic Automata
On Reachability in Parameterized Phaser Programs
On-the-Fly Exact Computation of Bisimilarity Distances
Nacpa: Native Checking with Parallel-Portfolio Analyses - (Competition Contribution)
Incremental Scene Graph Distribution Method for Distributed Virtual Environments
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors
The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration
Simplifying Linearizability Proofs with Reduction and Abstraction
An Interpolating Theorem Prover
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors
MAVEN: Modular Aspect Verification
Transitive Closures of Regular Relations for Verifying Infinite-State Systems
Property Checking Array Programs Using Loop Shrinking
Verification of Large State/Event Systems Using Compositionality and Dependency Analysis
Second Competition on Software Verification - (Summary of SV-COMP 2013)
Synthesizing Ranking Functions from Bits and Pieces
Compositional Analysis for Verification of Parameterized Systems
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems
HOLL: Program Synthesis for Higher Order Logic Locking
Pattern-Based Abstraction for Verifying Secrecy in Protocols
CSeq: A Sequentialization Tool for C - (Competition Contribution)
Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
Type-Dependence Analysis and Program Transformation for Symbolic Execution
Synthesis of Circular Compositional Program Proofs via Abduction
Forester: Shape Analysis Using Tree Automata - (Competition Contribution)
autoCode4: Structural Controller Synthesis
Insight: An Open Binary Analysis Framework
Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution)
Lazy Automata Techniques for WS1S
Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability
Specifying and Verifying Higher-order Rust Iterators
Feature-Guided Black-Box Safety Testing of Deep Neural Networks
Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II
Conditional Probabilities over Probabilistic and Nondeterministic Systems
JPF: From 2003 to 2023
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams
Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems
Symbolic Model Checking without BDDs
Learning Real-Time One-Counter Automata Using Polynomially Many Queries
NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Quantitative Multi-objective Verification for Probabilistic Systems
Certifying Proofs in the First-Order Theory of Rewriting
VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution)
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)
Hardware Verification: Techniques, Methodology and Solutions
Verics: A Tool for Verifying Timed Automata and Estelle Specifications
CLPS-B - A Constraint Solver for B
Online Timed Pattern Matching Using Derivatives
Simple Representative Instantiations for Multicast Protocols
The ETI Online Service in Action
A Matrix-Based Approach to Parity Games
Inferring Interval-Valued Floating-Point Preconditions
Skink: Static Analysis of Programs in LLVM Intermediate Representation - (Competition Contribution)
CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution)
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Services and Visualization: Towards User-Friendly Design, ACoS'98, VISUAL'98, AIN'97, Selected Papers
RESY: Requirement Synthesis for Compositional Model Checking
Java Memory Model-Aware Model Checking
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
Auction-Based Scheduling
Geometric Nontermination Arguments
GRASShopper - Complete Heap Verification with Mixed Specifications
Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings
Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)
Strategy Construction in Infinite Ganes with Streett and Rabin Chain Winning Conditions
Modelling for Mere Mortals
Quasi-Equal Clock Reduction: More Networks, More Queries
Measuring Masking Fault-Tolerance
Statistical Measurement of Information Leakage
Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings
Time-Efficient Model Checking with Magnetic Disk
Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution)
PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games
LTSmin: High-Performance Language-Independent Model Checking
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
A Verified Implementation of the Bounded List Container
Revisiting Positive Equality
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Manipulation Algorithms for K*BMDs
Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance
Static Guard Analysis in Timed Automata Verification
CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution)
SDSAT : Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver
Hardware and Software Synthesis, Optimization, and Verification from Esterel Programs
Monitoring Modulo Theories
Synthesis from LTL Specifications with Mean-Payoff Objectives
Unfolding Concurrent Well-Structured Transition Systems
Automating the Analysis of Quantitative Automata with QuAK
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution)
Most General Winning Secure Equilibria Synthesis in Graph Games
Optimal Base Encodings for Pseudo-Boolean Constraints
Policy Analysis for Self-administrated Role-Based Access Control
Symbolic Coloured SCC Decomposition
Automated Software Verification of Hyperliveness
Timed Automata Verification and Synthesis via Finite Automata Learning
Java Ranger at SV-COMP 2020 (Competition Contribution)
Automate where Automation Fails: Proof Strategies for Frama-C/WP
Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution)
Propositional Reasoning
Ultimate Kojak - (Competition Contribution)
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation
Parameterized Verification under TSO with Data Types
Efficient Guided Symbolic Reachability Using Reachability Expressions
Provable Preimage Under-Approximation for Neural Networks
Towards Parallel Boolean Functional Synthesis
Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I
Using a Visual Formalism for Design Verification in Industrial Environments
SMT-Based Verification of Software Countermeasures against Side-Channel Attacks
Fast Directed Model Checking Via Russian Doll Abstraction
Highly Automated Formal Proofs over Memory Usage of Assembly Code
GWIT: A Witness Validator for Java based on GraalVM (Competition Contribution)
cTc - A Tool Supporting the Construction of cTLA-Specifications
Formal Verification of Pipelined Processors
Some Issues in the Software Engineering of Verification Tools
Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
SeaHorn: A Framework for Verifying C Programs (Competition Contribution)
Context-Bounded Analysis for POWER
Partial Model Checking with ROBDDs
Fast value iteration: A uniform approach to efficient algorithms for energy games
InterpChecker: Reducing State Space via Interpolations - (Competition Contribution)
Fold/Unfold Transformations for Fixpoint Logic
Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic
The Term Processor Generator Kimwitu
Multi-objective Model Checking of Markov Decision Processes
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Correct Probabilistic Model Checking with Floating-Point Arithmetic
Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
Shape Analysis by Graph Decomposition
A Polymorphic Intermediate Verification Language: Design and Logical Encoding
Efficient Diagnostic Generation for Boolean Equation Systems
Better Counterexamples for Dafny
Network Traffic Classification by Program Synthesis
An Improvement of McMillan's Unfolding Algorithm
Resource-Constrained Model Checking of Recursive Programs
Hoare Logic for Realistically Modelled Machine Code
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking
Parallelism for Free: Bitvector Analyses -> No State Explosion!
A Study of Intelligent Multimedia Services over PSTNs and the Internet
A Bit Too Precise? Bounded Verification of Quantized Digital Filters