Pith. sign in

REVIEW 1 cited by

Programming Language Features for Refinement

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1606.02022 v1 pith:VPODPQEV submitted 2016-06-07 cs.PL cs.SE

Jason Koenig (Stanford University) , K. Rustan M. Leino (Microsoft Research) This is my paper · ORCID
classification cs.PLcs.SE
keywords refinementfeatureslanguageprogrammingprogramsomeaddedalgorithmic
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming language, but mainstream languages lack features for recording the sequence of refinement steps in the program text. To experiment with the combination of refinement, automated verification, and language design, refinement features have been added to the verification-aware programming language Dafny. This paper describes those features and reflects on some initial usage thereof.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement

    cs.SE 2026-06 unverdicted novelty 7.0 of 10

    Framework uses LLM-driven stepwise application of transformation rules to generate verifiable RTL hardware designs from specifications.

Pith tools