On the public citation graph

Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study

https://doi.org/10.29007/ddqm
0 signed · 35 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11813040_19openalex-snapshot
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions
inferredcites →https://doi.org/10.1007/11889229_6openalex-snapshot
A Tutorial Introduction to CSP in Unifying Theories of Programming
inferredcites →https://doi.org/10.1007/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/978-1-84882-912-1_5openalex-snapshot
Forward with Hoare
inferredcites →https://doi.org/10.1007/978-3-031-40744-4_5openalex-snapshot
Suspending OpenMP Tasks on Asynchronous Events: Extending the Taskwait Construct
inferredcites →https://doi.org/10.1007/978-3-319-08970-6_25openalex-snapshot
An Isabelle Proof Method Language
inferredcites →https://doi.org/10.1007/978-3-319-14806-9_2openalex-snapshot
Isabelle/UTP: A Mechanised Theory Engineering Framework
inferredcites →https://doi.org/10.1007/978-3-319-46750-4_17openalex-snapshot
Unifying Heterogeneous State-Spaces with Lenses
inferredcites →https://doi.org/10.1007/978-3-319-56841-6_2openalex-snapshot
UTP by Example: Designs
inferredcites →https://doi.org/10.1007/978-3-540-71067-7_16openalex-snapshot
Secure Microkernels, State Monads and Scalable Refinement
inferredcites →https://doi.org/10.1007/978-3-642-14203-1_9openalex-snapshot
Sledgehammer: Judgement Day
inferredcites →https://doi.org/10.1007/978-3-642-27705-4_16openalex-snapshot
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report
inferredcites →https://doi.org/10.1007/978-3-642-32347-8_8openalex-snapshot
Bridging the Gap: Automatic Verified Abstraction of C
inferredcites →https://doi.org/10.1007/978-3-642-38916-0_5openalex-snapshot
Test Program Generation for a Microprocessor
inferredcites →https://doi.org/10.1007/s00165-010-0152-5openalex-snapshot
The dynamic frames theory
inferredcites →https://doi.org/10.1007/s10817-015-9360-2openalex-snapshot
Eisbach: A Proof Method Language for Isabelle
inferredcites →https://doi.org/10.1090/psapm/019/0235771openalex-snapshot
Assigning meanings to programs
inferredcites →https://doi.org/10.1093/comjnl/5.1.10openalex-snapshot
Quicksort
inferredcites →https://doi.org/10.1109/lics.2002.1029817openalex-snapshot
Separation logic: a logic for shared mutable data structures
inferredcites →https://doi.org/10.1145/1629575.1629596openalex-snapshot
seL4
inferredcites →https://doi.org/10.1145/27651.27653openalex-snapshot
Laws of programming
inferredcites →https://doi.org/10.1145/363235.363259openalex-snapshot
An axiomatic basis for computer programming
inferredcites →https://doi.org/10.13182/nse68-a19548openalex-snapshot
The Art of Computer Programming
inferredcites →https://doi.org/10.26153/tsw/53177openalex-snapshot
Notes on Structured Programming
inferredcites →https://doi.org/10.29007/tnfdopenalex-snapshot
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-030-43520-2_7openalex-snapshot
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
inferred← citeshttps://doi.org/10.1007/978-3-031-66064-1_5openalex-snapshot
Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/978-3-031-69042-6_3openalex-snapshot
Certification of Sorting Algorithms Using Theorema and Coq
inferred← citeshttps://doi.org/10.1109/iceccme62383.2024.10796722openalex-snapshot
Certification of Insert-Sort and Merge-Sort in Coq
inferred← citeshttps://doi.org/10.1109/itsc48978.2021.9564771openalex-snapshot
Optimizing test-set diversity: Trajectory clustering for scenario-based testing of automated driving systems
inferred← citeshttps://doi.org/10.1109/itsc48978.2021.9564790openalex-snapshot
Towards threat metric evaluation in complex urban scenarios
inferred← citeshttps://doi.org/10.1109/itsc48978.2021.9565084openalex-snapshot
What if? Behavior Estimation by Predicting Traffic Scenes from State Histories
inferred← citeshttps://doi.org/10.1109/iv48863.2021.9575822openalex-snapshot
Self-Supervised Action-Space Prediction for Automated Driving
inferred← citeshttps://doi.org/10.23919/mipro52101.2021.9597065openalex-snapshot
5G-Connected Drone for Public Road Safety-Research Challenges and Future Research Roadmap
inferred← citeshttps://doi.org/10.29007/spjsopenalex-snapshot
Certification of Tail Recursive Bubble--Sort in Theorema and Coq
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.