yusuke1997/dblp-id-title huggingface dataset:
Formal Barriers to Longest-Chain Proof-of-Stake Protocols
Centralized Admissions for Engineering Colleges in India
Optimal Budget-Feasible Mechanisms for Additive Valuations
The Supply and Demand Effects of Review Platforms
Changes in the Interchange Agreements
Consumer-Optimal Market Segmentation
Nearly Optimal Pricing Algorithms for Production Constrained and Laminar Bayesian Selection
Iterated Deep Reinforcement Learning in Games: History-Aware Training for Improved Stability
How Do Machine Learning Algorithms Perform in Predicting Hospital Choices?: Evidence from Changing Environments
Spatio-Temporal Pricing for Ridesharing Platforms
Equilibrium Effects of Pay Transparency in a Simple Labor Market: Extended Abstract
Simple and Approximately Optimal Pricing for Proportional Complementarities
Budget-Feasible Mechanism Design for Non-Monotone Submodular Objectives: Offline and Online
Robust Commitments and Partial Reputation
Energy Equilibria in Proof-of-Work Mining
The Congressional Classification Challenge: Domain Specificity and Partisan Intensity
Individual Fairness in Hindsight
Naive Learning Through Probability Matching
Optimal Algorithm for Bayesian Incentive-Compatible Exploration
Simplicity Creates Inequity: Implications for Fairness, Stereotypes, and Interpretability
On the Price of Anarchy for flows over time
Dynamic Learning and Market Making in Spread Betting Markets with Informed Bettors
Mind the Mining
Estimating Approximate Incentive Compatibility
Buy-Many Mechanisms are Not Much Better than Item Pricing
Optimal Auctions vs. Anonymous Pricing: Beyond Linear Utility
Trading Networks with General Preferences
Displaying Things in Common to Encourage Friendship Formation: A Large Randomized Field Experiment
Temporal Reasoning for Automated Workflow in Health Care Enterprises
Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution
Identifying Bid Leakage in Procurement Auctions: Machine Learning Approach
Adversarial Contract Design for Private Data Commercialization
LP-based Approximation for Personalized Reserve Prices
Obvious Manipulations
Simple versus Optimal Contracts
Group Fairness in Committee Selection
A Marketplace for Data: An Algorithmic Solution
Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management
Equitable Voting Rules
Computing Large Market Equilibria using Abstractions
Simple Mechanisms for Profit Maximization in Multi-item Auctions
Machine-Negotiated, Ontology-Based EDI (Electronic Data Interchange)
The Information Marketplace: Achieving Success in Commercial Applications
Prior-free Data Acquisition for Accurate Statistical Estimation
Incorporating Compatible Pairs in Kidney Exchange: A Dynamic Weighted Matching Model
Obvious Dominance and Random Priority
Principal-Agent VCG Contracts
Managing Market Mechanism Transitions: A Randomized Trial of Decentralized Pricing Versus Platform Control
Carpooling and the Economics of Self-Driving Cars
The Standardisation of Flexible EDI Messages
School Choice in Chile
Electronic Commerce: An Overview
How to Sell a Dataset?: Pricing Policies for Data Monetization
Optimal Pricing in Markets with Non-Convex Costs
Smoothed Analysis of Multi-Item Auctions with Correlated Values
The Perils of Exploration under Competition: A Computational Modeling Approach
Price of Privacy in the Keynesian Beauty Contest
When Simulation Meets Antichains
Computing Adequately Permissive Assumptions for Synthesis
Semantic Importance Sampling for Statistical Model Checking
Advances in Automatic Software Verification: SV-COMP 2020
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols
Model Checking Database Applications
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - (Competition Contribution)
A Constraint-Oriented Service Creation Environment
Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS '95, Aarhus, Denmark, May 19-20, 1995, Proceedings
Abstraction Refinement of Linear Programs with Arrays
Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications
A Theoretical Analysis of Random Regression Test Prioritization
Stateless Model Checking for TSO and PSO
Verifying Reference Counting Implementations
Counter-Example Guided Fence Insertion under TSO
Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata
Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II
Bounded Validity Checking of Interval Duration Logic
Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
A Comparison of Two Verification Methods for Speculative Instruction Execution
CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution)
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification
Symbolic Test Selection Based on Approximate Analysis
Is There a Best Symbolic Cycle-Detection Algorithm?
Truly On-the-Fly LTL Model Checking
Büchi Store: An Open Repository of Büchi Automata
A Game for Linear-time-Branching-time Spectroscopy
Abstracting WS1S Systems to Verify Parameterized Networks
Relational Differential Dynamic Logic
Permutable Agents in Process Algebras
A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes
Efficient Property Preservation Checking of Model Refinements
Improving Neural Network Verification through Spurious Region Guided Refinement
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution)
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
JANI: Quantitative Model and Tool Interaction
An Alternative to SAT-Based Approaches for Bit-Vectors
MetAcsl: Specification and Verification of High-Level Properties
RTLola on Board: Testing Real Driving Emissions on your Phone
SMACK+Corral: A Modular Verifier - (Competition Contribution)
Demand-Driven Compositional Symbolic Execution
CPAchecker with Adjustable Predicate Analysis - (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings
Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution)
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution)
Incremental Verification by Abstraction
GameTime: A Toolkit for Timing Analysis of Software
GAVS+: An Open Platform for the Research of Algorithmic Game Solving
Automated Fast-Track Reconfiguration of Group Communication Systems
Reachability Analysis for Termination and Confluence of Rewriting
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
Under-Approximating Expected Total Rewards in POMDPs
Demonstrating Learning of Register Automata
Transition Power Abstractions for Deep Counterexample Detection
LydiaSyft: A Compositional Symbolic Synthesis Framework for LTL f Specifications
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol
Experience with Literate Programming in the Modelling and Validation of Systems
HiFrog: SMT-based Function Summarization for Software Verification
Oink: An Implementation and Evaluation of Modern Parity Game Solvers
Optimal Tableau Algorithms for Coalgebraic Logics
Distributed Analysis with mu CRL: A Compendium of Case Studies
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets
Automated Verification of Parallel Nested DFS
Runtime Monitoring with Union-Find Structures
ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions
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 III
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Discounting in LTL
Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs
UPPAAL in 1995
GPU Accelerated Strong and Branching Bisimilarity Checking
A Light-Weight Framework for Hardware Verification
Translation Validation
TIMES - A Tool for Modelling and Implementation of Embedded Systems
Graphs in METAFrame: The Unifying Power of Polymorphism
Generating Representation Invariants of Structurally Complex Data
Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution)
DYANA: An Environment for Embedded System Design and Analysis
SL-COMP: Competition of Solvers for Separation Logic
Intertwined Forward-Backward Reachability Analysis Using Interpolants
Weighted Pushdown Systems with Indexed Weight Domains
A Period Assignment Algorithm for Real-Time System Design
Theorem Prover Support for the Refinement of Stream Processing Functions
MSCan - A Tool for Analyzing MSC Specifications
ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution)
Compositionality Entails Sequentializability
Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests
Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution)
Make Flows Small Again: Revisiting the Flow Framework
On-the-Fly Reachability and Cycle Detection for Recursive State Machines
Symbolic Representation of Upward-Closed Sets
JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution)
BINSEC: Binary Code Analysis with Low-Level Regions
Synthesis of Compact Strategies for Coordination Programs
Symbiotic 4: Beyond Reachability - (Competition Contribution)
EMTST: Engineering the Meta-theory of Session Types
Automatic Deductive Verification with Invisible Invariants
Compositional Termination Proofs for Multi-threaded Programs
Presentation of the 9th Edition of the Model Checking Contest
EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)
Symbolic Regex Matcher
Combining Model Checking and Deduction for I/O-Automata
FlyFast: A Mean Field Model Checker
On Memory-Block Traversal Problems in Model-Checking Timed-Systems
Complementing Semi-deterministic Büchi Automata
Large State Space Visualization
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
Generalized Symbolic Execution for Model Checking and Testing
Searching for Shapes in Cryptographic Protocols
Dissipative quadratizations of polynomial ODE systems
Assume-Guarantee Verification for Probabilistic Systems
CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis - (Competition Contribution)
Cascade - (Competition Contribution)
Correct Approximation of Stationary Distributions
Formally verified asymptotic consensus in robust networks
Mona: Monadic Second-Order Logic in Practice
COASTAL: Combining Concolic and Fuzzing for Java (Competition Contribution)
Automatic Repair for Network Programs
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
eVolCheck: Incremental Upgrade Checker for C
Automatic Test Generation with AGATHA
T2: Temporal Property Verification
Reduction-Based Formal Analysis of BGP Instances
A Logical Treatment of Finite Automata
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs
Automatic Analysis of the Security of XOR-Based Key Management Schemes
VeriFuzz: Program Aware Fuzzing - (Competition Contribution)
A Platform for High Performance Statistical Model Checking - PLASMA
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 III
Clausal Proofs for Pseudo-Boolean Reasoning
MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
SV-COMP'25 Reproduction Report (Competition Contribution)
What a Difference a Variable Makes
How Vacuous Is Vacuous?
Speculative SAT Modulo SAT
Visualisation of Executable Formal Specifications for User Validation
On-the-Fly Techniques for Game-Based Software Model Checking
ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets
A Calculus for Modular Loop Acceleration
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
Modular Strategies for Recursive Game Graphs
Adaptor Synthesis for Real-Time Components
Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
νZ - An Optimizing SMT Solver
Non-cumulative Resource Analysis
Fair Termination for Parameterized Probabilistic Concurrent Systems
FDR3 - A Modern Refinement Checker for CSP
Active Learning for SAT Solver Benchmarking
A Tool to Support Formal Reasoning about Computer Languages
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Temporal Debugging for Concurrent Systems
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
JDart: A Dynamic Symbolic Analysis Framework
LLBMC: Improved Bounded Model Checking of C Programs Using LLVM - (Competition Contribution)
Approximating the Pareto Front of Multi-criteria Optimization Problems
Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution)
Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
Synthesizing Monitors for Safety Properties
Simulation Revisited
Incremental Analysis of Evolving Alloy Models
Rational Synthesis
The PROSPER Toolkit
WAPS: Weighted and Projected Sampling
Software Verification with PDR: An Implementation of the State of the Art
Model Checking Agent Knowledge in Dynamic Access Control Policies
Assume, Guarantee or Repair
The Real-Time Maude Tool
Resets vs. Aborts in Linear Temporal Logic
Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions
SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)
Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
Model-Checking for a Subclass of Event Structures
Deciding an Interval Logic with Accumulated Durations
TATOO: Testing and Analysis Tool for Object- Oriented Software
Minimal Assignments for Bounded Model Checking
Satisfiability Modulo the Theory of Costs: Foundations and Applications
Decidable Verification under Localized Release-Acquire Concurrency
Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus
A Verified Model Checker for the Modal µ-calculus in Coq
VyPR2: A Framework for Runtime Verification of Python Web Services
CPAchecker 4.0 as Witness Validator - (Competition Contribution)
International Competition on Runtime Verification (CRV)
Bridging the Gap Between Model-Based Development and Model Checking
On-The-Fly Algorithm for Reachability in Parametric Timed Games
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation
Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking
Learning One-Clock Timed Automata
SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution)
ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)
Decidability of Invariant Validation for Paramaterized Systems
Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
A Scalable Incomplete Test for the Boundedness of UML RT Models
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication
Transition Invariants and Transition Predicate Abstraction for Program Termination
Explainable Online Monitoring of Metric Temporal Logic
Proof-Like Counter-Examples
Optimal Stateless Model Checking for Causal Consistency
Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy
Combining Partial Order and Symmetry Reductions
Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
Fast Symbolic Computation of Bottom SCCs
EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution)
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
RacerF: Data Race Detection with Frama-C (Competition Contribution)
Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM
Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches
Dynamic Symmetry Reduction
Strategy Representation by Decision Trees in Reactive Synthesis
Computing Conditional Probabilities in Markovian Models Efficiently
Long-Run Rewards for Markov Automata
JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution
Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time
Improvements in Software Verification and Witness Validation: SV-COMP 2025
Formal Verification of Statecharts with Instantaneous Chain Reaction
Decomposing Farkas Interpolants
Generic System Support for Deductive Program Development
Boolean and Cartesian Abstraction for Model Checking C Programs
Test Input Generation for Programs with Pointers
Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic
Learning Minimal Separating DFA's for Compositional Verification
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems
Reachability for Nonsmooth Systems with Lexicographic Jacobians
A Temporal Logic of Nested Calls and Returns
MOSEL: A FLexible Toolset for Monadic Second-Order Logic
Fully Automatic Verifcation and Error Detection for Parameterized Iterative Sequential Circuits
Feature Necessity & Relevancy in ML Classifier Explanations
Robust Almost-Sure Reachability in Multi-Environment MDPs
Validation, Synthesis and Optimization for Cyber-Physical Systems
PROTON 2.1: Synthesizing Ranking Functions via fine-tuned locally Hosted LLM (Competition Contribution)
i _\mathrm Rank : A Variable Order Metric for DEDS Subject to Linear Invariants
Efficient Automatic STE Refinement Using Responsibility
Realtion-Algebraic Analysis of Petri Nets with RELVIEW
SyReNN: A Tool for Analyzing Deep Neural Networks
APTE: An Algorithm for Proving Trace Equivalence
A Tool for Proving Invariance Properties of Concurrent Systems Automatically
Detecting Races in Ensembles of Message Sequence Charts
Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution)
Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets
Biased Model Checking Using Flows
'Calls Considered Harmful' and Other Observations: A Tutorial on Telephony
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 II
Debugging of Behavioural Models with CLEAR
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution)
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
Basic Problems in Multi-View Modeling
Ramsey vs. Lexicographic Termination Proving
LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios
From Tests to Proofs
Endicheck: Dynamic Analysis for Detecting Endianness Bugs
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I
C2E2: A Verification Tool for Stateflow Models
Consistent Integration of Formal Methods
Alpinist: An Annotation-Aware GPU Program Optimizer
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
ML for ML: Learning Cost Semantics by Experiment
A Statistical Model Checker for Nondeterminism and Rare Events
Distributed Compression of Live Video - An Application for Active Networks
A Flexible Proof Format for SAT Solver-Elaborator Communication
Transforming Quantified Boolean Formulas Using Biclique Covers
A Tableau System for Linear-TIME Temporal Logic
Parallel SAT Simplification on GPU Architectures
Token Elimination in Model Checking of Petri Nets
Temporal Logic for Scenario-Based Specifications
Computing the Expected Execution Time of Probabilistic Workflow Nets
MaskD: A Tool for Measuring Masking Fault-Tolerance
Knor: reactive synthesis using Oink
Reasoning Algebraically About P-Solvable Loops
Tracking Heaps That Hop with Heap-Hop
Shepherding Hordes of Markov Chains
Underapproximation of Procedure Summaries for Integer Programs
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs ,
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 II
How Many Bits Does it Take to Quantize Your Neural Network?
Model Checking Security Protocols Using a Logic of Belief
Requirements and a Proposal for the Prevention of a Class of Service Interactions in Intelligent Networks
A Practical and Complete Approach to Predicate Refinement
Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution)
Checking Strong Specifications Using an Extensible Software Model Checking Framework
Frame Inference for Inductive Entailment Proofs in Separation Logic
Extending Promela and Spin for Real Time
Games and Modal Mu-Calculus
Modular Mix-and-Match Complementation of Büchi Automata
Hardware Testing Using a Communication Protocol Conformance Testing Tool
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I
AutoHyper: Explicit-State Model Checking for HyperLTL
On the Universal and Existential Fragments of the µ-Calculus
SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems
Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools
Learning Symbolic Automata
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL
Acceleration in Multi-PushDown Systems
Loop Summarization and Termination Analysis
Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)
SACO: Static Analyzer for Concurrent Objects
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution)
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Branching vs. Linear Time: Final Showdown
dReach: δ-Reachability Analysis for Hybrid Systems
Status Report on Software Verification - (Competition Summary SV-COMP 2014)
Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution)
SATMC: A SAT-Based Model Checker for Security-Critical Systems
cvc5: A Versatile and Industrial-Strength SMT Solver