| The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar |
13 |
| Compositional Falsification of Cyber-Physical Systems with Machine Learning Components |
6 |
| Synthesis of Obfuscation Policies to Ensure Privacy and Utility |
5 |
| Hammer for Coq: Automation for Dependent Type Theory |
4 |
| Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories |
3 |
| VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
3 |
| System-Level Non-interference of Constant-Time Cryptography. Part I: Model |
3 |
| Verified iptables Firewall Analysis and Verification |
2 |
| Formalization of the Resolution Calculus for First-Order Logic |
2 |
| Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits |
2 |
| A Unifying View on SMT-Based Software Verification |
2 |
| Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF |
2 |
| Formally Verifying the Solution to the Boolean Pythagorean Triples Problem |
2 |
| Guarded Cubical Type Theory |
2 |
| Verifying Relative Safety, Accuracy, and Termination for Program Approximations |
2 |
| Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic |
2 |
| Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory |
1 |
| Canonicity for Cubical Type Theory |
1 |
| Formal Verification of an Executable LTL Model Checker with Partial Order Reduction |
1 |
| Classification of Finite Fields with Applications |
1 |
| An Isabelle/HOL Formalisation of Green's Theorem |
1 |
| Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude |
1 |
| CoSMed: A Confidentiality-Verified Social Media Platform |
1 |
| A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality |
1 |
| QPCF: Higher-Order Languages and Quantum Circuits |
1 |
| Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic |
1 |
| A Proof Theory for Model Checking |
1 |
| Amortized Complexity Verified |
1 |
| Fast Formal Proof of the Erds-Szekeres Conjecture for Convex Polygons with at Most 6 Points |
1 |
| Bidirectional Grammars for Machine-Code Decoding and Encoding |
1 |
| The Flow of ODEs: Formalization of Variational Equation and Poincare Map |
1 |
| Proof Pearl: Bounding Least Common Multiples with Triangles |
1 |
| From Types to Sets by Local Type Definition in Higher-Order Logic |
1 |
| An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains |
1 |
| Efficient Active Automata Learning via Mutation Testing |
1 |
| Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL |
1 |
| Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq |
1 |
| Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic |
1 |
| Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL |
1 |
| On the Generation of Quantified Lemmas |
1 |
| Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs |
0 |
| Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants |
0 |
| Long-Distance Q-Resolution with Dependency Schemes |
0 |
| Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches |
0 |
| Verifying OpenJDK's Sort Method for Generic Collections |
0 |
| Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae |
0 |
| Formally Verified Approximations of Definite Integrals |
0 |
| Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms |
0 |
| The Matrix Reproved (Verification Pearl) |
0 |
| Automated Verification of Functional Correctness of Race-Free GPU Programs |
0 |
