yusuke1997/dblp-id-title huggingface dataset:
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Shape Analysis in the Absence of Pointers and Structure
An Abort-Aware Model of Transactional Programming
Software Verification with Liquid Types
Policy Iteration-Based Conditional Termination and Ranking Functions
Atomic Gliders and Cellular Automata as Language Generators
Predicate Abstraction for Linked Data Structures
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Verification of Concurrent Programs Using Petri Net Unfoldings
Flow-Sensitive Fault Localization
A Simulation Preorder for Abstraction of Reactive Systems
A Logical System for Modular Information Flow Verification
Abstract Interpretation-Based Feature Importance for Support Vector Machines
Lazy but Effective Functional Synthesis
Certifying Temporal Properties for Compiled C Programs
A General Framework for Probabilistic Characterizing Formulae
Constraint Solving for Interpolation
Fixing Code that Explodes Under Symbolic Evaluation
Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs
Abstraction-driven Concolic Testing
Reductions for Synthesis Procedures
Lightweight Shape Analysis Based on Physical Types
Properties of a Type Abstract Interpreter
Constructing Specialized Shape Analyses for Uniform Change
Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings
Monitoring the Full Range of omega-Regular Properties of Stochastic Systems
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
Strengthening Induction-Based Race Checking with Lightweight Static Analysis
Compositional and Lightweight Dependent Type Inference for ML
Solving Nonlinear Integer Arithmetic with MCSAT
Model Checking of Systems Employing Commutative Functions
Decision Procedures for Automating Termination Proofs
Sufficient Preconditions for Modular Assertion Checking
Abstraction-Based Interaction Model for Synthesis
Exact Heap Summaries for Symbolic Execution
Improved Model Checking of Hierarchical Systems
Syntactic Partial Order Compression for Probabilistic Reachability
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties
A Logic-Based Framework for Verifying Consensus Algorithms
Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
Using Abstract Interpretation to Correct Synchronization Faults
Average-Price-per-Reward Games on Hybrid Automata with Strong Resets
A Design of GPU-Based Quantitative Model Checking
Inferring Canonical Register Automata
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
Decision Procedures for Multisets with Cardinality Constraints
Automatic Inference of Relational Object Invariants
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines
High Assurance Software for Financial Regulation and Business Platforms
Timing Analysis of Parallel Software Using Abstract Execution
Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I
Fast BGP Simulation of Large Datacenters
Revisiting MITL to Fix Decision Procedures
Sound and Complete Flow Typing with Unions, Intersections and Negations
What's Decidable About Arrays?
Reduction of Workflow Nets for Generalised Soundness Verification
Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications
Improving the Encoding of LTL Model Checking into SAT
On the Complexity of Error Explanation
Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers
Guaranteed Inference for Probabilistic Programs: A Parallelisable, Small-Step Operational Approach
Conjunctive Abstract Interpretation Using Paramodulation
Liveness with Invisible Ranking
Sound Non-statistical Clustering of Static Analysis Alarms
Termination of Polynomial Programs
Data Race Detection by Digest-Driven Abstract Interpretation
Abstract Interpretation of Cellular Signalling Networks
Practical Floating-Point Tests with Integer Code
The Correctness of a Code Generator for a Functional Language
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I
Optimized Live Heap Bound Analysis
Static Analysis of String Encoders and Decoders
Semantic Hierarchy Refactoring by Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings
From LTL to Symbolically Represented Deterministic Automata
Reward-Bounded Reachability Probability for Uncertain Weighted MDPs
Uncovering Symmetries in Irregular Process Networks
Symmetry Reductions in Model-Checking
Synthesis with Identifiers
More Precise Yet Widely Applicable Cost Analysis
Refuting Heap Reachability
Efficient Verification of Timed Automata with BDD-Like Data-Structures
Complexity of Nesting Analysis in Mobile Ambients
Model Checking for Object Specifications in Hidden Algebra
Advances in Program Termination and Liveness
Considerate Reasoning and the Composite Design Pattern
Bringing LTL Model Checking to Biologists
A Constraint Solver Based on Abstract Domains
STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking
Constructing Trustworthy Smart Contracts
Witnessing Secure Compilation
Program Analysis and Programming Languages for Security
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Using Simulated Execution in Verifying Distributed Algorithms
On the Termination of Integer Loops
The Verifying Compiler, a Grand Challenge for Computing Research
Improving Parity Game Solvers with Justifications
A Generic Framework to Coarse-Grain Stochastic Reaction Networks by Abstract Interpretation
Relational String Abstract Domains
TP-DejaVu: Combining Operational and Declarative Runtime Verification
AGNES: Abstraction-Guided Framework for Deep Neural Networks Security
Symbolic Abstract Heaps for Polymorphic Information-Flow Guard Inference
An Abstract Domain to Discover Interval Linear Equalities
D^3 : Data-Driven Disjunctive Abstraction
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
Static Monotonicity Analysis for lambda-definable Functions over Lattices
Generalized Arrays for Stainless Frames
Verification of an Error Correcting Code by Abstract Interpretation
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Satisfiability Modulo Custom Theories in Z3
LTL Generalized Model Checking Revisited
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
Modeling Parsimonious Putative Regulatory Networks: Complexity and Heuristic Approach
Modeling Asynchronous Message Passing for C Programs
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis
Internal and External Logics of Abstract Interpretations
Loop Verification with Invariants and Contracts
Detecting All High-Level Dataraces in an RTOS Kernel
Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning
StaticPersist: Compiler Support for PMEM Programming
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
I/O Efficient Directed Model Checking
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
Formalizing and Checking Multilevel Consistency
Environment Abstraction for Parameterized Verification
Proofs Methods for Bisimulation Based Information Flow Security
Fanoos: Multi-resolution, Multi-strength, Interactive Explanations for Learned Systems
A Model for Industrial Real-Time Systems
Logico-Numerical Max-Strategy Iteration
Approximate Probabilistic Model Checking
Probabilistic Verification for Modular Network-on-Chip Systems
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
Automatic Verification of RMA Programs via Abstraction Extrapolation
Reachability for Dynamic Parametric Processes
Shape Analysis of Low-Level C with Overlapping Structures
Deciding Extensions of the Theories of Vectors and Bags
Solving $\mathrm {LIA} ^\star $ Using Approximations
Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
Proving Stabilization of Biological Systems
Property Directed Polyhedral Abstraction
Automata Learning with Automated Alphabet Abstraction Refinement
Efficient Computation of Recurrence Diameters
Interpolants and Symbolic Model Checking
Property Directed Abstract Interpretation
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
Model-Guided Synthesis for LTL over Finite Traces
Lazy Synthesis
A CLP Method for Compositional and Intermittent Predicate Abstraction
Efficient Discovery of Actual Causality in Stochastic Systems
Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings
Dependent Array Type Inference from Tests
Distributed and Predictable Software Model Checking
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
Automatic Generation of Propagation Complete SAT Encodings
Optimizing Bounded Model Checking for Linear Hybrid Systems
The Arithmetic-Geometric Progression Abstract Domain
Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings
A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs
The Spotlight Principle
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Effective Synthesis of Asynchronous Systems from GR(1) Specifications
Abstract Interpretation with Alien Expressions and Heap Structures
Approximation Refinement for Interpolation-Based Model Checking
Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation - (Invited Talk)
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking
A Fully Verified Persistency Library
Selfless Interpolation for Infinite-State Model Checking
Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety
Symbolic Implementation of the Best Transformer
Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems
Automata-Theoretic Decision of Timed Games
Relatively Complete Pushdown Analysis of Escape Continuations
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
Towards Complete Reasoning about Axiomatic Specifications
Synthesis for Polynomial Lasso Programs
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
From Verification to Optimizations
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Sound Bit-Precise Numerical Domains
Abstract Interpretation-Based Certification of Assembly Code
Finding Photonics Circuits via δ-Weakening SMT
Automatic Verification of Probabilistic Free Choice
Minimal Synthesis of String to String Functions from Examples
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
Reducing Behavioural to Structural Properties of Programs with Procedures
Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE
Analysis of Recursive Game Graphs Using Data Flow Equations
Access Analysis-Based Tight Localization of Abstract Memories
Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings
History-Dependent Scheduling for Cryptographic Processes
Static Analysis versus Software Model Checking for Bug Finding
Termination of Nondeterministic Probabilistic Programs
Parameterized Verification of Disjunctive Timed Networks
Tree Automata-Based Refinement with Application to Horn Clause Verification
Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings
Constraint-Based Invariant Inference over Predicate Abstraction
Effective Bug Finding in C Programs with Shape and Effect Abstractions
Boosting Constrained Horn Solving by Unsat Core Learning
Precise Set Sharing Analysis for Java-Style Programs
Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training
Widening for Control-Flow
Modular Analysis of Executables Using On-Demand Heyting Completion
Borrowable Fractional Ownership Types for Verification
Generating Tests by Example
Gradual Program Verification
Abstraction of Expectation Functions Using Gaussian Distributions
Solving and Interpolating Constant Arrays Based on Weak Equivalences
Don't Know in the µ-Calculus
From Shapes to Amortized Complexity
Efficient Elimination of Redundancies in Polyhedra by Raytracing
Verifying Array Programs by Transforming Verification Conditions
Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings
A Static Analysis of Entanglement
Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings
Construction of a Semantic Model for a Typed Assembly Language
Sets with Cardinality Constraints in Satisfiability Modulo Theories
Storage Size Reduction by In-place Mapping of Arrays
Ranking Abstraction of Recursive Programs
On the Expressiveness of 3-Valued Models
DIVINE: DIscovering Variables IN Executables
Relative Safety
Automatic Program Repair Using Formal Verification and Expression Templates
Proving the Existence of Fair Paths in Infinite-State Systems
On the Verification of the Correctness of a Subgraph Construction Algorithm
Invariant Generation for Multi-Path Loops with Polynomial Assignments
Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability
SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
Finding Relevant Templates via the Principal Component Analysis
Applying Jlint to Space Exploration Software
Interpolation and Quantifiers in Ortholattices
An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
On Flat Programs with Lists
Reduced Product Combination of Abstract Domains for Shapes
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
A Complete Method for the Synthesis of Linear Ranking Functions
Demand Control-Flow Analysis
Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness
Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Deriving Bisimulations by Simplifying Partitions
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)
Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings
Regression Verification for Multi-threaded Programs
Monitoring Off-the-Shelf Components
Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives
IC3 - Flipping the E in ICE
Shape Analysis with Reference Set Relations
Resilience and Home-Space for WSTS
Parameterized Model Checking of Token-Passing Systems
A Self-certifying Compilation Framework for WebAssembly
Program Analysis with Local Policy Iteration
Access Nets: Modeling Access to Physical Spaces
SMT-Based Bisimulation Minimisation of Markov Models
Sound Symbolic Execution via Abstract Interpretation and Its Application to Security
A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal
Verification of Register Allocators
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone
Automatic Verification of Intermittent Systems
Loop Invariant Symbolic Execution for Parallel Programs
Partitioned Memory Models for Program Analysis
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
On the Expressive Power of Canonical Abstraction
More Precise Partition Abstractions
P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols
Doomsday Equilibria for Omega-Regular Games
Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems
Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
Static Analysis of Binary Code with Memory Indirections Using Polyhedra
Automatic Inference of Access Permissions
An Overview of Semantics for the Validation of Numerical Programs
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
Collective Assertions
On Preprocessing for Weighted MaxSAT
CTL as an Intermediate Language
Shape Analysis through Predicate Abstraction and Model Checking
Minimizing Counterexample with Unit Core Extraction and Incremental SAT
An Evaluation of Automata Algorithms for String Analysis
Domain Compression for Complete Abstractions
Security, Protocols, and Trust
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic
BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results
Interpolant Strength
Shape Analysis by Predicate Abstraction
Cheap CTL Compassion in NuSMV
On abstraction and compositionality for weak-memory linearisability
Automata as Proofs
Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems
Extending Model Checking with Dynamic Analysis
Independence Abstractions and Models of Concurrency
Automatic Verification by Abstract Interpretation
Automatic Inference of Necessary Preconditions
Mostly-Functional Behavior in Java Programs
Formal Runtime Error Detection During Development in the Automotive Industry
Deductive Verification of Parameterized Embedded Systems Modeled in SystemC
Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, AIOOL@VMCAI 2005, Paris, France, January 21, 2005
Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings
Cloud-Based Verification of Concurrent Software
Abstraction of Arrays Based on Non Contiguous Partitions
Purity and Side Effect Analysis for Java Programs
A Systematic Approach to Abstract Interpretation of Program Transformations
Complexity Results on Branching-Time Pushdown Model Checking
Twinning Automata and Regular Expressions for String Static Analysis
Petrification: Software Model Checking for Programs with Dynamic Thread Management
Synthesizing Protocols for Digital Contract Signing
Finding Concurrency-Related Bugs Using Random Isolation
Ideal Abstractions for Well-Structured Transition Systems
Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs
Analyzing Cryptographic Protocols in a Reactive Framework
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation
Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
Synthesis of Reactive(1) Designs
Invariant and Type Inference for Matrices
Compositional Sequentialization of Periodic Programs
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement
Abstract Interpretation of the Physical Inputs of Embedded Programs
versat: A Verified Modern SAT Solver
Synthesizing Switching Logic Using Constraint Solving
Better Under-Approximation of Programs by Hiding Variables
euforia: Complete Software Model Checking with Uninterpreted Functions
Abstracting Induction by Extrapolation and Interpolation
Verification of Generic VHDL Designs and Their Translation to Rocq
Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings
Automatic Abstraction for Congruences
Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Language Inclusion for Finite Prime Event Structures
Fast Three-Valued Abstract Bit-Vector Arithmetic
Proof Minimization in Neural Network Verification
Abstract Read Permissions: Fractional Permissions without the Fractions
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
Type Inference for Parameterized Race-Free Java
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Verifying Compensating Transactions
Abstraction Refinement for Probabilistic Software
A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
A Model-Constructing Satisfiability Calculus
Quality Engineering: Leveraging Heterogeneous Information - (Invited Talk)
Verification of Well-Formed Communicating Recursive State Machines
Diagnostic Information for Realizability
Field Constraint Analysis
Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings
Compositional Termination Analysis of Symbolic Forward Analysis
Synthesizing Efficient Controllers
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
Abstraction-Guided Synthesis
Causality Checking for Complex System Models
Learning Algorithms and Formal Verification (Invited Tutorial)
Synchronous Closing of Timed SDL Systems for Model Checking
How to Win First-Order Safety Games
A Flow-Insensitive-Complete Program Representation
Crowfoot: A Verifier for Higher-Order Store Programs
All for the Price of Few
EPMC Gets Knowledge in Multi-agent Systems
Completeness and Complexity of Bounded Model Checking
Abstract Interpretation-Based Protection
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Efficient Strongly Relational Polyhedral Analysis
Compositional Model Checking for Multi-properties
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings
Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions
Affine Disjunctive Invariant Generation with Farkas' Lemma
A Forward-Backward Abstraction Refinement Algorithm
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem
Analysis of Systems with Stochastic Process Creation
Model Checking Algorithms for Hyperproperties (Invited Paper)
Application of Abstract Interpretation to the Automotive Electronic Control System
Verifying Concurrent Programs with Chalice
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
A Scalable Memory Model for Low-Level Code
Towards Automatic Stability Analysis for Rely-Guarantee Proofs
Bayesian Parameter Estimation with Guarantees via Interval Analysis and Simulation
Effective Abstractions for Verification under Relaxed Memory Models
Towards Shape Analysis for Device Drivers
All You Need Is Compassion
Error Control for Probabilistic Model Checking
Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning
Relational Thread-Modular Static Value Analysis by Abstract Interpretation
Refinement-Based CFG Reconstruction from Unstructured Programs
Piecewise FIFO Channels Are Analyzable