yusuke1997/dblp-id-title huggingface dataset:
CRIS: The Power of Imagination in Specification and Verification (Invited Talk)
Formalizing Polynomial Laws and the Universal Divided Power Algebra
Constructive Formalization of Hybrid Logic with Eventualities
Lutsig: a verified Verilog compiler for verified circuit development
Formal verification of control-flow graph flattening
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR
Univalent Double Categories
Mechanized Verification of Computing Dominators for Formalizing Compilers
Formalizing π-calculus in guarded cubical Agda
A Recipe for Modular Verification of Generic Tree Traversals
A Compositional Semantics for Verified Separate Compilation and Linking
Coq's vibrant ecosystem for verification engineering (invited talk)
Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda
Program Certification by Higher-Order Model Checking
Matching logic: the foundation of the K framework (invited talk)
Exploration of neural machine translation in autoformalization of mathematics in Mizar
The Speedup Theorem in a Primitive Recursive Framework
Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
Proof Pearl: The Marriage Theorem
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions
A modular, efficient formalisation of real algebraic numbers
A linear logical framework in hybrid (invited talk)
Formal microeconomic foundations and the first welfare theorem
Undecidability of higher-order unification formalised in Coq
A Formal Model and Correctness Proof for an Access Control Policy Framework
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Equivalence of system f and ź2 in Coq based on context morphism lemmas
Semantic cut elimination for the logic of bunched implications, formalized in Coq
Formalization of a newton series representation of polynomials
A machine-checked direct proof of the Steiner-lehmus theorem
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi
A Coq formalization of data provenance
Mechanised Semantics for Gated Static Single Assignment
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Formalization of Karp-Miller tree construction on petri nets
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Certifying the Decidability of the Word Problem in Monoids at Large
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
Markov processes in Isabelle/HOL
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
A proof-theoretic approach to certifying skolemization
Windmills of the minds: an algorithm for fermat's two squares theorem
An equational theory for weak bisimulation via generalized parameterized coinduction
Aliasing Restrictions of C11 Formalized in Coq
Formalising lie algebras
Bisimulation up-to techniques for psi-calculi
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings
The Poincaré-Bendixson theorem in Isabelle/HOL
An Isabelle/HOL Framework for Synthetic Completeness Proofs
Proof Pearl: Abella Formalization of λ-Calculus Cube Property
The HoTT library: a formalization of homotopy type theory in Coq
Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection
Formalizing determinacy of concurrent revisions
A minimalistic verified bootstrapped compiler (proof pearl)
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025
A verified prover based on ordered resolution
A verified algorithm for detecting conflicts in XACML access control rules
A Coq formalization of normalization by evaluation for Martin-Löf type theory
Overcoming restraint: composing verification of foreign functions with cogent
Triangulating context lemmas
Three equivalent ordinal notation systems in cubical Agda
Towards formally verified compilation of tag-based policy enforcement
Applying formal verification to microkernel IPC at meta
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem
A formalization of the Berlekamp-Zassenhaus factorization algorithm
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
Layers of Confluence for Actors
Verified programming of Turing machines in Coq
Formalized Burrows-Wheeler Transform
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023
A CHERI C Memory Model for Verified Temporal Safety
Mechanized verification of preemptive OS kernels (invited talk)
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Full Reduction at Full Throttle
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk)
Formal foundations of 3D geometry to model robot manipulators
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Teaching Experience: Logic and Formal Methods with Coq
Reasoning about monotonicity in separation logic
A verified SAT solver with watched literals using imperative HOL
Certified Abstract Interpretation with Pretty-Big-Step Semantics
Mostly Sound Type System Improves a Foundational Program Verifier
Lifting proof-relevant unification to higher dimensions
A formal proof of hensel's lemma over the p-adic integers
HOπ in Coq
Proving Concurrent Noninterference
A Framework for Verifying Depth-First Search Algorithms
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
Formalising real numbers in homotopy type theory
An anti-locally-nameless approach to formalizing quantifiers
Contextual refinement of the Michael-Scott queue (proof pearl)
UTC Time, Formally Verified
A compositional proof framework for FRETish requirements
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
Certified Parsing of Regular Languages
Œuf: minimizing the Coq extraction TCB
Improved Assistance for Interactive Proof (Keynote)
Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
Shall We Juggle, Coinductively?
The vampire and the FOOL
Split Decisions: Explicit Contexts for Substructural Languages
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
CertiStr: a certified string solver
Verifying x86 instruction implementations
Verified security of BLT signature scheme
First Steps towards the Certification of an ARM Simulator Using Compcert
A drag-and-drop proof tactic
Formalizing and Computing Propositional Quantifiers
Teaching algorithms and data structures with a proof assistant (invited talk)
Implementing a category-theoretic framework for typed abstract syntax
Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)
Undecidability, incompleteness, and completeness of second-order logic in Coq
Proof assistants at the hardware-software interface (invited talk)
Computational Verification of Network Programs in Coq
A formal proof of PAC learnability for decision stumps
Producing Certified Functional Code from Inductive Specifications
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
A Formalization of Doob's Martingale Convergence Theorems in mathlib
Brack: A Verified Compiler for Scheme via CakeML
A functional proof pearl: inverting the Ackermann hierarchy
Porting the HOL light analysis library: some lessons (invited talk)
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Axiomatic semantics for compiler verification
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
VCFloat2: Floating-Point Error Analysis in Coq
On synthetic undecidability in coq, with an application to the entscheidungsproblem
Refinement based verification of imperative data structures
Certified abstract machines for skeletal semantics
The lean mathematical library
A mechanized formalization of GraphQL
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Certifiably Sound Parallelizing Transformations
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions
Formal verification of a distributed dynamic reconfiguration protocol
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016
Completeness and Decidability of de Bruijn Substitution Algebra in Coq
Formalising Sharkovsky's Theorem (Proof Pearl)
ConCert: a smart contract certification framework in Coq
Mechanized Dominator Tree Certification
On the formalisation of Kolmogorov complexity
Certified Kruskal's Tree Theorem
Finite sets in homotopy type theory
Verifying a hash table and its iterators in higher-order separation logic
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018
Formally verified big step semantics out of x86-64 binaries
Proof pearl: Braun trees
Proof-Carrying Code in a Session-Typed Process Calculus
Higher-order representation predicates in separation logic
Coq à la carte: a practical approach to modular syntax with binders
Computing Cohomology Rings in Cubical Agda
Extracting smart contracts tested and verified in Coq
A Formalization of Complete Discrete Valuation Rings and Local Fields
Formal Reasoning about the C11 Weak Memory Model
Recording Completion for Certificates in Equational Reasoning
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Towards Composable Proofs of Cache Coherence Protocols
Cylindrical Algebraic Decomposition in Coq/Rocq
Building Blocks for Step-Indexed Program Logics
A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL
P4Cub: A Little Language for Big Routers
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
Total Haskell is reasonable Coq
Formalizing category theory in Agda
Verified solving and asymptotics of linear recurrences
Leakage-Free Probabilistic Jasmin Programs
A Coq formal proof of the LaxMilgram theorem
Nominal Matching Logic with Fixpoints
From C to interaction trees: specifying, verifying, and testing a networked server
Verified Validation of Program Slicing
Formally verified differential dynamic logic
Mechanising blockchain consensus
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Constructive Completeness for Modal Logic with Transitive Closure
Dynamic class initialization semantics: a jinja extension
The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof
A Temporal Differential Dynamic Logic Formal Embedding
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
Compositional Verification of a Baby Virtual Memory Manager
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
Verification of Scalable Synchronous Queue
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL
Formal verification of semi-algebraic sets and real analytic functions
A Proposal for Broad Spectrum Proof Certificates
Frying the egg, roasting the chicken: unit deletions in DRAT proofs
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
A verified protocol buffer compiler
An Executable Semantics for CompCert C
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)
Large model constructions for second-order ZF in dependent type theory
A Formalized Reduction of Keller's Conjecture
Automatic cyclic termination proofs for recursive procedures in separation logic
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Mechanized verification of a fine-grained concurrent queue from meta's folly library
Eliminating reflection from type theory
Formalising the h-Principle and Sphere Eversion
Modular SMT Proofs for Fast Reflexive Checking Inside Coq
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Precise Reasoning about Container-Internal Pointers with Logical Pinning
The next 700 syntactical models of type theory
A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem
Coquet: A Coq Library for Verifying Hardware
Verified and Efficient Matching of Regular Expressions with Lookaround
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
A Decision Procedure for Regular Expression Equivalence in Type Theory
Certified Normalization of Context-Free Grammars
Intrinsically-typed definitional interpreters for linear, session-typed languages
A Typed C11 Semantics for Interactive Theorem Proving
On homotopy of walks and spherical maps in homotopy type theory
Mechanising and verifying the WebAssembly specification
Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting
Formalising Decentralised Exchanges in Coq
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Under-Approximation for Scalable Bug Detection (Keynote)
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory
Formalising perfectoid spaces
Lassie: HOL4 tactics by example
Adhesive Category Theory for Graph Rewriting in Rocq
The generalised continuum hypothesis implies the axiom of choice in Coq
A Formal Proof of Square Root and Division Elimination in Embedded Programs
Proofs in conflict-driven theory combination
Formally verified superblock scheduling
Intrinsically Correct Sorting in Cubical Agda
Mechanizing Synthetic Tait Computability in Istari
Compositional Verification of Concurrent C Programs with Search Structure Templates
Towards a mizar environment for isabelle: foundations and language
Formalization of Differential Privacy in Isabelle/HOL
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor
Verifying Term Graph Optimizations using Isabelle/HOL
An extension of the framework types-to-sets for Isabelle/HOL
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
Certified ACKBO
Noninterference for Operating System Kernels
Formalizing Probabilistic Noninterference
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Unification for Subformula Linking under Quantifiers
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines
Adapting proof automation to adapt proofs
Foundational Verification of Running-Time Bounds for Interactive Programs
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
A nominal exploration of intuitionism
Complx: a verification framework for concurrent imperative programs
Practical Tactics for Verifying C Programs in Coq
Mechanizing the Metatheory of mini-XQuery
BliStrTune: hierarchical invention of theorem proving strategies
A verified packrat parser interpreter for parsing expression grammars
Refinements for Free!
Formalization of Wu's Simple Method in Coq
π n (S n ) in Homotopy Type Theory
Proving Lock-Freedom Easily and Automatically
Planning for change in a formal verification of the raft consensus protocol
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
A constructive formalisation of Semi-algebraic sets and functions
Constructing the propositional truncation using non-recursive HITs
Extracting Proofs from Tabled Proof Search
A novice-friendly induction tactic for lean
Rating Disambiguation Errors
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
A Formal Disproof of Hirsch Conjecture
Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL
Call-by-push-value in coq: operational, equational, and denotational theory
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015
VeriSmall: Verified Smallfoot Shape Analysis
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026
Type-and-scope safe programs and their proofs
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
A Formally-Verified Alias Analysis
Dependent type practice (invited talk)
Certified Connection Tableaux Proofs for HOL Light and TPTP
Coherent and Strongly Discrete Rings in Type Theory
Towards efficient and verified virtual machines for dynamic languages
Machine Checked Proofs and Programs in Algebraic Combinatorics
Verbatim++: verified, optimized, and semantically rich lexing with derivatives
Automatically Verifying Typing Constraints for a Data Processing Language
Displayed Monoidal Categories for the Semantics of Linear Logic
Verified VCG and Verified Compiler for Dafny
Forward build systems, formally
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems
A unified Coq framework for verifying C programs with floating-point computations
Specification and verification of a transient stack
A Constructive Theory of Regular Languages in Coq
Univalent Semantics of Constructive Type Theories
Perspectives on formal verification (invited talk)
A Certifying Proof Assistant for Synthetic Mathematics in Lean
Formalizing jordan normal forms in Isabelle/HOL
A constructive formalization of the weak perfect graph theorem
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs
Binder aware recursion over well-scoped de Bruijn syntax
Generic derivation of induction for impredicative encodings in Cedille
Completeness and decidability of converse PDL in the constructive type theory of Coq
Towards verifying ethereum smart contract bytecode in Isabelle/HOL
(Deep) induction rules for GADTs
Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings
Clean-Slate Development of Certified OS Kernels
A modular Isabelle framework for verifying saturation provers
Formalizing the ring of Witt vectors
Terms for Efficient Proof Checking and Parsing
Reflection, rewinding, and coin-toss in EasyCrypt
Martin-Löf à la Coq
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
REPLica: REPL instrumentation for Coq analysis
Epoch Load Sharing in a Network of Workstations
A computer simulation for a space-time satellite positioning system
Simulation model of a public enquiry system: Application case study in revenue Canada, taxation
A simulation of final stop consonants in speech perception using the bicameral neural network model
Proceedings 28st Annual Simulation Symposium (SS '95), April 25-28, 1995, Santa Barbara, California, USA
Implementing Parallel Cell-DEVS
SCAR - Scattering, Concealing and Recovering Data within a DHT
A multiple subsystem simulator of processor scheduling
Assessing and Improving Testing of Real-time Software using Simulation
Simulation of ram-based asynchronous sequential circuits
Power Conservation Schemes for Energy Efficient Data Propagation in Heterogeneous Wireless Sensor Networks
An Integrated Web-based Grid-Computing Environment for Research and Education in Computational Science and Engineering
Handling Delay Sensitive Contents Using Adaptive Traffic-Based Control Method for Minimizing Energy Consumption in Wireless Devices
Dynamic Structure DEVS: Improving the Real-Time Embedded Systems Simulation and Design
Performance Impacts of Superscalar Microarchitecture on SOM Execution
Model instantiation for query driven simulation in active KDL
Assessing the Performance of Multiprocessor Architectures through SWN Models Simulation: A Case Study in the Field of Plant Automation Systems
Integrated System Design, Analysis and Database-Driven Simulation Model Generation
Object-oriented design of a scene generation simulation
MC++: A Parallel, Portable, Monte Carlo Neutron Transport Code in C++
What price virtual memory?
Modelling and Performability Analysis of Network Memory Servers
Sensitivity of predictive scheduling
Model Reduction: Some Results
Performance Evaluation and Analysis of Protocols for IP Mobility Support: A Quantitative Study
Multiresolution Behavioral Modeling in a Virtual Environment
A case against event-driven simulation for digital system design
Fair Arbitration in Point-to-Point Networks
Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18-22 April 2004, Arlington, VA, USA
A Generic Simulator of Real-Time Scheduling Algorithms
Trace Driven modeling: An update
Management of a large computer network simulation project
A Collaborative Service-Oriented Simulation Framework with Microsoft Robotic Studio®
An algorithm for parallel discrete event simulation using common memory
Design of an environment for physical phenomena simulation: application to visualization and animation of electrostatic field and potential
A performance comparison of adaptive and static load balancing in heterogeneous distributed systems
Simulation of fast packet-switched photonic networks for interprocessor communication
SIM-ENG: A Traffic Simulation Engine
The effect of strict firing and real characteristics of multiprocessors on performance - a simulation approach
Controlling Buffer Usage in Critical Channel Traversing
Performance Analysis of Parallel Job Scheduling in Distributed Systems
Warplog: Time Warped Logical Objects
The computer system representation problem
Performance Analysis for Data Service in Third Generation Mobile Telecommunication Networks
A Framework for Adaptive Wavelet Prediction in Self-Sizing Networks
The design of a multi-microprocessor based simulation computer - I
Cyclo-static multiprocessing model and simulation results
Comparative Analysis of Scheduling Algorithms For Integrated Service Networks
Efficient memory simulation in SimICS
Simulating the DASH Architecture in HASE
A tool to aid in model development and validation
Modeling and Simulation of a Fault Tolerant ATM Switching Architecture
A C++ Environment For Modeling Communication Systems
Simulating The Global Directory Service With OPNET
Parallel Simulation: Past, Present, and Future
A Parallel Algorithm For Dynamics Simulation Of Multibody Chains-implementation On A Transputer System
TimeNET-Sim-a parallel simulator for stochastic Petri nets
Digital simulation as an evaluation aid in the development of dynamic color graphics human-machine interfaces
Temporal Uncertainty Time Warp: An Agent-Based Implementation
Adapting MASCOT Methodology to Software Performance Engineering using Object-Oriented Simulation
Coping with Complexity: Abstractions, Models, and Data