yusuke1997/dblp-id-title huggingface dataset:
A Framework for Defining Logics
Axiomatizable Classes of Finite Models and Definability of Linear Order
Lovász-Type Theorems and Game Comonads
The Geometry of Linear Higher-Order Recursion
High-Level Methods for Quantum Computation and Information
Type-Based Productivity of Stream Definitions in the Calculus of Constructions
Logical Foundations of Quantitative Equality
Equivariant ideals of polynomials
Some Results on the Interpretation of lambda-calculus in Operator Algebras
On Hoare Logic and Kleene Algebra with Tests
Polymorphism is conservative over simple types (Preliminary Report)
On symmetries of spheres in univalent foundations
Weighted Relational Models of Typed Lambda-Calculi
Subtyping Dependent Types (Summary)
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Relativized Logspace and Generalized Quantifiers over Finite Structures
The Strength of the Subset Type in Martin-Löf's Type Theory
Proving Liveness of Parameterized Programs
From Verification to Control: Dynamic Programs for Omega-Regular Objectives
On the Cubic Bottleneck in Subtyping and Flow Analysis
On the Axiomatizability of Impossible Futures: Preorder versus Equivalence
Piecewise Testable Tree Languages
A Contraction Method to Decide MSO Theories of Deterministic Trees
Ludics with Repetitions (Exponentials, Interactive Types and Completeness)
Compressing Polarized Boxes
Higher-Kinded Data Types: Syntax and Semantics
Higher-order parity automata
Towards Action-Refinement in Process Algebras
On the Power of Symmetric Linear Programs
Composing Codensity Bisimulations
A Fully Abstract Game Semantics for Finite Nondeterminism
A Computation Model for Executable Higher-Order Algebraic Specification Languages
From Axioms to Analytic Rules in Nonclassical Logics
A Sheaf-Theoretic Model of Concurrency
Linear Logic With Boxes
Bialgebraic Operational Semantics and Modal Logic
First-order logic with counting
On the denotation of circular and non-wellfounded proofs in linear logic with fixed points
Categorical Semantics for Time Travel
A Metalanguage for Cost-Aware Denotational Semantics
Order Invariance on Decomposable Structures
Plausibility Measures and Default Reasoning: An Overview
Complexity of Two-Variable Logic with Counting
Allegories: decidability and graph homomorphisms
The Planning Spectrum - One, Two, Three, Infinity
Asymptotic Probabilities of Languages with Generalized Quantifiers
Infinitary Lambda Calculi from a Linear Perspective
A Probabilistic Powerdomain of Evaluations
Equivalences on Observable Processes
Variables as Resource in Hoare Logics
Extending the Lambda Calculus with Surjective Pairing is Conservative
Tree-like Queries in OWL 2 QL: Succinctness and Complexity Results
An Algebraic Process Calculus
On Recurrent Reachability for Continuous Linear Dynamical Systems
Rigid E-Unifiability is DEXPTIME-Complete
Improved Algorithms for One-Pair and k-Pair Streett Objectives
Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension
A Categorical Linear Framework for Petri Nets
The Axiomatic Derivation of Absolute Lower Bounds
Infinite Objects in Type Theory
Complexity Classes, Propositional Proof Systems, and Formal Theories
The logic of counting query answers
Fully Abstract Logical Bisimilarity for a Polymorphic Object Calculus
An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990
A Survey of Elementary Object Systems
Segal Condition Meets Computational Effects
Untwisting two-way transducers in elementary time
Compositional Testing Preorders for Probabilistic Processes
Semantical Analysis of Higher-Order Abstract Syntax
A Unified Sequent Calculus for Focused Proofs
On Bunched Predicate Logic
A Complete Proof Systems for QPTL
Specifying and Proving Serializability in Temporal Logic
Dependent Types for Program Termination Verification
Proof by Consistency in Equational Theories
Higher-Dimensional Subdiagram Matching
The Dynamic Logic of Permission
Clipping: A Semantics-Directed Syntactic Approximation
A Proof System for Reasoning about Probabilistic Concurrent Processes
A Fully Abstract Game Semantics of Local Exceptions
Continuous Reasoning: Scaling the impact of formal methods
Decidability Problems for the Prenex Fragment of Intuitionistic Logic
Linearity in Process Languages
An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC
Arbitrary Action Model Logic and Action Model Synthesis
Logics with Aggregate Operators
Quantifier Elimination for Regular Integer Linear-Exponential Programming
Modular Construction of Cut-free Sequent Calculi for Paraconsistent Logics
Set Constraints with Intersection
Coherence and Consistency in Domains (Extended Outline)
A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names
On delay and regret determinization of max-plus automata
Graded Computation Tree Logic
Towards a Cut-free Sequent Calculus for Boolean BI
Lower Bounds for QBFs of Bounded Treewidth
Operational Domain Theory and Topology of a Sequential Programming Language
Branching Bisimilarity on Normed BPA Is EXPTIME-Complete
Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity
The Metric Analogue of Weak Bisimulation for Probabilistic Processes
Reflections on Finite Model Theory
Logical paradoxes in quantum computation
Explicit Clock Temporal Logic
Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?
The Monadic Quantifier Alternation Hierarchy over Graphs is Infinite
Semantics of Meta-Logic in an Algebra of Programs
A first-order completeness result about characteristic Boolean algebras in classical realizability
Term Declaration Logic and Generalised Composita
Strong Call-by-Value is Reasonable, Implosively
Presburger Vector Addition Systems
The boundedness and zero isolation problems for weighted automata over nonnegative rationals
Complexity Bounds of Hoare-style Proof Systems
Defining algorithmically presented structures in first order logic
Counting Modulo Quantifiers on Finite Linearly Ordered Trees
Countermodels from Sequent Calculi in Multi-Modal Logics
Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma
The Complexity of Proving the Discrete Jordan Curve Theorem
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
The Design and Implementations of Intuit
Unifying Classical and Intuitionistic Logics for Computational Control
Data structures for quasistrict higher categories
Provable Implementations of Security Protocols
Combining probabilistic and non-deterministic choice via weak distributive laws
Type inference and logical relations
General Decidability Theorems for Infinite-State Systems
Three-Valued Abstractions of Games: Uncertainty, but with Precision
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991
The Qualitative Collapse of Concurrent Games
Separability, Expressiveness, and Decidability in the Ambient Logic
Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields
The Complexity of Dynamic Data Race Prediction
A Compositional Cost Model for the λ-calculus
Navigational hierarchies of regular languages
Saturated Semantics for Reactive Systems
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
Stratified Polymorphism (Extended Summary)
Universal Covers, Color Refinement, and Two-Variable Counting Logic: Lower Bounds for the Depth
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
Virtual Symmetry Reduction
Partial derivatives on graphs for Kleene allegories
Eager Functions as Processes
Strong Normalization for Second Order Classical Natural Deduction
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
Groupoids, Hypergraphs, and Symmetries in Finite Models
Efficient Representation and Validation of Proofs
The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)
Universal Skolem Sets
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus
One-Clock Priced Timed Games are PSPACE-hard
From Multisets over Distributions to Distributions over Multisets
The Theory of Hybrid Automata
The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations
Type Inference and Extensionality
Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees
Unary negation fragment with equivalence relations has the finite model property
A Fully Abstract Denotational Model for Higher-Order Processes (Extended Abstract)
A proof theory of right-linear (ω-)grammars via cyclic proofs
Dot-depth three, return of the J-class
Semantics of a Sequential Language for Exact Real-Number Computation
On the Complexity of Abduction
Strong Sequentiality of Left-Linear Overlapping Term Rewriting Systems
A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics
The Emptiness Problem for Tree Automata with Global Constraints
Normalization for Multimodal Type Theory
Experience with Type Theory as a Foundation for Computer Science
Alignment Completeness for Relational Hoare Logics
Bayesian Kernel Methods
A Short Introduction to Learning with Kernels
An Introduction to Boosting and Leveraging
Learning Comprehensible Theories from Structured Data
Advanced Lectures on Machine Learning, Machine Learning Summer School 2002, Canberra, Australia, February 11-22, 2002, Revised Lectures
A Few Notes on Statistical Learning Theory
An Introduction to Reinforcement Learning Theory: Value Function Methods
Algorithms for Association Rules
Online Learning of Linear Classifiers
ISO/IEC Standards and Design of an Artificial Intelligence System
Short Paper Proceedings of the 6th International Workshop on Experience with SQuaRE Family and Its Future Direction co-located with 31th Asia-Pacific Software Engineering Conference (APSEC 2024), Chongqing, China, December 3th, 2024
AI Evaluation and ISO Standards: Is the Gap Closed?
Considerations and Proposals for Quality Engineering in the Context of SQuaRE
Data and Dataset Quality for Artificial Intelligence Systems
A Path Discovery Method of Penetration Testing Based on SAC Reinforcement Learning
Research on Quality Assurance Methods for Software Products Based on Low Code Development
Strategic Quality Management Approach in SI Projects
Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip
Exact and Efficient Verification of Parameterized Cache Coherence Protocols
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '95, Frankfurt/Main, Germany, October 2-4, 1995, Proceedings
A partial-order approach to the verification of concurrent systems: checking liveness properties
Hierarchical Verification Using an MDG-HOL Hybrid Tool
Problems encountered in the machine-assisted proof of hardware
Proof Engineering in the Large: Formal Verification of Pentium ® 4 Floating-Point Divider
A Specification Methodology by a Collection of Compact Properties as Applied to the Intel ® Itanium TM Processor Bus Protocol
Finite Horizon Analysis of Markov Chains with the Mur-phi Verifier
Coverability Analysis Using Symbolic Model Checking
Formal support for the ELLA hardwar description language
Verifying hardware components within JACK
Improved Symbolic Verification Using Partitioning Techniques
Transforming boolean relations by symbolic encoding
Verification Challenges in Configurable Processor Design with ASIP Meister
Pruning Techniques for the SAT-Based Bounded Model Checking Problem
Verification and Diagnosis of Digital Systems by Termary Reasoning
A Graph-Based Method for Timing Diagrams Representation and Verification
An approach to Verilog-VHDL interoperability for synchronous designs
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment
A Higher-Level Language for Hardware Synthesis
Validation of Object-Oriented Concurrent Designs by Model Checking
FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers
Strongly-Typed Theory of Structures and Behaviours
A Systematic Incrementalization Technique and Its Application to Hardware Design
Automatic verification of the SCI cache coherence protocol
Convergence Testing in Term-Level Bounded Model Checking
Formally-Based Design Evaluation
Symbolic Partial Order Reduction for Rule Based Transition Systems
Towards the Pervasive Verification of Automotive Systems
High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design
Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors
Vacuity Detection in Temporal Model Checking
Interleaved Invariant Checking with Dynamic Abstraction
Wired: Wire-Aware Circuit Design
Verifying Quantitative Properties Using Bound Functions
A Theory of Generic Interpreters
Heuristics for Hierarchical Partitioning with Application to Model Checking
Model Checking TLA + Specifications
Exploiting Constraints in Transformation-Based Verification
Symbolic model checking for a discrete clocked temporal logic with intervals
Design and Verification of CoreConnectTM IP Using Esterel
CheckOff-M: model checking and its role in IP
Refinement and Property Checking in High-Level Synthesis using Attribute Grammars
Algebraic Models and the Correctness of Microprocessors
Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular
Automatic Verification of Speed-Independent Circuit Designs Using the Circal System
Hardware Synthesis Using SAFL and Application to Processor Design
Improved probabilistic verification by hash compaction
Improvements to the Implementation of Interpolant-Based Model Checking
Bisimulation and Model Checking
Net Reductions for LTL Model-Checking
Hazard-Freedom Checking in Speed-Independent Systems
Efficient CTL* model checking for analysis of rainbow designs
Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs
Timing analysis of asynchronous circuits using timed automata
State enumeration with abstract descriptions of state machines
Temporal Modalities for Concisely Capturing Timing Diagrams
ASIC/system hardware verification at Nortel: a view from the trenches
Deriving Real-Time Programs from Duration Calculus Specifications
What if model checking must be truly symbolic
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification
Efficient Debugging in a Formal Verification Environment
Calculational Derivation of a Counter with Bounded Response Time
Hints to accelerate Symbolic Traversal
A parallel approach to symbolic traversal based on set partitioning
Efficient Decompositional Model Checking for Regular Timing Diagrams
A Programming Language Based Analysis of Operand Forwarding
Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies
Introducing Abstractions via Rewriting
On the Correctness of an Intrusion-Tolerant Group Communication Protocol
Formal Synthesis at the Algorithmic Level
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specification
Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting
Correct Compilation of Specifications to Deterministic Asynchronous Circuits
Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '93, Arles, France, May 24-26, 1993, Proceedings
Symbolic analysis and verification of CPA descriptions
Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings
Describing and verifying synchronous circuits with the Boyer-Moore theorem prover
Advancements in Symbolic Traversal Technique
Exploiting Retiming in a Guided Simulation Based Validation Methodology
Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming
Towards Diagrammability and Efficiency in Event Sequence Languages
A Hazards-Based Correctness Statement for Pipelined Circuits
Abstract BDDs: A Technique for Using Abstraction in Model Checking
Linear and Nonlinear Arithmetic in ACL2
A Framework for Microprocessor Correctness Statements
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking
Implementation of a multiple-domain decision diagram package
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer
Reasoning about GSTE Assertion Graphs
Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques
Automatic post-synthesis verification support for a high level synthesis step by using the HOL theorem proving system
Resolving Quartz Overloading
Constrained Symbolic Simulation with Mathematica and ACL2
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems
CTL May Be Ambiguous When Model Checking Moore Machines
Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning
On Complementing Nondeterministic Büchi Automata
Program Slicing of Hardware Description Languages
Results of the Verification of a Complex Pipelined Machine Model
Automatic Generation of Hints for Symbolic Traversal
Towards a Provably Correct Hardware Implementation of Occam
Verifying out-of-order executions
Modleing and Checking Networks of Communicating Real-Time Process
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units
View from the Fringe of the Fringe
Multiclock Esterel
Register Transformations with Multiple Clock Domains
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP
Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell
Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction
Verification of Basic Block Schedules Using RTL Transformations
Semantics of a verification-oriented subset of VHDL
Formalization of the DE2 Language
The Design and Verification of a Sorter Core
Design error diagnosis in sequential circuits
Circular Compositional Reasoning about Liveness
Yet another Look at the LTL Model Checking
How Thorough Is Thorough Enough?
Inductive Assertions and Operational Semantics
Formal Verification of the VAMP Floating Point Unit
Formal Verification of Designs with Complex Control by Symbolic Simulation
Xs are for Trajectory Evaluation, Booleans are for Theorem Proving
Temporal Properties of Self-Timed Rings
Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings
The Charme of Abstract Entities
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation
Using induction and BDDs to model check invariants
A Symbolic Relation for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking
Induction-Oriented Formal Verification in Symmetric Interconnection Networks
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard
Deadlock Prevention in the Æthereal Protocol
Formal Pipeline Design
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
Regular Vacuity
Effcient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning
A polymodal semantics for VHDL
Verification of Infinite State Systems by Compositional Model Checking
A Methodology for System-Level Design for Verifiability
Predicate Abstraction with Minimum Predicates
Design and Implementation of an Abstract Interpreter for VHDL
Minimizing Counterexample of ACTL Property
Real-Time Model Checking Is Really Simple
Finding and Fixing Faults
Using Combinatorial Optimization Methods for Quantification Scheduling
On the Verification of Memory Management Mechanisms
From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking
Exploiting Transition Locality in Automatic Verification
Integrating RAM and Disk Based Verification within the Mur-phi Verifier
An Optimized Symbolic Bounded Model Checking Engine
Towards Verifying Large(r) Systems: A Strategy and an Experiment
Formal Verification of Synchronizers
Coverage Metrics for Formal Verification
Specifying Hardware Timing with ET-L OTOS
Using Abstract Specifications to Verify PowerPC TM Custom Memories by Symbolic Trajectory Evaluation
Data Refinement for Synchronous System Specification and Construction
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology
Language containment of non-deterministic omega -automata
DDD-FM9001: Derivation of a Verified Microprocessor
A Case Study: Formal Verification of Processor Critical Properties
A semantic model for VHDL-AMS
Is there a crisis in hardware verification?
The ROBDD Size of Simple CNF Formulas
"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation
A Compositional Theory of Refinement for Branching Time
Advances in Hardware Design and Verification, IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods, 16-18 October 1997, Montréal, Québec, Canada
Simulation-based verification of network protocols performance
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking
Integrated reasoning support in system design: design derivation and theorem proving
On the non-termination of MDGs-based abstract state enumeration
Verifying Timing Behavior by Abstract Interpretation of Executable Code
Rewriting with Constraints in T-Ruby
Identification and Counter Abstraction for Full Virtual Symmetry
Acceleration of SAT-Based Iterative Property Checking
Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract)
Combining Symbolic Evaluation and Object-Oriented Approach for Verifying Processor-Like Architectures at the RT-Level
Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic
Embedding Hardware Verification Within a Commercial Design Framework
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
Proving the correctness of the interlock mechanism in processor design
Reproducing Synchronization Bugs with Model Checking
Logic Verification of Incomplete Functions and Design Error Location
Formal modeling and validation applied to a commercial coherent bus: a case study
The PSL/Sugar Specification Language A Language for all Seasons
Semi-formal Verification of Memory Systems by Symbolic Simulation
Formal Verification of Conflict Detection Algorithms
What Is beyond the RTL Horizon for Microprocessor and System Design?
Model checking without hardware drivers
An Approach to Formalization of Data Flow Graphs
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings
Formal Verification of Explicitly Parallel Microprocessors
From Operational Semantics to Denotational Semantics for Verilog
A Petri Net Approach for the Analysis of VHDL Descriptions
Fault Models for Embedded Systems (Extended Abstract)
Formally embedding existing high level synthesis algorithms
A New SAT-Based Algorithm for Symbolic Trajectory Evaluation
Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths