yusuke1997/dblp-id-title huggingface dataset:
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic
LCF-Style Propositional Simplification with BDDs and SAT Solvers
S: A Machine Readable Specification Notation based on Higher Order Logic
Using Lattice Theory in Higher Order Logic
Verified Lexical Analysis
Autotically Synthesized Term Denotation Predicates: A Proof Aid
Formal Verification of Serial Pipeline Multipliers
Formalizing Hilbert's Grundlagen in Isabelle/Isar
First Steps Towards Automating Hardware Proofs in HOL
Simple Types in Type Theory: Deep and Shallow Encodings
Value-Passing CCS in HOL
Formalizing Convex Hull Algorithms
Program Verification using HOL-UNITY
Isomorphisms - A Link Between the Shallow and the Deep
Recursive Function Definition over Coinductive Types
Derivation and Use of Induction Schemes in Higher-Order Logic
Verifying Nonlinear Real Formulas Via Sums of Squares
Applications of Polytypism in Theorem Proving
Finite Set Theory in ACL2
Reasoning about Proof Search Specifications: An Abstract
A Formalization of Abstraction in LAMBDA
On the Refinement of symmetric memory protocols
A Mizar Mode for HOL
Machine Abstraction in Microprocessor Specification
An Engineering Approach to Formal Digital System Design
Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings
Type-Theoretic Functional Semantics
Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings
A Comparison between Statecharts and State Transition Assertions
Alpha-Structural Recursion and Induction
Error Analysis of Digital Filters Using Theorem Proving
On the Style of Mechanical Proving
Proof Terms for Simply Typed Higher Order Logic
From I/O Automata to Timed I/O Automata
Improving the Usability of HOL Through Controlled Automation Tactics
Binary Decision Diagrams as a HOL Derived Rule
Extending Window Inference
Formal Techniques in Software Engineering: Correct Software and Safe Systems
Locales - A Sectioning Concept for Isabelle
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2
Turning Inductive into Equational Specifications
Proving Equalities in a Commutative Ring Done Right in Coq
Extensionality in the Calculus of Constructions
Combining Testing and Proving in Dependent Type Theory
Formalizing Dijkstra
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System
Coq and Hardware Verification: A Case Study
An ACL2 Tutorial
Interfacing HOL90 with a Functional Database Query Language
Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings
A Coverage Checking Algorithm for LF
VCC: A Practical System for Verifying Concurrent C
Proving Hybrid Protocols Correct
Verification of Integrated Subsystems
Safety in Railway Signalling Data: A Behavioural Analysis
Specification and Verification of a Steam-Boiler with Signal-Coq
Disjoint Sums over Type Classes in HOL
Automating Verification by Functional Abstraction at the System Level
Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
Recursive Function Definition for Types with Binders
A Practical Method for Reasoning about Distributed Systems in a Theorem Prover
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment
Using HOL to produce custom verification tools
The Seventeen Provers of the World, Foreword by Dana S. Scott
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling
Total-Correctness Refinement for Sequential Reactive Systems
A Structural Embedding of Ocsid in PVS
Executing Formal Specifications by Translation to Higher Order Logic Programming
Verifying a Garbage Collection Algorithm
Server-Process Restrictiveness in HOL
Exploiting Parallelism in Interactive Theorem Provers
Formalised Cut Admissibility for Display Logic
The Semantics of Statecharts in HOL
Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL
Inheritance in Higher Order Logic: Modeling and Reasoning
A Certified Polynomial-Based Decision Procedure for Propositional Logic
Extensible Hierarchical Tactic Construction in a Logical Framework
A Formulation of TLA in Isabelle
Formal Analysis of Optical Waveguides in HOL
On the Correctness of Operating System Kernels
Weak Alternating Automata in Isabelle/HOL
Defining Recursive Functions in HOL
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
Co-inductive Axiomatization of a Synchronous Language
Integrating a First-Order Automatic Prover in the HOL Environment
Verification of Compiler Correctness for the WAM
Formalizing Integration Theory with an Application to Probabilistic Algorithms
Design-Flow Graph Partitioning
Twenty Years of Theorem Proving for HOLs Past, Present and Future
Verified Bytecode Model Checkers
Refinement Calculus for Logic Programming in Isabelle/HOL
A Type of Partial Recursive Functions
Verification of Expectation Properties for Discrete Random Variables in HOL
Predicates, Temporal Logic, and Simulations
Formal Verification of Exact Computations Using Newton's Method
Fast Tactic-Based Theorem Proving
Proof Pearl: Looping Around the Orbit
Function Definition in Higher-Order Logic
Simulating Microprocessors from Formal Specifications
Reasoning about Petri Nets in HOL
A Prototype Proof Translator from HOL to Coq
Possibly Infinite Sequences in Theorem Provers: A Comparative Study
A Brief Overview of Agda - A Functional Language with Dependent Types
Verification in Higher Order Logic of Mutual Exclusion Algorithm
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
A New Interface for HOL - Ideas, Issues and Implementation
A Classical Type Theory with Transfinite Types
Formal Methods at NASA Langley
Abstraction and Refinement in Higher Order Logic
The HOL Logic Extended with Quantification over Type Variables
Higher Order Unification 30 Years Later
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic
Otter/Ivy
A HOL Decision Procedure for Elementary Real Algebra
Modelling Bit Vectors in HOL: the word library
Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings
A Short Presentation of Coq
Minlog
Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings
Certification of Termination Proofs Using CeTA
The Twelf Proof Assistant
The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover
Modeling a Hardware Synthesis Methodology in Isabelle
Packaging Mathematical Structures
Adding External Decision Procedures to HOL90 Securely
Tracking Design Changes with Formal Verification
Polytypic Proof Construction
The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL
Fix-Point Equations for Well-Founded Recursion in Type Theory
An HOL Theory for Logic States with Indeterminate Strengths
Higher-Order Annotated Terms for Proof Search
ML Programming in Constructive Type Theory (abstract)
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction
Nested General Recursion and Partiality in Type Theory
Verifying a Secure Information Flow Analyzer
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle
Classical Propositional Decidability via Nuprl Proof Extraction
A Proof Development System for HOL
Refining Reactive Systems in HOL Using Action Systems
Source-Level Proof Reconstruction for Interactive Theorem Proving
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
A Sequent Formulation of a Logic of Predicates in HOL
On the Mechanization of Real Analysis in Isabelle/HOL
Recursive Boolean Functions in HOL
Mechanizing Security in HOL
Set Theory, Higher Order Logic or Both?
Adding New Rules to an LCF-style Logic Implementation
JavaCard Program Verification
Reasoning About Software
Proving Liveness of Fair Transition Systems
A Hierarchical Method for Reasoning about Distributed Programming Languages
Importing MDG Verification Results into HOL
Essential Incompleteness of Arithmetic Verified by Coq
Certifying Machine Code Safety: Shallow Versus Deep Embedding
Calculational Reasoning Revisited (An Isabelle/Isar Experience)
Automatically Translating Type and Function Definitions from HOL to ACL2
Reachability Programming in HOL98 Using BDDs
Meta Reasoning in ACL2
Changing Data Representation within the Coq System
A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor
Formalising Java's Data Race Free Guarantee
A Mechanized Logic for Secure Key Escrow Protocol Verification
Higher Order Quotients and their Implementation in Isabelle HOL
Verifying Uniqueness in a Logical Framework
Towards Applying the Composition Principle to Verify a Microkernel Operating System
A Compiled Implementation of Normalization by Evaluation
A Comparison of PVS and Isabelle/HOL
HOL
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
Proof Pearl: Defining Functions over Finite Sets
Proving the Equivalence of Microstep and Macrostep Semantics
A Formally Verified Prover for the ALC Description Logic
Program Derivation Using the Refinement Calculator
Proving Bounds for Real Linear Programs in Isabelle/HOL
Modelling Non-Deterministic System in HOL
Using a PVS Embedding of CSP to Verify Authentication Protocols
Extended First-Order Logic
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation
Isar - A Generic Interpretative Approach to Readable Formal Proof Documents
Formal Verification of a SHA-1 Circuit Core Using ACL2
Mechanical Verification of Distributed Algorithms in Higher-Order Logic
Proceedings of the First Workshop on Verification of Adaptive Systems, VerAS@TPHOLs 2007, Kaiserslautern, Germany, September 14, 2007
Embedding of Systems of Affine Recurrence Equations in Coq
Lightweight Separation
On the Implementation of an Extensible Declarative Proof Language
Reasoning about Real Circuits
Algebraic Structures and Dependent Records
Three Tactic Theorem Proving
Experiments with ZF Set Theory in HOL and Isabelle
Automating the Search for Answers to Open Questions
Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings
A Type Annotation Scheme for Nuprl
Formalizing Stålmarck's Algorithm in Coq
Proof Reuse with Extended Inductive Types
Floating Point Verification in HOL
Formalising Generalised Substitutions
Secure Microkernels, State Monads and Scalable Refinement
An Automata Theory Dedicated towards Formal Circuit Synthesis
Mechanising some Advanced Refinement Concepts
Reasoning About a Class of Linear Systems of Equations in HOL
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic
Stucture and Behaviour in Hardware Verification
A Structure Preserving Encoding of Z in Isabelle/HOL
A Comparative Study of Coq and HOL
Equational Reasoning via Partial Reflection
Inference Rules for Programming Languages with Side Effects in Expressions
From PSL to LTL: A Formal Validation in HOL
First-Class Type Classes
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
Nominal Inversion Principles
Another Look at Nested Recursion
Abstractions for Fault-Tolerant Distributed System Verification
A Modular Coding of UNITY in COQ
Toward a Super Duper Hardware Tactic
AC Unification in HOL90
A Brief Overview of Mizar
Verifying Arithmetic Hardware in Higher-Order Logic
Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions
Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms
A Brief Overview of PVS
Liveness Reasoning with Isabelle/HOL
A Strong and Mechanizable Grand Logic
Linking Other Theorem Provers to HOL Using PM: Proof Manager
Without Loss of Generality
Formal Tools in Tri-State Design in Busses
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing
Formal Reasoning About Causality Analysis
HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux
A Functional Approach for Formalizing Regular Hardware Structures
Mechanizing Program Verification in HOL
TkWinHOL: A Tool for Window Inference in HOL
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
A Mechanisation of Computability Theory in HOL
Dependently Typed Records for Representing Mathematical Structure
Proving Compatibility Using Refinement
A HOL Formalisation of the Temporal Logic of Actions
CoCoA and CoCoALib: Fast Prototyping and Flexible C++ Library for Computations in Commutative Algebra
Ideal Centroid Striving: An Unsupervised and Prediction Parameterized Anomaly Detection Method
Landscape Analysis using Simulated Annealing
Deciding Conjugacy in Thompson's Group F in Linear Time
Role-Based Access Control in Software Services: Theory vs. Practice
An Energy Efficient Intelligent Wireless Body Area Network for Real-Time Vital Signs Monitoring
Checking Correctness and Compliance of Integrated Process Models
Pivot-Free Block Matrix Inversion
A Parallel Algorithm for Rendering Huge Terrain Surfaces
Hybrid Immune Based Method for Generating Healthy Meals for Older Adults
Feature Extraction Using Genetic Programming with Applications in Malware Detection
12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010, Timisoara, Romania, 23-26 September 2010
The CMDS Medical Diagnosis System
Using Domain Specific Hierarchical Good Practice for Ranking Service Compositions
Ontology engineering with Large Language Models
Parallel CBIR System for Efficient Hyperspectral Image Retrieval from Heterogeneous Networks of Workstations
What is Hybrid Symbolic-Numeric Computation?
Weighted Threshold RSA Based on the Chinese Remainder Theorem
Soft Competitive Learning and Growing Self-Organizing Neural Networks for Pattern Classification
SORMSYS: Towards a Resource Management Platform for Self-Organizing Large Scale Distributed Systems
Building Agent-Based Simulations Using Structural and Process Mental Models
What Does "Without Loss of Generality" Mean (And How Do We Detect It)
Proof of Useful Work Based on Matrix Computation
Automated Software Analysis
Unified Strategy for Feature Selection and Data Imputation
Generic Representation for Extension-Based Semantics of Argumentation Frameworks
Improving Lost/Won Classification in CRM Systems Using Sentiment Analysis
Scalable Task Deployment System Inspired from Virus Propagation Models for Large Distributed Workflow Based Systems
Eye Detection For Drivers Using Convolutional Neural Networks With Automatically Generated Ground Truth Data
An Adaptive Particle Swarm Optimizer Using Balanced Explorative and Exploitative Behaviors
On One Approach to Goal-Driven Proof Search in Classical First-Order Logic
Opinion Influence Analysis in Online Forum Threads
A Fraudster in a Haystack: Crafting a Classifier for Non-delivery Fraud Prediction at Online Auction Sites
Improving ACSTL Iris Segmentation Method
Graphs hard-to-process for greedy algorithm MIN
Supporting Heterogeneous Pools in a Single Ceph Storage Cluster
Implementation and Evaluation Model for the Asynchronous Search Techniques: From a Synchronously Distributed System to an Asynchronous Distributed System
Proof Techniques for Synthesis of Sorting Algorithms
Particle Swarm Optimization Hybrids for Searching Ground States of Ising Spin Glasses
Automatic and Reliable Distribution of Data in Grids over Globus Toolkit
Evolutionary Design of Deep Neural Networks
GLinda - Grid-Based Distributed Linda System
A Security Protocol for Vehicular Distributed Systems
Machine Learning Based Approaches for Sex Identification in Bioarchaeology
Exploring Sum-Product Networks for Image Classification. Applications
Double distillation for class incremental learning
Toward Non-flat Geometrical Origami Folds with Eos System
Multi-agent Resource Allocation Algorithm Based on the XSufferage Heuristic for Distributed Systems
A Compiler for Origami Construction and Verification
Optimising Artificial Neural Network topologies using Genetic Algorithms with very small populations
Optimization of Resource Scheduling in Cloud Computing
Automatic Improvements of Wallis' Inequality
PEARLS: An Integrated Environment for Task Scheduling
Uniform SAmplINg with BOLTZmann
Survey on Feasibility of Pattern Matching Techniques In Heterogeneous Architectures for Bioinformatics
Topological Image Analysis and (Normalised) Representations for Plant Phenotyping
SMT Solvers for Testing, Program Analysis and Verification at Microsoft
What is an Equation?
Minimizing Resource Rent Loss while Maximizing User Availability in Cloud Applications through Online Switching of the Scaling Method
A Poly-algorithmic Approach to Quantifier Elimination
Analyzing WMSOL Definable Properties on Sum-Like Weighted Labeled Trees
Psychologically Inspired, Rule-Based Outlier Detection in Noisy Data
Concern-Oriented and Ontology-Based Design Approach of Software Architectures
Theory and Practice of Programming Applied to Membrane Systems
Extended Z3 Array
A Numerical Solution of the Semi Linear Singularly Perturbed Boundary Value Problem Using Multi Region Finite Difference Method
AFOPT Algorithm for Multi-Level Databases
Lagrange Inversion and Lambert W
Prepared for Lift-Off: Hybrid CNN-LSTM Architecture for Aircraft Engine Remaining Useful Life Estimation
Incremental Deterministic Planning
A Proposed Automatic Speech and Sentiment Recognition Serious Game for Older Adults with Parkinson's Disease
Composite clustering crossover operator for improving genetic algorithms
A Hybrid Genetic Programming and Boosting Technique for Learning Kernel Functions from Training Data
Optimized Zero False Positives Perceptron Training for Malware Detection
Properties of Multisets Compared to Sets
Computing Origami Universal Molecules with Cyclic Tournament Forests
A Hybrid Test Generation Approach Based on Extended Finite State Machines
Early Prediction of the Cost of HPC Application Execution in the Cloud
Towards Using Grid Services for Mining Fuzzy Association Rules
An Evolutionary Approach for Modeling Time Series
Using Cylindrical Algebraic Decomposition and Local Fourier Analysis to Study Numerical Methods: Two Examples
Tuning Evolutionary Algorithm Performance Using Nature Inspired Heuristics
Cellular Automata Applications
Towards a Multi-Agent System for Medical Records Processing and Knowledge Discovery
AlphaFold-based protein analysis pipeline
Topic Modeling Using Contextual Cues
Numerically Optimizing Weights for Monte Carlo Integration on Smooth Compact Manifolds
Automatic Assessment of Cardiac Artery Disease by Using DCAD Module
A Reinforcement Learning Approach for Solving the Fragment Assembly Problem
Coloring Random Graphs: A Short Survey
BluEJAMM: A Bluespec Embedded Java Architecture with Memory Management
Levenberg-Marquardt Learning Algorithm for Quaternion-Valued Neural Networks
Multi-phase Identification in Microstructures Images Using a GPU Accelerated Fuzzy C-Means Segmentation
Combining Meta-Heuristics to Solve the Rook Problem
Quantum Reinforcement Learning in Protein Folding
Assessing Features Importance in the 15-Class Galaxy Classification Problem
Resource Competition and Synchronization in Membranes
System Description: Statistical Parsing of Informalized Mizar Formulas
A Supervised Learning Process to Elicit Fraud Cases in Online Auction Sites
Real-Time Computation of Legendre-Sobolev Approximations
Parallel Migration Models Applied to Competitive Differential Evolution
Ontology-Based Recommender for Distributed Machine Learning Environment
Software Random Number Generation Based on Race Conditions
Tiers of webOrigami Programming
On the Variants of Subset Sum: Projected and Unbounded
On the Existence of 1-Bounded Bi-ideals with the WELLDOC Property
Motif Detection in Biological Networks
Correct Metric Semantics for a Biologically-Inspired Formalism
Color Grading with Neural Network
Grid Service Based on GIMP for Processing Remote Sensing Images
Towards Validating Prediction Systems for Process Understandability: Measuring Process Understandability
A Practical Guide for Detecting the Java Script-Based Malware Using Hidden Markov Models and Linear Classifiers
Leveraging self-supervised label generation in ego-trajectory segmentation for self-driving vehicles
Gröbner Bases Computation and Macaulay Matrices
Solving Nonsmooth Interval Equations with Slopes
A Metric-Based Approach to Modelling a Virtual Machine for Smart Contract Execution
Evolutionary Support Vector Regression Machines
SUDS: A Simplified U-Net Architecture with Depth-Wise Separable Convolutions
Timed Catalytic Petri Nets
Assessing Predictor Influence in LSTM Models for Enhanced Solar Energy Forecasting
The Confluence Property for Petri Nets and its Applications
Termination Analysis by Program Inversion
Computation Results of the Riemann Zeta Search Project
Artificial Conflict Sampling for Real Satisfiability Problems
Behavioral Trading System - Detecting Crisis, Risk and Stability in Financial Markets
McC and Mc#: Unified C++ and C# Design Facts Extractors Tools
Learning to Maximize Return in a Stag Hunt Collaborative Scenario through Deep Reinforcement Learning
A Duality-Aware Calculus for Quantified Boolean Formulas
Efficient Computation of the Isotropy Group of a Finite Graph: A Combinatorial Approach
A New Approach for Accelerating the Sparse Matrix-Vector Multiplication
Decentralized Dynamic Resource Allocation for Workflows in Grid Environments
Token Free Bounded Delay Codes and Hash Iteration
Customized Reflection Lines for Surface Interrogation in Car Body Design
Gödel Incompleteness and Proof-Assistants Extended Abstract
26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2024, Timisoara, Romania, September 16-19, 2024
Static Analysis in Finitely Supported Mathematics
Grid-Aware Intrusion Detection System Using Gossip Algorithms
New Techniques in Numerical Analysis for Artificial Intelligence
Investigation of Alternative Evolutionary Prototype Generation in Medical Classification
Computer Aided Diagnosis for Contrast-Enhanced Ultrasound Using Transformer Neural Network
Cph CT Toolbox: CT Reconstruction for Education, Research and Industrial Applications
Application of Meaningful Text Analytics to Online Product Reviews
Dataset Distillation via Multi-objective Genetic Algorithms
SPIKE, an automatic theorem prover - revisited
Generating Healthy Menus for Older Adults Using a Hybrid Honey Bees Mating Optimization Approach
Relational Operators in Heterogeneous Random Databases
Aesthetic Evolution of Target 3D Volumes in Minecraft
24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2022, Hagenberg / Linz, Austria, September 12-15, 2022
Business Reviews Classification Using Sentiment Analysis
Functional-Based Synthesis of Systolic Online Multipliers
Using N-Gram Variations in Static Analysis for Malware Detection
Traders' Behavior Effect on Stock Price Evolution
Assessing SLA Compliance from Palladio Component Models
Enhancing the performance of software effort estimation through boosting ensemble learning
23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021, Timisoara, Romania, December 7-10, 2021
Implementing Reasoning Modules in Implicit Induction Theorem Provers
Intelligent Agent for Food Recognition in a Smart Fridge
SAT-Based Big-Step Local Search