yusuke1997/dblp-id-title huggingface dataset:
Correction to: A survey of challenges for runtime verification from advanced application domains (beyond software)
SMT-based verification of program changes through summary repair
A Formal Theory of Simulations between Infinite Automata
2018 CAV award
Bounded model checking of infinite state systems
Modeling and visualizing object-oriented programs with Codecharts
Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
Test Case Verification by Model Checking
Automatic WSTS-based repair and deadlock detection of parameterized systems
Quantitative monitoring of STL with edit distance
Automatic assume-guarantee reasoning for safety and liveness using passive learning
The complexity gap in the static analysis of cache accesses grows if procedure calls are added
Preface of the special issue on the Conference on Computer-Aided Verification 2022
Cones and foci: A mechanical framework for protocol verification
Safety verification of non-linear hybrid systems is quasi-decidable
Priority scheduling of distributed systems based on model checking
Reducing concurrent analysis under a context bound to sequential analysis
Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs
Introduction to the Special Issue on Verification of Arithmetic Hardware
Reasoning about memory layouts
Formal Verification of a Distributed Computer System
Formal methods for mobile ad hoc networks: a survey
Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms
CEGAR for compositional analysis of qualitative properties in Markov decision processes
Limits of Using Signatures for Permutation Independent Boolean Comparison
Logic Based Abstractions of Real-Time Systems
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Model Checking at IBM
Pointfree expression and calculation: from quantification to temporal logic
An Overview of the Runtime Verification Tool Java PathExplorer
Introduction: Special Issue on the Fourth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, Trento, July 11-12, 1999 - Selected Papers
Translating VHDL into Functional Symbolic Finite-State Models
Verifying the Implementation of an Error Control Code
Formal Verification of Square Root Algorithms
Template polyhedra and bilinear optimization
Automatic symbolic compositional verification by learning assumptions
Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394
The symbolic OBDD scheme for generating mechanical assembly sequences
Scenario-based verification of real-time systems using Uppaal
Foreword to the special issue on the 2017 Static Analysis Symposium
2010 CAV award announcement
Model-Based Verification of a Security Protocol for Conditional Access to Services
SAT-Solving the Coverability Problem for Petri Nets
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs
A Unifying Theoretical Background for Some Bdd-based Data Structures
Runtime enforcement monitors: composition, synthesis, and enforcement abilities
Abstraction and mining of traces to explain concurrency bugs
Efficient Detection of Vacuity in Temporal Model Checking
The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor
Difficult Configurations-On the Complexity of LTrL
Partial bounding for recursive function synthesis
A Formal Verification Environment for Railway Signaling System Design
On the optimal reachability problem of weighted timed automata
Introduction: Special Issue on Partial Order in Formal Methods
Automatic Verification of Distributed Systems: The Process Algebra Approach
Model checking mobile ad hoc networks
Checking extended CTL properties using guarded quotient structures
Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs
Automatic analysis of DMA races using model checking and k -induction
Hybrid systems: from verification to falsification by combining motion planning and discrete search
Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment
Event clock message passing automata: a logical characterization and an emptiness checking algorithm
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement
Boolean functional synthesis: hardness and practical algorithms
Rule-Based Induction
A methodology to take credit for high-level verification during RTL verification
Local proofs for global safety properties
GSTE is partitioned model checking
Using Forward Reachability Analysis for Verification of Lossy Channel Systems
A Functional Rephrasing of the Assumption/Commitment Specification Style
Annotation guided collection of context-sensitive parallel execution profiles
Preface of the special issue on the conference on computer-aided verification 2018
Symbolic bounded synthesis
Relative Liveness: From Intuition to Automated Verification
Automated Analysis of Fault-Tolerance in Distributed Systems
The T-Ruby Design System
InterAspect: aspect-oriented instrumentation with GCC
Automating the addition of fault tolerance with discrete controller synthesis
An Experiment in Program Composition and Proof
Software doping analysis for human oversight
Reluplex: a calculus for reasoning about deep neural networks
Accommodating Interference in the Formal Design of Concurrent Object-Based Programs
Hybrid automata-based CEGAR for rectangular hybrid systems
Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability
Parameter synthesis for Markov models: covering the parameter space
On-the-fly verification and optimization of DTA-properties for large Markov chains
A WSDL-based type system for asynchronous WS-BPEL processes
Coverage-guided test generation for continuous and hybrid systems
Looped Schedules for Dataflow Descriptions of Multirate Signal Processing Algorithms
Verifying Time Partitioning in the DEOS Scheduling Kernel
Weighted modal transition systems
On-the-Fly Model Checking Under Fairness that Exploits Symmetry
Testing-based translation validation of generated code in the context of IEC 61508
Preface for the Formal Methods in System Design special issue on 'FASE 2022'
Symbolic unfolding of parametric stopwatch Petri nets
Formal Verification of Dynamic Properties in an Aerospace Application
Reasoning About Analog-Level Implementations of Digital Systems
A New Heuristic for Bad Cycle Detection Using BDDs
Markov automata with multiple objectives
Divider verification using symbolic computer algebra and delayed don't care optimization: theory and practical implementation
Achieving distributed control through model checking
Parameterized verification of leader/follower systems via first-order temporal logic
Action Language verifier: an infinite-state model checker for reactive software specifications
Percentile queries in multi-dimensional Markov decision processes
SAT modulo discrete event simulation applied to railway design capacity analysis
Correction: Hypercontracts
Verification of STM on relaxed memory models
Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness
Using Hybrid Automata to Support Human Factors Analysis in a Critical System
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
A Symbolic Algorithms for Maximum Flow in 0-1 Networks
Proving the Correctness of the Standardized Algorithm for ABR Conformance
The Implicit Set Paradigm: A New Approach to Finite State System Verification
Unified QBF certification and its applications
Feature interaction detection by pairwise analysis of LTL properties - A case study
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function
Introduction: Special Issue on Microprocessor Verifications
A divide-and-conquer approach for analysing overlaid data structures
A Comparative Study of Synthesis Methods for Discrete Event Controllers
Verisym: Verifying Circuits by Symbolic Simulation
Verification of evolving software via component substitutability analysis
Towards neural-network-guided program synthesis and verification
Combining Partial Order Reductions with On-the-Fly Model-Checking
The Theory of Zero-Suppressed BDDs and the Number of Knight's Tours
Property Preserving Abstractions for the Verification of Concurrent Systems
Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP
Timed substitutions for regular signal-event languages
Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects
Inferring functional properties of matrix manipulating programs by abstract interpretation
Fences in weak memory models (extended version)
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs
Monitorability for the Hennessy-Milner logic with recursion
Using Integer Programming to Verify General Safety and Liveness Properties
On using priced timed automata to achieve optimal scheduling
Formal Verification of Out-of-Order Execution with Incremental Flushing
Compact and efficiently verifiable models for concurrent systems
A Complete Mechanization of Correctness of a String-Preprocessing Algorithm
Automated Correctness Condition Generation for Formal Verification of Synthesized RTL Designs
Monitoring of temporal first-order properties with aggregations
Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System Revisiting Seven Myths of Formal Methods
Probabilistic contracts for component-based design
From Pre-Historic to Post-Modern Symbolic Model Checking
Java-MaC: A Run-Time Assurance Approach for Java Programs
Refutation-based synthesis in SMT
Runtime verification of partially-synchronous distributed system
Exploiting Symmetry in Temporal Logic Model Checking
Theorem prover approach to semistructured data design
On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification
Extending rely-guarantee thinking to handle real-time scheduling
Gordon's Computer: A Hardware Verification Case Study in OBJ3
Generating Model Checkers from Algebraic Specifications
Scalable offline monitoring of temporal specifications
Full simulation coverage for SystemC transaction-level models of systems-on-a-chip
Deciding floating-point logic with abstract conflict driven clause learning
Automatic proofs of memory deallocation for a Whiley-to-C Compiler
Parallelizing the Murj Verifier
A Mechanized Proof Environment for the Convenient Computations Proof Method
A Formal Framework for Verification of Embedded Custom Memories of the Motorola MPC7450 Microprocessor
Bounded Delay Timing Analysis of a Class of CSP Programs
Numerical invariants through convex relaxation and max-strategy iteration
Introduction to the Special Issue on Multi-Terminal Binary Decision Diagrams
Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01)
Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics
A Comparison of Free BDDs and Transformed BDDs
Doomed program points
Robust online monitoring of signal temporal logic
First-order temporal logic monitoring with BDDs
Quasi-optimal partial order reduction
A game approach to determinize timed automata
NP-completeness of small conflict set generation for congruence closure
Distributed disk-based algorithms for model checking very large Markov chains
Probabilistic Verification of Boolean Functions
Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
An empirical study of adaptive concretization for parallel program synthesis
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)
Industrial Practice of Formal Hardware Verification: A Sampling
Automata-based symbolic string analysis for vulnerability detection
Preface of the special issue on the Conference on Formal Methods in Computer-Aided Design 2017
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
Functional synthesis via input-output separation
Predicate Abstraction of ANSI-C Programs Using SAT
Hashing-based approximate counting of minimal unsatisfiable subsets
Preface of the Special Issue in Memoriam Helmut Veith
Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
Foreword: Special issue on numerical software verification
The ins and outs of first-order runtime verification
Statistical verification of PCTL using antithetic and stratified samples
Scalable reachability analysis via automated dynamic netlist-based hint generation
Translation and Run-Time Validation of Loop Transformations
Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis
Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
Specification and Automatic Verification of Self-Timed Queues
Integrating formal specifications into applications: the ProB Java API
Compositional SCC Analysis for Language Emptiness
Recognizing malicious software behaviors with tree automata inference
LTL model checking of self modifying code
Compared Study of Two Correctness Proofs for the Standardized
Compositional verification of priority systems using sharp bisimulation
A Technique of State Space Search Based on Unfolding
Dealing with practical limitations of distributed timed model checking for timed automata
Automated repair for timed systems
Feasibility analysis for robustness quantification by symbolic model checking
Global guidance for local generalization in model checking
Early verification and validation of mission critical systems
On the complexity of monitoring Orchids signatures, and recurrence equations
Fingerprinting and analysis of Bluetooth devices with automata learning
Analysis and Identification of Speed-Independent Circuits on an Event Model
Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory
Undefined Expressions and Logic in Z and B
Verification of continuous dynamical systems by timed automata
Cut-off theorems for the PV-model
SMT-based scenario verification for hybrid systems
On the Computational Power of Binary Decision Diagram with Redundant Variables
Benchmarking a model checker for algorithmic improvements and tuning for performance
Bayesian statistical model checking with application to Stateflow/Simulink verification
Symbolic Protocol Verification with Queue BDDs
Quantifier-free encoding of invariants for hybrid systems
Special issue on formal methods for globally asynchronous and locally synchronous (GALS) systems
Temporal prophecy for proving temporal properties of infinite-state systems
Synthesising correct concurrent runtime monitors
The probabilistic termination tool amber
Church synthesis on register automata over linearly ordered data domains
Structural Operational Semantics for a Portable Subset of Behavioral VHDL-93
Constructive Boolean circuits and the exactness of timed ternary simulation
A search-based procedure for nonlinear real arithmetic
A verified durable transactional mutex lock for persistent x86-TSO
Formal Verification Successes at Motorola
Bridging the gap between single- and multi-model predictive runtime verification
Asynchronous Datapaths and the Design of an Asynchronous Adder
A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits
An Analysis of Bitstate Hashing
Data-driven invariant learning for probabilistic programs
Towards efficient verification of population protocols
Formal Design of Cache Memory Protocols in IBM
Applying Formal Verification to the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods
Using Fixed-Point Semantics to Prove Retiming Lemmas
Exploiting partial variable assignment in interpolation-based model checking
Pushdown module checking
Formal analysis and offline monitoring of electronic exams
Reduction and Quantifier Elimination Techniques for Program Validation
Deadlock-freedom in component systems with architectural constraints
Efficient verification of railway infrastructure designs against standard regulations
Stratified guarded first-order transition systems
Synthesis of opaque systems with static and dynamic masks
Cardinality constraints for arrays (decidability results and applications)
A Practical Methodology for the Formal Verification of RISC Processors
Robust safety of timed automata
Program repair without regret
R2U2: monitoring and diagnosis of security threats for unmanned aerial systems
Automating regression verification of pointer programs by predicate abstraction
Factored Edge-Valued Binary Decision Diagrams
Efficient generation of small interpolants in CNF
Ranking function synthesis for bit-vector relations
Correction: (Un)Solvable loop analysis
Information-flow interfaces
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
Symbolic Verification and Analysis of Discrete Timed Systems
Combining Software and Hardware Verification Techniques
Analog property checkers: a DDR2 case study
Hierarchical Reachability Graph Generation for Petri Nets
Data structures for symbolic multi-valued model-checking
Algorithmic games for full ground references
Software Model Checking: The VeriSoft Approach
Conjugate symmetry
A Flowgraph Semantics of VHDL: Toward a VHDL Verification Workbench in HOL
Analysis of an Industrial System
Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment
Checking Finite Traces Using Alternating Automata
Almost event-rate independent monitoring
True Concurrency in Models of Asynchronous Circuit Behavior
Static priority scheduling of event-triggered real-time embedded systems
A Formalization of a Subset of VHDL in the Boyer-Moore Logic
Efficient Simulation of Formal Processor Models
Faster algorithms for mean-payoff games
Properties of Hybrid Systems-A Computer Science Perspective
Efficient emptiness check for timed Büchi automata
Efficient data race detection for async-finish parallelism
Relational abstract interpretation of arrays in assembly code
Multiway Decision Graphs for Automated Hardware Verification
Reachability computation for polynomial dynamical systems
On a Class of Optimal Abstractions of Finite-State Machines
Model checking approach to automated planning
Model Checking for Action-Based Logics
Special Issue on Syntax-Guided Synthesis Preface
Signal Transition Graph Constraints for Synthesis of Hazard-Free Asynchronous Circuits with Unbounded-Gate Delays
Learning inductive invariants by sampling from frequency distributions
Compositional runtime enforcement revisited
Abstractions of Random Finite-State Machines
An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation
A Colored Petri Net Model of VHDL
Time-triggered runtime verification
Computing differential invariants of hybrid systems as fixedpoints
A Unified Signal Transition Graph Model for Asynchronous Control Circuit Synthesis
Finding optimal hardware/software partitions
An Exercise in the Automatic Verification of Asynchronous Designs
From LTL to unambiguous Büchi automata via disambiguation of alternating automata
Enforcing termination of interprocedural analysis
On WLCDs and the Complexity of Word-Level Decision Diagrams-A Lower Bound for Division
Control strategies for off-line testing of timed systems
SMT proof checking using a logical framework
Colored nested words
Forward Analysis of Updatable Timed Automata
Constraint-Based Verification of Parameterized Cache Coherence Protocols
The Incorporation of Testing into Formal Verification: Direct, Modular, and Hierarchical Correctness Degrees
The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2
A scalable entropy estimator
Certified SAT solving with GPU accelerated inprocessing
Bounded satisfiability checking of $\hbox {FOL}^*$ formulas with aggregations
Transparent partial order reduction
Description of a Design Management System for the P-ASIC Design Flow Using EXPDL
A Constructive Approach to Hardware/Software Partitioning
Analysis of Timed Systems Using Time-Abstracting Bisimulations
TeLEx: learning signal temporal logic from positive examples using tightness metric
Formal Verification of a Complex Pipelined Processor
Reasoning about Action Systems using the B-Method
Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude
Safely composing security protocols
An approach for extracting a small unsatisfiable core
Theory and methodology of assumption/commitment based system interface specification and architectural contracts
The CAV award
Memory access protocols: certified data-race freedom for GPU kernels
Para 2 : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
Performance analysis of probabilistic timed automata using digital clocks
Learning analysis strategies for octagon and context sensitivity from labeled data generated by static analyses
A new abstraction framework for affine transformers
Vacuity in synthesis
An abstraction-refinement framework for trigger querying
Hiding Propositional Constants in BDDs
Word level bitwidth reduction for unbounded hardware model checking
Distributed bounded model checking
An Efficient Algorithm for Minimizing Real-Time Transition Systems
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
On multi-language abstraction: Towards a static analysis of multi-language programs
A predictive synchronizer for periodic clock domains
Non-Abelian Groups in Optimization of Decision Diagrams Representations of Discrete Functions
Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
Constructing the Real Numbers in HOL
On simulation-based probabilistic model checking of mixed-analog circuits
Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics
Memory model sensitive bytecode verification
Mechanizing Some Advanced Refinement Concepts
Context-aware counter abstraction
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems
Wireless protocol validation under uncertainty
Summarization for termination: no return!
Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning
Accelerating Tableaux Proofs Using Compact Representations
Equivalence checking and intersection of deterministic timed finite state machines
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation
Inferring event stream abstractions
From invariant checking to invariant inference using randomized search
On compiling Boolean circuits optimized for secure multi-party computation
Accelerating Bounded Model Checking of Safety Properties
Certifying compilers using higher-order theorem provers as certificate checkers
Vacuity in practice: temporal antecedent failure
Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components
Memory-efficient fixpoint computation
Construction of verifier combinations from off-the-shelf components
Extended symbolic finite automata and transducers
Timed verification of the generic architecture of a memory circuit using parametric timed automata
An extension of the inverse method to probabilistic timed automata
SMT-based model checking for recursive programs
The word problem for visibly pushdown languages described by grammars