yusuke1997/dblp-id-title huggingface dataset:
Adapting an AI Planning Heuristic for Directed Model Checking
What Went Wrong: Explaining Counterexamples
Verifying Pipeline Implementations in OpenMP
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
Nevertrace Claims for Model Checking
Building Extensible Specifications and Implementations of Promela with AbleP
Enhanced Probabilistic Verification with 3Spin and 3Murphi
Automated Evaluation of Secure Route Discovery in MANET Protocols
Towards a GPGPU-parallel SPIN model checker
Execution Generated Test Cases: How to Make Systems Code Crash Itself
Learning the State Machine Behind a Modal Text Editor: The (Neo)Vim Case Study
Automatic Generation of Model Checking Scripts Based on Environment Modeling
The Birth of Model Checking
Model Checking Publish-Subscribe Systems
Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM
Taming the AI Monster: Monitoring of Individual Fairness for Effective Human Oversight
Tutorial on FDR and Its Applications
Formal Verification of a Flash Memory Device Driver - An Experience Report
Random Access on Narrow Decision Diagrams in External Memory
Verifying Commit-Atomicity Using Model-Checking
Unit testing for SPIN: runspin and parsepan
Sound Transaction-Based Reduction Without Cycle Detection
Correctness by Construction: Towards Verification in Hierarchical System Development
Backward coverability with pruning for lossy channel systems
Fair Testing and Stubborn Sets
Typical Structural Properties of State Spaces
Transformations for Model Checking Distributed Java Programs
Don't Know in Probabilistic Systems
High-Coverage Symbolic Patch Testing
Efficient Modeling of Concurrent Systems in BMC
String Abstraction for Model Checking of C Programs
Conformance Testing of Schedulers for DSL-based Model Checking
Randomized Backtracking in State Space Traversal
Potency-Based Heuristic Search with Randomness for Explicit Model Checking
Model Checking Systems of Replicated Processes with Spin
Elimination of Detached Regions in Dependency Graph Verification
Abstraction in Software Model Checking: Principles and Practice (Tutorial Overview and Bibliography)
Extending the Translation from SDL to Promela
Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study
Experience with Model Checking Linearizability
Residual Checking of Safety Properties
Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes
Stuttering Congruence for chi
Directed Model Checking for PROMELA with Relaxation-Based Distance Functions
The Temporal Rover and the ATG Rover
Symbolic Object Code Analysis
Model Checking Abstract Components within Concrete Software Environments
Automatic handling of native methods in Java PathFinder
A Tool Integrating Model Checking into a C Verification Toolset
Solving String Theories Involving Regular Membership Predicates Using SAT
A hot method for synthesising cool controllers
Software Model Checking for Mobile Security - Collusion Detection in \mathbb K K
Parallel Recursive State Compression for Free
Cartesian Partial-Order Reduction
Symbolic Context-Bounded Analysis of Multithreaded Java Programs
A Study of Learning Data Structure Invariants Using Off-the-shelf Tools
Abstraction-Based Guided Search for Hybrid Systems
Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings
Fast, All-Purpose State Storage
A Nearly Memory-Optimal Data Structure for Sets and Mappings
Local Model Checking of Weighted CTL with Upper-Bound Constraints
Improved On-the-Fly Equivalence Checking Using Boolean Equation Systems
Learning-Based Assume-Guarantee Verification (Tool Paper)
Expression Reduction from Programs in a Symbolic Binary Executor
An improvement of the piggyback algorithm for parallel model checking
From Dynamic State Machines to Promela
Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking
Comparing Symbolic and Explicit Model Checking of a Software System
SAT-Based Summarization for Boolean Programs
Model Verification Through Dependency Graphs
Probabilistic Model Checking of Randomized Java Code
Optimal Scheduling Using Branch and Bound with SPIN 4.0
Compositional Semantics and Analysis of Hierarchical Block Diagrams
ACSAR: Software Model Checking with Transfinite Refinement
Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
Model Checking Software - 31st International Symposium, SPIN 2025, Hamilton, ON, Canada, May 7-8, 2025, Proceedings
Software Model Checking Improving Security of a Billion Computers
Mining Models
Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11-13, 2002, Proceedings
Model Checking Operator Procedures
SPIN Tutorial: How to Become a SPIN Doctor
Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems
Checking Consistency of SDL+MSC Specifications
Promela Planning
DiPro - A Tool for Probabilistic Counterexample Generation
From Church and Prior to PSL
A Methodology for Model-Checking Ad-hoc Networks
Directed Model Checking with Distance-Preserving Abstractions
A Retrospective on Mur phi
Model Checking Software - 29th International Symposium, SPIN 2023, Paris, France, April 26-27, 2023, Proceedings
Repairing Structurally Complex Data
Automated formal reasoning about amazon web services (keynote)
Parallel State Space Construction for Model-Checking
alpha SPIN: Extending SPIN with Abstraction
Formal Methods Adoption: What's Working, What's Not!
Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU)
Symbolic String Verification: An Automata-Based Approach
Runtime Verification of Expected Energy Consumption in Smartphones
Toward parameterized verification of synchronous distributed applications
Generating Compact MTBDD-Representations from ProbmelaSpecifications
Property-Dependent Reductions for the Modal Mu-Calculus
Runtime enforcement of reactive systems using synchronous enforcers
Demonstration of an Automated Integrated Test Environment for Web-Based Applications
A Model-Checked I 2 C Specification
SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings
Parallel and Distributed Model Checking in Eddy
Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Dynamic Bounds and Transition Merging for Local First Search
CARET model checking for malware detection
Autonomous Agent Behaviour Modelled in PRISM - A Case Study
Layered Duplicate Detection in External-Memory Model Checking
Distributed LTL Model-Checking in SPIN
On-the-Fly Emptiness Checks for Generalized Büchi Automata
EMMA: Explicit Model Checking Manager (Tool Presentation)
Java PathFinder, A Translator from Java to Promela
Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals
smid: A Black-Box Program Driver
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software
An Analytic Evaluation of SystemC Encodings in Promela
Assume-Guarantee Model Checking of Software: A Comparative Case Study
Benchmarking and Resource Measurement
Sound Concurrent Traces for Online Monitoring
Validation of UML Models via a Mapping to Communicating Extended Timed Automata
Symmetric Spin
Analyzing Mode Confusion via Model Checking
STAD: Stack Trace Based Automatic Software Misconfiguration Diagnosis via Value Dependency Graph
Distributed binary decision diagrams for symbolic reachability
Formal Modeling and Analysis of an Avionics Triplex Sensor Voter
Industrial Model Checking Based on Satisfiability Solvers
Symbolic Model Checking for Asynchronous Boolean Programs
0-1 Laws for LTL and CTL over Random Transition Systems
The Influence of Software Module Systems on Modular Verification
Model Checking if Your Life Depends on It a View from Intel's Trenches
SMT-Based Software Model Checking
Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers
Local Abstraction-Refinement for the mu-Calculus
Abstract Matching for Software Model Checking
Instrumenting C Programs with Nested Word Monitors
Model Extraction for ARINC 653 Based Avionics Software
Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation
The Maude LTL Model Checker and Its Implementation
Learning Guided Enumerative Synthesis for Superoptimization
Mining Sequential Patterns to Explain Concurrent Counterexamples
Error-Completion in Interface Theories
Test-Case Generation with Automata-Based Software Model Checking
The Case for Context-Bounded Verification of Concurrent Programs
A Branching Time Variant of CaRet
Applications of Model Checking at Honeywell Laboratories
Optimizing parallel Korat using invalid ranges
Symbolic Causality Checking Using Bounded Model Checking
From Model Checking to a Temporal Proof
On-the-Fly Cone-of-Influence Reduction for Model Checking Concurrent Software
FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation
TransVer: A Modular Program-Transformation Framework for Reduction to Reachability
Symbolic Model Checking of Stochastic Systems: Theory and Implementation
Automated Reasoning in Quantum Circuit Compilation
Verifying Pattern-Generated LTL Formulas: A Case Study
A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols
Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
Extracting Safe Thread Schedules from Incomplete Model Checking Results
Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench
A Typical Testing Problem: Validating WML Cellphones
Counterexample-Based Refinement for a Boundedness Test for CFSM Languages
Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings
A Counterexample-Guided Refinement Tool for Open Procedural Programs
Certification for configurable program analysis
Distributed-Memory Model Checking with SPIN
Efficient Probabilistic Model Checking on General Purpose Graphics Processors
Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
On Parallel Software Verification Using Boolean Equation Systems
Large-Scale Directed Model Checking LTL
Applying Model Checking Approach with Floating Point Arithmetic for Verification of Air Collision Avoidance Maneuver Hybrid Model
A SAT Characterization of Boolean-Program Correctness
Petri Net Reductions for Counting Markings
Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials
Directed Explicit Model Checking with HSF-SPIN
Implementing LTL Model Checking with Net Unfoldings
SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Tutorial: Parallel Model Checking
Synthesis of Rigorous Floating-Point Predicates
Formal verification of data-intensive applications through model checking modulo theories
Model Checking Software - 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings
Model-Driven Software Verification
Resource-Aware Verification Using Randomized Exploration of Large State Spaces
ExpoSE: practical symbolic execution of standalone JavaScript
The SpinJa Model Checker
Model Checking Software, 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings
Parallel SAT-Based Parameterised Three-Valued Model Checking
A Comparative Study of Decision Diagrams for Real-Time Model Checking
Model Checking for Managers
25 Years of Model Checking - History, Achievements, Perspectives
Incremental bounded software model checking
Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution
Model Checking Programs with Java PathFinder
SAT-Based Counterexample Guided Abstraction Refinement
Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid
The BLAST Software Verification System
Refinement Selection
SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions
A Compositional Minimization Approach for Large Asynchronous Design Verification
Model Checking Software - 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings
McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking
Accelerating Black Box Testing with Light-Weight Learning
Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis
2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014
Xspin/Project - Integrated Validation Management for Xspin
Who Really Cares If the Program Crashes?
Larger Automata and Less Work for LTL Model Checking
Regression Verification Using Impact Summaries
River Basin Management with Spin
Linking ST e P with SPIN
Accelerating the Computation of Dead and Concurrent Places Using Reductions
Verifying Compiler Based Refinement of BluespecTM
New Challenges in Model Checking
Embedding a Dialect of SDL in PROMELA
Black-Box Conformance Testing for Real-Time Systems
Translation from Adapted UML to Promela for CORBA-Based Applications
Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings
Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings
Subsumer-First: Steering Symbolic Reachability Analysis
A Language Framework for Expressing Checkable Properties of Dynamic Software
Bounded-Memory Runtime Enforcement
Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models
Modelling Without a Modelling Language
SpinRCP: the eclipse rich client platform integrated development environment for the spin model checker
Advanced SPIN Tutorial
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs
Fault Localization on Verification Witnesses
Model learning and model checking of SSH implementations
On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
Program Verification with Separation Logic
Formal Analysis of Processor Timing Models
Counterexample Explanation by Anomaly Detection
Quantitative Model Checking for a Controller Design
Probabilistic Verification of Coordinated Multi-robot Missions
Bytecode Model Checking: An Experimental Analysis
Etch: An Enhanced Type Checking Tool for Promela
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving
Cobra: fast structural code checking (keynote)
Effective Bug Hunting with Spin and Modex
From SysML to Model Checkers via Model Transformation
Go2Pins: A Framework for the LTL Verification of Go Programs
The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited
Practical Stutter-Invariance Checks for ω-Regular Languages
Parallelizing the Spin Model Checker
Incremental Hashing for Spin
Probabilistic Reachability for Parametric Markov Models
Bebop: A Symbolic Model Checker for Boolean Programs
Reuse of Verification Results - Conditional Model Checking, Precision Reuse, and Verification Witnesses
On-the-Fly Dynamic Dead Variable Analysis
Proving Properties of Concurrent Programs - (Extended Abstract)
GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data
VIP: A Visual Interface for Promela
Software Verification with BLAST
Runtime Checking of Multithreaded Applications with Visual Threads
A Model Checking Project at Philips Research
SPINning Parallel Systems Software
mctau: Bridging the Gap between Modest and UPPAAL
p2b: A Translation Utility for Linking Promela and Symbolic Model Checking (Tool Paper)
Automated Consistency Analysis for Legal Contracts
Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin
PickLock: A Deadlock Prediction Approach under Nested Locking
Fast, Dynamically-Sized Concurrent Hash Table
Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings
Automated Analysis of Asynchronously Communicating Systems
Behavioural Models for Hierarchical Components
System Specification and Verification Using High Level Concepts - A Tool Demonstration
Improving Spin's Partial-Order Reduction for Breadth-First Search
(Asynchronous) Temporal Logics for Hyperproperties on Finite Traces
IF Validation Environment Tutorial
Low-Fat Recipes for SPIN
Is there a best büchi automaton for explicit model checking?
Compositional Approach to Suspension and Other Improvements to LTL Translation
A Framework for Automatic Construction of Abstract Promela Models
Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
Heuristic Model Checking for Java Programs
Synthesizing Controllers for Automation Tasks with Performance Guarantees
Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness
Model Checking: From Tools to Theory
Solving Constrained Horn Clauses as C Programs with CHC2C
Efficient Model Checking of Safety Properties
Using SPIN to Verify Security Properties of Cryptographic Protocols
A SystemC/TLM Semantics in Promelaand Its Possible Applications
Software Verification Witnesses 2.0
PatEC: Pattern-Based Equivalence Checking
Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-Attacks
The Quest for Correctness-Beyond a Posteriori Verification
ParaGnosis: A Tool for Parallel Knowledge Compilation
A Requirements Patterns-Driven Approach to Specify Systems and Check Properties
Verifying Multi-threaded C Programs with SPIN
S2N: Model Transformation from SPIN to NuSMV - (Tool Paper)
Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006, Proceedings
Analysis of Distributed Spin Applied to Industrial-Scale Models
Events in Property Patterns
Efficient Runtime Verification of First-Order Temporal Properties
VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs
Local state space construction for compositional verification of concurrent systems
Behavioural Analysis of the Enterprise JavaBeans TM Component Architecture
Increasing usability of spin-based C code verification using a harness definition language: leveraging model-driven code checking to practitioners
Depth Bounded Explicit-State Model Checking
Distributed Explicit Fair Cycle Detection (Set Based Approach)
Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study
Model Checking Unbounded Concurrent Lists
Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings
Explicit state model checking with generalized Büchi and Rabin automata
The Agreement Problem Protocol Verification Environment
On the Synergy of Probabilistic Causality Computation and Causality Checking
Applying Model Checking in Java Verification
MESS: Memory Performance Debugging on Embedded Multi-core Systems
A Novel Decentralized LTL Monitoring Framework Using Formula Progression Table
Abstract Interpretation: Theory and Practice
Verification Experiments on the MASCARA Protocol
Bottleneck Analysis of a Gigabit Network Interface Card: Formal Verification Approach
Accelerating CAR-Based Model-Checking with Multiple Unsatisfiable Cores
An Embeddable Virtual Machine for State Space Generation
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017
Partial Order Reduction in Directed Model Checking
Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing
Dynamic Delayed Duplicate Detection for External Memory Model Checking
State Focusing: Lazy Abstraction for the Mu-Calculus
Locating Concurrency Errors in Windows .NET Applications by Fuzzing over Thread Schedules
Some Solutions to the Ignoring Problem
Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software
Using Fairness to Make Abstractions Work
Approximating happens-before order: interplay between static analysis and state space traversal
Towards Automatic Synthesis of Software Verification Tools
Model Counting for Complex Data Structures
Quantifying information leaks using reliability analysis
Using Garbage Collection in Model Checking
Modeling and Verifying a Price Model for Congestion Control in Computer Networks Using Promela/Spin
Verige: verification with invariant generation engine
COMPLeTe - A COMmunication Protocol vaLidation Toolchain
Identifying Modeling Errors in Signatures by Model Checking
Model Checking Based on Simultaneous Reachability Analysis
Guided test case generation for mobile apps in the TRIANGLE project: work in progress
Thread-Modular Model Checking
Model Checking Knowledge and Time
Scalable Multi-core LTL Model-Checking
Unification & Sharing in Timed Automata Verification
LTL Satisfiability Checking
Context-Updates Analysis and Refinement in Chisel
DSVerifier: A Bounded Model Checking Tool for Digital Systems
A View from the Engine Room: Computational Support for Symbolic Model Checking
SunDew: systematic automated security testing (keynote)
Verification of MPI-Based Software for Scientific Computation
An Efficient and Versatile Approach to Shortest Path Problems in Interprocedural Programs
Combining Static and Dynamic Reasoning for the Discovery of Program Properties
Tolerange: Quantifying Fault Masking in Stochastic Systems
Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance
Family-Based Model Checking Without a Family-Based Model Checker
Model Checking Industrial Robot Systems
Efficient Stateful Dynamic Partial Order Reduction
Combining the Sweep-Line Method with the Use of an External-Memory Priority Queue
A SPIN-Based Model Checker for Telecommunication Protocols
Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin
SIMPAL: a compositional reasoning framework for imperative programs
Verification of Medical Guidelines by Model Checking - A Case Study
Property-Driven Benchmark Generation
Gossiping Girls Are All Alike
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs
Local Parallel Model Checking for the Alternation-Free µ-Calculus
Model Checking Software - 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings
BEEM: Benchmarks for Explicit Model Checkers
Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN
Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks
Model Checking Genetic Regulatory Networks Using GNA and CADP
Modeling and Verification of Interactive Flexible Multimedia Presentations Using PROMELA/SPIN
Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9-10, 2003, Proceedings
Generic Verification of Security Protocols
Tool Presentation: Teaching Concurrency and Model Checking
Comparative Analysis of Leakage Tools on Scalable Case Studies
On Refinement of Büchi Automata for Explicit Model Checking
Runtime enforcement using Büchi games
Improving Non-Progress Cycle Checks
Symmetry Reduction Criteria for Software Model Checking
Logic Verification of ANSI-C Code with SPIN
Verification of Java Programs Using Symbolic Execution and Invariant Generation
Symbolic Game Semantics for Model Checking Program Families
Fast and Accurate Bitstate Verification for SPIN
From Helena Ensemble Specifications to Promela Verification Models
Experimental Comparison of Concolic and Random Testing for Java Card Applets
Symbolic Execution with Abstract Subsumption Checking
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Program Sketching via CTL* Model Checking
Interaction Abstraction for Compositional Finite State Systems
Fifteen Years of Formal Property Verification in Intel
Addressing Dynamic Issues of Program Model Checking
Practical controller synthesis for MTL 0, ∞